Real meaning of rationally computed endpoint enclosures

Rational endpoint calculations enclose arbitrary real members of an interval, not just rational samples. The rounding interface still accepts only executable rationals. Its endpoint bounds are embedded into the reals after the computation, so no real-number rounding oracle is needed.

def FloatLib.Numerics.Interval.ContainsReal {α : Type u_1} (decode : α → Option ℚ) (I : Interval α) (x : ℝ) : Prop

Interpret finite rational endpoints as a closed interval of real numbers.

@[simp]

theorem FloatLib.Numerics.Interval.containsReal_some_iff (I : Interval ℚ) (x : ℝ) : ContainsReal some I x ↔ ↑I.lo ≤ x ∧ x ≤ ↑I.hi

Rational endpoints embed directly as closed real bounds.

theorem FloatLib.Numerics.Interval.containsReal_iff_of_decode? {α : Type u_1} {decode : α → Option ℚ} {I : Interval α} {a : Interval ℚ} (ha : decode? decode I = some a) (x : ℝ) : ContainsReal decode I x ↔ ↑a.lo ≤ x ∧ x ≤ ↑a.hi

A successful finite decoder supplies the real endpoint inequalities.

theorem FloatLib.Numerics.Interval.containsReal_encloseInterval? {α : Type u_1} (R : OutwardRounding α ℚ) {a : Interval ℚ} {I : Interval α} (h : encloseInterval? R a = some I) {x : ℝ} (hx : ↑a.lo ≤ x ∧ x ≤ ↑a.hi) : ContainsReal R.decode I x

Rational outward rounding encloses every real between the exact rational bounds.

theorem FloatLib.Numerics.Interval.containsReal_liftUnary? {α : Type u_1} (R : OutwardRounding α ℚ) (f : Interval ℚ → Interval ℚ) (g : ℝ → ℝ) (hf : ∀ (a : Interval ℚ) (x : ℝ), ↑a.lo ≤ x ∧ x ≤ ↑a.hi → ↑(f a).lo ≤ g x ∧ g x ≤ ↑(f a).hi) {I K : Interval α} (h : liftUnary? R f I = some K) {x : ℝ} (hx : ContainsReal R.decode I x) : ContainsReal R.decode K (g x)

Lift a rational endpoint enclosure whose interpreted bounds enclose the desired real image.

theorem FloatLib.Numerics.Interval.containsReal_liftBinary? {α : Type u_1} (R : OutwardRounding α ℚ) (f : Interval ℚ → Interval ℚ → Interval ℚ) (g : ℝ → ℝ → ℝ) (hf : ∀ (a b : Interval ℚ) (x y : ℝ), ↑a.lo ≤ x ∧ x ≤ ↑a.hi → ↑b.lo ≤ y ∧ y ≤ ↑b.hi → ↑(f a b).lo ≤ g x y ∧ g x y ≤ ↑(f a b).hi) {I J K : Interval α} (h : liftBinary? R f I J = some K) {x y : ℝ} (hx : ContainsReal R.decode I x) (hy : ContainsReal R.decode J y) : ContainsReal R.decode K (g x y)

Lift a rational binary endpoint enclosure to arbitrary real members of its input intervals.

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

Successful negation encloses the negative of every represented real.

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

Successful rational endpoint addition encloses sums of arbitrary real members.

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

Successful rational endpoint subtraction encloses differences of arbitrary real members.

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

Successful rational four-corner multiplication encloses products of arbitrary real members.

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

Successful rational four-corner division encloses quotients of arbitrary real members.