logIntervalMono_contains_log
plain-language theorem explainer
Log of any real inside a positive rational interval I lies inside the monotonicity-derived interval with rational endpoints a and b whenever a bounds log(I.lo) from below and b bounds log(I.hi) from above. Numerics researchers building certified enclosures for transcendental functions cite this when composing interval images under log. The tactic proof extracts the two-sided containment of x, applies Real.log_le_log on each endpoint, and finishes with linarith.
Claim. Let $I$ be a closed interval with rational endpoints and positive lower bound. Let $a,b$ be rationals with $aleq b$ such that $a leq log(I_{lo})$ and $log(I_{hi}) leq b$. Then for every real $x$ with $I_{lo} leq x leq I_{hi}$, one has $a leq log x leq b$.
background
The module develops interval arithmetic for the natural logarithm on positive reals. An Interval is the structure with rational fields lo and hi together with the proof lo leq hi. The predicate contains asserts that a real lies between these endpoints. The auxiliary definition logIntervalMono builds a fresh Interval whose endpoints are the supplied rationals lo_bound and hi_bound, using only the monotonicity of log on (0,infty) to guarantee enclosure.
proof idea
The tactic unfolds contains on both intervals, extracts I.lo leq x leq I.hi from the hypothesis, and deduces positivity of x from the given lower bound. Two invocations of Real.log_le_log produce log(I.lo) leq log x and log x leq log(I.hi). Linear arithmetic then transfers the inequalities through the supplied rational bounds.
why it matters
The result certifies correctness of the logIntervalMono constructor, ensuring that the constructed interval really contains the image of I under log. It directly supports sibling constructions such as logPhiInterval that supply certified bounds for log(phi) inside the phi-ladder numerics. In the Recognition framework this supplies part of the numerical certification layer that underpins the phi-based constants and the alpha inverse interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.