Proved exponential and logarithm enclosures

The bounds below describe the output of the rational algorithms, including truncation error. They use Real.exp_bound and Real.abs_log_sub_add_sum_range_le; no external numerical oracle or unproved approximation estimate enters the argument.

The exponential reduction is valid for every rational input. The logarithm theorem requires a positive argument, so a format must handle its own zero and exceptional values before calling it.

theorem FloatLib.Numerics.Enclosure.cast_expTaylor (x : ℚ) (n : ℕ) : ↑(expTaylor x n) = ∑ i ∈ Finset.range n, ↑x ^ i / ↑i.factorial

The rational Taylor sum denotes the corresponding real Taylor polynomial.

theorem FloatLib.Numerics.Enclosure.cast_expRadius (x : ℚ) (n : ℕ) : ↑(expRadius x n) = |↑x| ^ n * ↑(n + 1) / (↑n.factorial * ↑n)

The rational error radius is the real Taylor remainder estimate.

theorem FloatLib.Numerics.Enclosure.abs_exp_sub_expTaylor_le (x : ℚ) (degree : ℕ) (hx : |x| ≤ 1) : |Real.exp ↑x - ↑(expTaylor x (degree + 1))| ≤ ↑(expRadius x (degree + 1))

The executable exponential polynomial satisfies its computed absolute-error bound.

theorem FloatLib.Numerics.Enclosure.contains_expSmall (x : ℚ) (degree : ℕ) (hx : |x| ≤ 1) : (expSmall x degree).Contains (Real.exp ↑x)

Taylor truncation and its rational remainder bound enclose the small exponential.

theorem FloatLib.Numerics.Enclosure.abs_div_expScale_lt_one (x : ℚ) : |x / 2 ^ expScale x| < 1

Dividing by the executable binary reduction scale puts the argument inside the unit ball.

theorem FloatLib.Numerics.Enclosure.exp_reduced_pow (x : ℚ) : Real.exp ↑(x / 2 ^ expScale x) ^ 2 ^ expScale x = Real.exp ↑x

Binary argument reduction is inverted by the matching power of the exponential.

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

Exact repeated squaring restores the exponential after binary argument reduction.

theorem FloatLib.Numerics.Enclosure.cast_logOneSubTaylor (x : ℚ) (n : ℕ) : ↑(logOneSubTaylor x n) = ∑ i ∈ Finset.range n, ↑x ^ (i + 1) / ↑(i + 1)

The rational logarithm polynomial denotes the real Taylor sum.

theorem FloatLib.Numerics.Enclosure.abs_log_add_logOneSubTaylor_le (x : ℚ) (degree : ℕ) (hx : |x| < 1) : |Real.log (1 - ↑x) + ↑(logOneSubTaylor x degree)| ≤ ↑(logOneSubRadius x degree)

The executable logarithm polynomial satisfies its computed absolute-error bound.

theorem FloatLib.Numerics.Enclosure.contains_logOneSub (x : ℚ) (degree : ℕ) (hx : |x| < 1) : (logOneSub x degree).Contains (Real.log (1 - ↑x))

Taylor truncation encloses log (1 - x) when |x| < 1.

theorem FloatLib.Numerics.Enclosure.abs_log_argument_lt_one (x : ℚ) (hx : 0 < x) : |(x - 1) / (x + 1)| < 1

The logarithm change of variable maps a positive input into (-1, 1).

theorem FloatLib.Numerics.Enclosure.log_argument_identity (x : ℚ) (hx : 0 < x) : Real.log (1 + ↑((x - 1) / (x + 1))) - Real.log (1 - ↑((x - 1) / (x + 1))) = Real.log ↑x

The transformed logarithms reconstruct the original positive argument.

theorem FloatLib.Numerics.Enclosure.contains_logSeries (x : ℚ) (degree : ℕ) (hx : 0 < x) : (logSeries x degree).Contains (Real.log ↑x)

The rational series encloses the exact logarithm of every positive argument.

theorem FloatLib.Numerics.Enclosure.div_logScale_bounds (x : ℚ) (hx : 1 ≤ x) : 1 ≤ x / 2 ^ logScale x ∧ x / 2 ^ logScale x < 2

Removing the computed power of two puts an argument at least one into [1, 2).

theorem FloatLib.Numerics.Enclosure.log_reduced_argument_bounds (x : ℚ) (hx : 1 ≤ x) : have reduced := x / 2 ^ logScale x; 0 ≤ (reduced - 1) / (reduced + 1) ∧ (reduced - 1) / (reduced + 1) < 1 / 3

The transformed series argument is uniformly small after binary reduction.

theorem FloatLib.Numerics.Enclosure.log_reduction_identity (x : ℚ) (hx : 0 < x) : Real.log ↑(x / 2 ^ logScale x) + ↑(logScale x) * Real.log 2 = Real.log ↑x

The removed power of two contributes its exact integer multiple of log 2.

theorem FloatLib.Numerics.Enclosure.contains_logLarge (x : ℚ) (degree : ℕ) (hx : 0 < x) : (logLarge x degree).Contains (Real.log ↑x)

Binary argument reduction and reconstruction preserve logarithm containment.

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

The reduced rational algorithm encloses the exact logarithm of every positive argument.