Refinement of rational Taylor enclosures

The computed error radii tend to zero as the degree increases. These results justify arbitrary accuracy of the enclosures; deciding a rounded result also requires handling exact rounding boundaries.

theorem FloatLib.Numerics.Enclosure.expRadius_le_two_div (x : ℚ) (n : ℕ) (hx : |x| ≤ 1) (hn : 0 < n) : expRadius x n ≤ 2 / ↑n

A coarse degree-dependent exponential bound, useful for proving convergence.

theorem FloatLib.Numerics.Enclosure.tendsto_expRadius (x : ℚ) (hx : |x| ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(expRadius x (n + 1))) Filter.atTop (nhds 0)

Increasing the Taylor degree drives the exponential remainder bound to zero.

theorem FloatLib.Numerics.Enclosure.tendsto_logOneSubRadius (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(logOneSubRadius x n)) Filter.atTop (nhds 0)

The logarithm remainder is a decaying geometric sequence on its convergence interval.

theorem FloatLib.Numerics.Enclosure.tendsto_expTaylor (x : ℚ) (hx : |x| ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(expTaylor x (n + 1))) Filter.atTop (nhds (Real.exp ↑x))

The exact rational exponential polynomials converge to the real exponential.

theorem FloatLib.Numerics.Enclosure.tendsto_expSmall_lo (x : ℚ) (hx : |x| ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(expSmall x n).lo) Filter.atTop (nhds (Real.exp ↑x))

The lower small-exponential endpoints converge to the exact target.

theorem FloatLib.Numerics.Enclosure.tendsto_expSmall_hi (x : ℚ) (hx : |x| ≤ 1) : Filter.Tendsto (fun (n : ℕ) => ↑(expSmall x n).hi) Filter.atTop (nhds (Real.exp ↑x))

The upper small-exponential endpoints converge to the exact target.

theorem FloatLib.Numerics.Enclosure.tendsto_exp_lo (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(exp x n).lo) Filter.atTop (nhds (Real.exp ↑x))

After argument reduction, the lower exponential endpoints still approach the exact value.

theorem FloatLib.Numerics.Enclosure.tendsto_exp_hi (x : ℚ) : Filter.Tendsto (fun (n : ℕ) => ↑(exp x n).hi) Filter.atTop (nhds (Real.exp ↑x))

After argument reduction, the upper exponential endpoints still approach the exact value.

theorem FloatLib.Numerics.Enclosure.tendsto_neg_logOneSubTaylor (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => -↑(logOneSubTaylor x n)) Filter.atTop (nhds (Real.log (1 - ↑x)))

The signed rational logarithm polynomials converge to the exact logarithm.

theorem FloatLib.Numerics.Enclosure.tendsto_logOneSub_lo (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(logOneSub x n).lo) Filter.atTop (nhds (Real.log (1 - ↑x)))

The lower logarithm-series endpoints converge to the exact target.

theorem FloatLib.Numerics.Enclosure.tendsto_logOneSub_hi (x : ℚ) (hx : |x| < 1) : Filter.Tendsto (fun (n : ℕ) => ↑(logOneSub x n).hi) Filter.atTop (nhds (Real.log (1 - ↑x)))

The upper logarithm-series endpoints converge to the exact target.

theorem FloatLib.Numerics.Enclosure.tendsto_logSeries_lo (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(logSeries x n).lo) Filter.atTop (nhds (Real.log ↑x))

The lower logarithm endpoints converge for every positive rational argument.

theorem FloatLib.Numerics.Enclosure.tendsto_logSeries_hi (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(logSeries x n).hi) Filter.atTop (nhds (Real.log ↑x))

The upper logarithm endpoints converge for every positive rational argument.

theorem FloatLib.Numerics.Enclosure.tendsto_logLarge_lo (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(logLarge x n).lo) Filter.atTop (nhds (Real.log ↑x))

The lower endpoints retain convergence after binary logarithm reduction.

theorem FloatLib.Numerics.Enclosure.tendsto_logLarge_hi (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(logLarge x n).hi) Filter.atTop (nhds (Real.log ↑x))

The upper endpoints retain convergence after binary logarithm reduction.

theorem FloatLib.Numerics.Enclosure.tendsto_log_lo (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(log x n).lo) Filter.atTop (nhds (Real.log ↑x))

The lower reduced-logarithm endpoints converge for every positive rational argument.

theorem FloatLib.Numerics.Enclosure.tendsto_log_hi (x : ℚ) (hx : 0 < x) : Filter.Tendsto (fun (n : ℕ) => ↑(log x n).hi) Filter.atTop (nhds (Real.log ↑x))

The upper reduced-logarithm endpoints converge for every positive rational argument.