Endpoint convergence under scaling and subtraction #
Scaling by a negative rational exchanges the lower and upper endpoints. When both endpoints converge to the same real value, either sign gives the expected scaled limit. Subtraction pairs the lower endpoint of one interval with the upper endpoint of the other.
theorem
FloatLib.Numerics.RationalInterval.tendsto_scale_lo
{α : Type u_1}
{l : Filter α}
{intervals : α → RationalInterval}
{x : ℝ}
(hlo : Filter.Tendsto (fun (a : α) => ↑(intervals a).lo) l (nhds x))
(hhi : Filter.Tendsto (fun (a : α) => ↑(intervals a).hi) l (nhds x))
(factor : ℚ)
:
Filter.Tendsto (fun (a : α) => ↑((intervals a).scale factor).lo) l (nhds (↑factor * x))
The lower endpoints of scaled intervals converge to the scaled common limit.
theorem
FloatLib.Numerics.RationalInterval.tendsto_scale_hi
{α : Type u_1}
{l : Filter α}
{intervals : α → RationalInterval}
{x : ℝ}
(hlo : Filter.Tendsto (fun (a : α) => ↑(intervals a).lo) l (nhds x))
(hhi : Filter.Tendsto (fun (a : α) => ↑(intervals a).hi) l (nhds x))
(factor : ℚ)
:
Filter.Tendsto (fun (a : α) => ↑((intervals a).scale factor).hi) l (nhds (↑factor * x))
The upper endpoints of scaled intervals converge to the scaled common limit.
theorem
FloatLib.Numerics.RationalInterval.tendsto_sub_lo
{α : Type u_1}
{l : Filter α}
{left right : α → RationalInterval}
{x y : ℝ}
(hleft : Filter.Tendsto (fun (a : α) => ↑(left a).lo) l (nhds x))
(hright : Filter.Tendsto (fun (a : α) => ↑(right a).hi) l (nhds y))
:
Filter.Tendsto (fun (a : α) => ↑((left a).sub (right a)).lo) l (nhds (x - y))
Lower endpoints of interval differences converge to the difference of endpoint limits.
theorem
FloatLib.Numerics.RationalInterval.tendsto_sub_hi
{α : Type u_1}
{l : Filter α}
{left right : α → RationalInterval}
{x y : ℝ}
(hleft : Filter.Tendsto (fun (a : α) => ↑(left a).hi) l (nhds x))
(hright : Filter.Tendsto (fun (a : α) => ↑(right a).lo) l (nhds y))
:
Filter.Tendsto (fun (a : α) => ↑((left a).sub (right a)).hi) l (nhds (x - y))
Upper endpoints of interval differences converge to the difference of endpoint limits.