Containment and refinement of rational-power logarithm bounds

The logarithm enclosures contain the exact logarithms, and their endpoints converge as the degree grows. Scaling and subtraction preserve both properties. Doubling the degree therefore separates the logarithm difference from zero whenever the power differs from the target, and the comparison that relies on this decides the equality case beforehand.

theorem FloatLib.Numerics.RationalPower.contains_logDifference (base exponent target : ℚ) (degree : ℕ) (hbase : 0 < base) (htarget : 0 < target) : (logDifference base exponent target degree).Contains (Real.log (↑base ^ ↑exponent) - Real.log ↑target)

The executable interval contains the exact difference of real logarithms.

theorem FloatLib.Numerics.RationalPower.tendsto_logDifference_lo (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 < target) : Filter.Tendsto (fun (degree : ℕ) => ↑(logDifference base exponent target degree).lo) Filter.atTop (nhds (Real.log (↑base ^ ↑exponent) - Real.log ↑target))

Lower endpoints converge to the exact logarithm difference.

theorem FloatLib.Numerics.RationalPower.tendsto_logDifference_hi (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 < target) : Filter.Tendsto (fun (degree : ℕ) => ↑(logDifference base exponent target degree).hi) Filter.atTop (nhds (Real.log (↑base ^ ↑exponent) - Real.log ↑target))

Upper endpoints converge to the exact logarithm difference.

theorem FloatLib.Numerics.RationalPower.exists_logDifference_separating (base exponent target : ℚ) (hbase : 0 < base) (htarget : 0 < target) (hne : ↑base ^ ↑exponent ≠ ↑target) : ∃ (level : ℕ), Enclosure.Comparison.Separates (logDifference base exponent target (2 ^ level)) 0

When the power differs from the target, doubling the degree eventually gives a logarithm bound that excludes zero.