npow_contains_pow
plain-language theorem explainer
If a real x lies in a closed interval I with positive rational lower bound, then x to a natural power n lies inside the interval whose endpoints are the corresponding powers of I's endpoints. Researchers building verified bounds for polynomials or iterated functions in exact arithmetic would cite this to chain containments. The tactic proof casts positivity, deduces x > 0, and invokes the monotonicity lemma pow_le_pow_left₀ on each endpoint.
Claim. Let $I=[a,b]$ be a closed interval with rational endpoints satisfying $a>0$ and $a≤b$. If a real number $x$ satisfies $a≤x≤b$, then for any natural number $n$ the real $x^n$ satisfies $a^n≤x^n≤b^n$.
background
This module supplies verified interval arithmetic with rational endpoints to bound real-valued computations. An Interval is a structure consisting of rational lower and upper bounds together with the validity condition that the lower bound does not exceed the upper. The contains predicate asserts that a real lies between these bounds after casting to reals: $(I.lo:ℝ)≤x∧x≤(I.hi:ℝ)$ (quoted from the sibling definition).
proof idea
The tactic proof first casts the positivity hypothesis on the lower bound to reals and deduces that x itself is positive via lt_of_lt_of_le. It then constructs the two-sided containment by applying pow_le_pow_left₀ (the lemma that 0≤a≤b implies a^n≤b^n) once to the lower endpoint and once to the upper endpoint after the positivity adjustment.
why it matters
This lemma supplies a basic building block for rigorous powering inside the numerics layer that supports bound computations on transcendental functions. It aligns with the module's goal of using exact rational endpoints to enclose real values, enabling downstream chaining of interval containments without floating-point error. No downstream uses are recorded yet, leaving open its integration into larger verified pipelines for constants or ladders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.