Convergence through rational interval operations #
Repeated squaring preserves endpoint convergence to a nonnegative target. Together with the containment lemmas, this lets an analytic kernel reduce its argument without losing either soundness or arbitrary accuracy.
theorem
FloatLib.Numerics.RationalInterval.tendsto_squareRepeat_lo
{α : Type u_1}
{l : Filter α}
{intervals : α → RationalInterval}
{x : ℝ}
(hlo : Filter.Tendsto (fun (a : α) => ↑(intervals a).lo) l (nhds x))
(hx : 0 ≤ x)
(n : ℕ)
:
Filter.Tendsto (fun (a : α) => ↑((intervals a).squareRepeat n).lo) l (nhds (x ^ 2 ^ n))
The lower endpoints of a repeatedly squared enclosure approach the corresponding power.
theorem
FloatLib.Numerics.RationalInterval.tendsto_squareRepeat_hi
{α : Type u_1}
{l : Filter α}
{intervals : α → RationalInterval}
{x : ℝ}
(hhi : Filter.Tendsto (fun (a : α) => ↑(intervals a).hi) l (nhds x))
(n : ℕ)
:
Filter.Tendsto (fun (a : α) => ↑((intervals a).squareRepeat n).hi) l (nhds (x ^ 2 ^ n))
The upper endpoints of a repeatedly squared enclosure approach the corresponding power.