Soundness of binary-grid exponential and logarithm enclosures

Rounded Horner steps and rectangular splitting contain the exponential and odd logarithm Taylor polynomials. Rounded powers and exact scalar factors enclose their remainder bounds. Mathlib's real estimates therefore apply at every grid precision, including zero.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.contains_toRationalInterval (precision : ℕ) (I : Interval ℤ) (x : ℝ) : (toRationalInterval precision I).Contains x ↔ Interval.ContainsReal (Interval.BinaryGrid.decode precision) I x

Decoding the final grid endpoints preserves real containment.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_scaleRat (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) I x) (factor : ℚ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (scaleRat I factor) (↑factor * x)

Scalar rounding encloses the exact rational multiple of every real input member.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_divideNat (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) I x) (n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (divideNat I n) (x / ↑n)

Natural scalar division rounds outward without requiring a grid divisor interval.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_around (precision : ℕ) {midpoint radius : Interval ℤ} {m r x : ℝ} (hm : Interval.ContainsReal (Interval.BinaryGrid.decode precision) midpoint m) (hr : Interval.ContainsReal (Interval.BinaryGrid.decode precision) radius r) (herror : |x - m| ≤ r) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (around midpoint radius) x

Midpoint and radius enclosures turn an absolute-error estimate into grid containment.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_expHorner (precision : ℕ) {X : Interval ℤ} {x : ℚ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X ↑x) (start n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (expHorner precision X start n) ↑(Taylor.horner (Taylor.expStep x) start n 0)

Each rounded exponential Horner step contains the corresponding exact polynomial tail.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logOddHorner (precision : ℕ) {X Q : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X x) (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q (x ^ 2)) (start n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logOddHorner precision X Q start n) (∑ i ∈ Finset.range n, x ^ (2 * i + 1) / ↑(2 * (start + i) + 1))

Rounded odd Horner steps enclose the corresponding tail of the logarithm polynomial.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_expRadius (precision : ℕ) {X : Interval ℤ} {x : ℚ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X ↑x) (n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (expRadius precision X n) ↑(Enclosure.expRadius x n)

The rounded exponential radius contains the rational remainder bound Enclosure.expRadius.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_expSmall (x : ℚ) (degree precision : ℕ) (hx : |x| ≤ 1) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (expSmall x degree precision) (Real.exp ↑x)

For |x| ≤ 1, the grid Taylor enclosure expSmall contains exp x.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_squareRepeat (precision : ℕ) {I : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) I x) (n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (squareRepeat precision I n) (x ^ 2 ^ n)

Rounded repeated squaring contains the matching power of every real input member.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.contains_exp (x : ℚ) (degree precision : ℕ) : (exp x degree precision).Contains (Real.exp ↑x)

The binary-grid exponential encloses exp x at every degree and precision.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.size_powerTableAux (precision : ℕ) (Q : Interval ℤ) (n : ℕ) (current : Interval ℤ) (powers : Array (Interval ℤ)) : (powerTableAux precision Q n current powers).size = powers.size + n + 1

Extending a table by n steps appends n + 1 powers.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.size_powerTable (precision : ℕ) (Q : Interval ℤ) (n : ℕ) : (powerTable precision Q n).size = n + 1

A power table up to n has n + 1 entries, from the zeroth power to the nth.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_powerTableAux (precision : ℕ) {Q : Interval ℤ} {q : ℝ} (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q q) (n : ℕ) (current : Interval ℤ) (powers : Array (Interval ℤ)) (hpowers : ∀ (i : ℕ) (hi : i < powers.size), Interval.ContainsReal (Interval.BinaryGrid.decode precision) powers[i] (q ^ i)) (hcurrent : Interval.ContainsReal (Interval.BinaryGrid.decode precision) current (q ^ powers.size)) (i : ℕ) (hi : i < (powerTableAux precision Q n current powers).size) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (powerTableAux precision Q n current powers)[i] (q ^ i)

Extending a table preserves containment of each power, including the appended powers.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_powerTable (precision : ℕ) {Q : Interval ℤ} {q : ℝ} (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q q) (n i : ℕ) (hi : i ≤ n) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (powerTable precision Q n)[i] (q ^ i)

Every stored interval encloses its real power, at every grid precision.

noncomputable def FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.evenSum (q : ℝ) (start n : ℕ) : ℝ

Even-power sum that gives the odd logarithm polynomial once multiplied by the argument.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.evenSum_add (q : ℝ) (start a b : ℕ) : evenSum q start (a + b) = evenSum q start a + q ^ a * evenSum q (start + a) b

Splitting a range factors the first omitted power from the remaining terms.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_blockSumAux (precision : ℕ) {powers : Array (Interval ℤ)} {q : ℝ} (hpowers : ∀ (i : ℕ) (hi : i < powers.size), Interval.ContainsReal (Interval.BinaryGrid.decode precision) powers[i] (q ^ i)) (start n : ℕ) (hn : n ≤ powers.size) (total : Interval ℤ) {a : ℝ} (htotal : Interval.ContainsReal (Interval.BinaryGrid.decode precision) total a) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (blockSumAux powers start n total) (evenSum q start n + a)

A block accumulator contains the exact partial sum plus its incoming real value.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_blockSum (precision : ℕ) {powers : Array (Interval ℤ)} {q : ℝ} (hpowers : ∀ (i : ℕ) (hi : i < powers.size), Interval.ContainsReal (Interval.BinaryGrid.decode precision) powers[i] (q ^ i)) (start n : ℕ) (hn : n ≤ powers.size) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (blockSum powers start n) (evenSum q start n)

Each scalar block encloses the corresponding even-power polynomial.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_blockHorner (precision : ℕ) {powers : Array (Interval ℤ)} {q : ℝ} (hpowers : ∀ (i : ℕ) (hi : i < powers.size), Interval.ContainsReal (Interval.BinaryGrid.decode precision) powers[i] (q ^ i)) {stride : Interval ℤ} (start blockSize blocks : ℕ) (hstride : Interval.ContainsReal (Interval.BinaryGrid.decode precision) stride (q ^ blockSize)) (hsize : blockSize ≤ powers.size) (tail : Interval ℤ) {a : ℝ} (htail : Interval.ContainsReal (Interval.BinaryGrid.decode precision) tail a) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (blockHorner precision powers stride start blockSize blocks tail) (evenSum q start (blockSize * blocks) + q ^ (blockSize * blocks) * a)

Block Horner evaluation encloses the sum over the full blocks plus q ^ (blockSize * blocks) times the tail.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.mul_evenSum_sq (x : ℝ) (start n : ℕ) : x * evenSum (x ^ 2) start n = ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / ↑(2 * (start + i) + 1)

Multiplying the even-power sum by its argument gives the reference odd polynomial.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.LogPolynomial.containsReal_logOddRectangular (precision : ℕ) {X Q : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X x) (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q (x ^ 2)) (start n blockSize : ℕ) (hblock : 0 < blockSize) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logOddRectangular precision X Q start n blockSize) (∑ i ∈ Finset.range n, x ^ (2 * i + 1) / ↑(2 * (start + i) + 1))

Rectangular splitting encloses the same odd polynomial for every positive block size.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logOddPolynomial (precision : ℕ) {X Q : Interval ℤ} {x : ℝ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X x) (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q (x ^ 2)) (start n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logOddPolynomial precision X Q start n) (∑ i ∈ Finset.range n, x ^ (2 * i + 1) / ↑(2 * (start + i) + 1))

Both logarithm evaluation strategies enclose the reference odd polynomial.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logOddRadius (precision : ℕ) {X Q : Interval ℤ} {x : ℚ} (hx : Interval.ContainsReal (Interval.BinaryGrid.decode precision) X ↑x) (hq : Interval.ContainsReal (Interval.BinaryGrid.decode precision) Q (↑x ^ 2)) (n : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logOddRadius precision X Q x n) (|↑x| ^ (2 * n + 1) / (1 - ↑x ^ 2))

The grid remainder encloses the odd logarithm series error bound.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logSeries (x : ℚ) (degree precision : ℕ) (hx : 0 < x) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logSeries x degree precision) (Real.log ↑x)

The transformed grid series encloses the logarithm of every positive rational.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logUnreduced {value : ℚ} (hvalue : 0 < value) (precision : ℕ) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logUnreduced value precision) (Real.log ↑value)

The unreduced series encloses the logarithm of every positive rational.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.containsReal_logLarge (x : ℚ) (degree precision : ℕ) (hx : 0 < x) : Interval.ContainsReal (Interval.BinaryGrid.decode precision) (logLarge x degree precision) (Real.log ↑x)

Binary reduction and the rounded multiple of log 2 preserve logarithm containment.

theorem FloatLib.Numerics.Enclosure.BinaryGrid.contains_log (x : ℚ) (degree precision : ℕ) (hx : 0 < x) : (log x degree precision).Contains (Real.log ↑x)

Binary-grid logarithm evaluation encloses the exact logarithm at every precision.