Containment for interval powers and set operations

The scalar contracts lift exact endpoint bounds through OutwardRounding. For rational decoders, the real contracts cover every real member of the input intervals. Even powers use monotonicity on absolute values, retaining the zero minimum of a zero-crossing interval.

theorem FloatLib.Numerics.Interval.contains_abs? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I K : Interval α} (h : abs? R I = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K |x|

Every successful absolute-value operation encloses the absolute value of each member.

theorem FloatLib.Numerics.Interval.contains_square? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I K : Interval α} (h : square? R I = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K (x ^ 2)

Every successful square encloses the square of each member, including across zero.

theorem FloatLib.Numerics.Interval.contains_pow? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I K : Interval α} (n : ℕ) (h : pow? R I n = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K (x ^ n)

Every successful natural-power operation encloses the corresponding power of each member.

theorem FloatLib.Numerics.Interval.contains_min? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) {I J K : Interval α} (h : min? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (min x y)

Pointwise minimum preserves containment.

theorem FloatLib.Numerics.Interval.contains_max? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) {I J K : Interval α} (h : max? R I J = some K) {x y : β} (hx : Contains R.decode I x) (hy : Contains R.decode J y) : Contains R.decode K (max x y)

Pointwise maximum preserves containment.

theorem FloatLib.Numerics.Interval.contains_inv? {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] [IsStrictOrderedRing β] (R : OutwardRounding α β) {I K : Interval α} (h : inv? R I = some K) {x : β} (hx : Contains R.decode I x) : Contains R.decode K x⁻¹

Every successful reciprocal encloses the inverse of each member of a nonzero range.

theorem FloatLib.Numerics.Interval.inv?_eq_none_of_contains_zero {α : Type u_1} {β : Type u_2} [Field β] [LinearOrder β] (R : OutwardRounding α β) {I : Interval α} (hzero : Contains R.decode I 0) : inv? R I = none

A range containing zero is rejected by reciprocal, including a zero endpoint.

theorem FloatLib.Numerics.Interval.contains_hull? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) {I J K : Interval α} (h : hull? R I J = some K) {x : β} (hx : Contains R.decode I x ∨ Contains R.decode J x) : Contains R.decode K x

A successful hull contains every member of either input interval.

theorem FloatLib.Numerics.Interval.contains_intersect? {α : Type u_1} {β : Type u_2} [LinearOrder β] (R : OutwardRounding α β) {I J K : Interval α} (h : intersect? R I J = some K) {x : β} (hx : Contains R.decode I x) (hy : Contains R.decode J x) : Contains R.decode K x

A successful intersection contains every common member of the input intervals.

theorem FloatLib.Numerics.Interval.containsReal_abs? {α : Type u_1} (R : OutwardRounding α ℚ) {I K : Interval α} (h : abs? R I = some K) {x : ℝ} (hx : ContainsReal R.decode I x) : ContainsReal R.decode K |x|

Rational endpoint absolute value encloses absolute values of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_square? {α : Type u_1} (R : OutwardRounding α ℚ) {I K : Interval α} (h : square? R I = some K) {x : ℝ} (hx : ContainsReal R.decode I x) : ContainsReal R.decode K (x ^ 2)

Rational endpoint squaring encloses squares of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_pow? {α : Type u_1} (R : OutwardRounding α ℚ) {I K : Interval α} (n : ℕ) (h : pow? R I n = some K) {x : ℝ} (hx : ContainsReal R.decode I x) : ContainsReal R.decode K (x ^ n)

Rational endpoint powers enclose natural powers of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_min? {α : Type u_1} (R : OutwardRounding α ℚ) {I J K : Interval α} (h : min? R I J = some K) {x y : ℝ} (hx : ContainsReal R.decode I x) (hy : ContainsReal R.decode J y) : ContainsReal R.decode K (min x y)

Rational endpoint minimum encloses minima of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_max? {α : Type u_1} (R : OutwardRounding α ℚ) {I J K : Interval α} (h : max? R I J = some K) {x y : ℝ} (hx : ContainsReal R.decode I x) (hy : ContainsReal R.decode J y) : ContainsReal R.decode K (max x y)

Rational endpoint maximum encloses maxima of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_inv? {α : Type u_1} (R : OutwardRounding α ℚ) {I K : Interval α} (h : inv? R I = some K) {x : ℝ} (hx : ContainsReal R.decode I x) : ContainsReal R.decode K x⁻¹

Rational endpoint reciprocal encloses inverses of arbitrary real members.

theorem FloatLib.Numerics.Interval.containsReal_hull? {α : Type u_1} (R : OutwardRounding α ℚ) {I J K : Interval α} (h : hull? R I J = some K) {x : ℝ} (hx : ContainsReal R.decode I x ∨ ContainsReal R.decode J x) : ContainsReal R.decode K x

The hull contains every real member of either input interval.

theorem FloatLib.Numerics.Interval.containsReal_intersect? {α : Type u_1} (R : OutwardRounding α ℚ) {I J K : Interval α} (h : intersect? R I J = some K) {x : ℝ} (hx : ContainsReal R.decode I x) (hy : ContainsReal R.decode J x) : ContainsReal R.decode K x

The intersection contains every common real member of the input intervals.