Basic inclusion extensions for interval_dyadic_real

This file defines basic operations for the interval_dyadic_real inclusion family.

def Inclusion.IntervalDyadicReal.mkRealIVar : InclusionExt

Construct an inclusion variable for a real expression using a dyadic interval.

Equations

• One or more equations did not get rendered due to their size.

theorem Inclusion.IntervalDyadicReal.mem_iff_mem_map {x : ℝ} {I : Interval Dyadic} : x ∈ I ↔ x ∈ I.map Dyadic.toReal

theorem Inclusion.IntervalDyadicReal.natCast_mem (n : ℕ) : ↑n ∈ Interval.singleton ↑n

theorem Inclusion.IntervalDyadicReal.ofNat_mem (n : ℕ) : OfNat.ofNat n ∈ Interval.singleton ↑n

theorem Inclusion.IntervalDyadicReal.intCast_mem (z : ℤ) : ↑z ∈ Interval.singleton ↑z

theorem Inclusion.IntervalDyadicReal.add_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x + y ∈ I.add J

theorem Inclusion.IntervalDyadicReal.neg_mem {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) : -x ∈ I.neg

theorem Inclusion.IntervalDyadicReal.abs_mem {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) : |x| ∈ I.abs

theorem Inclusion.IntervalDyadicReal.sub_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x - y ∈ I.sub J

theorem Inclusion.IntervalDyadicReal.mul_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x * y ∈ I.mul J

theorem Inclusion.IntervalDyadicReal.pow_mem (n : ℕ) {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) : x ^ n ∈ I.pow n

theorem Inclusion.IntervalDyadicReal.le_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x ≤ y ∈ I.le J

theorem Inclusion.IntervalDyadicReal.lt_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x < y ∈ I.lt J

theorem Inclusion.IntervalDyadicReal.eq_mem {x y : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hy : y ∈ J) : x = y ∈ I.eq J

theorem Inclusion.IntervalDyadicReal.mem_Ici {a x : ℝ} {I J : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) : (x ∈ Set.Ici a) ∈ I.le J

theorem Inclusion.IntervalDyadicReal.mem_Ioi {a x : ℝ} {I J : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) : (x ∈ Set.Ioi a) ∈ I.lt J

theorem Inclusion.IntervalDyadicReal.mem_Iic {b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hb : b ∈ J) : (x ∈ Set.Iic b) ∈ I.le J

theorem Inclusion.IntervalDyadicReal.mem_Iio {b x : ℝ} {I J : Interval Dyadic} (hx : x ∈ I) (hb : b ∈ J) : (x ∈ Set.Iio b) ∈ I.lt J

theorem Inclusion.IntervalDyadicReal.mem_Icc {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) : (x ∈ Set.Icc a b) ∈ (I.le J).and (J.le K)

theorem Inclusion.IntervalDyadicReal.mem_Ico {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) : (x ∈ Set.Ico a b) ∈ (I.le J).and (J.lt K)

theorem Inclusion.IntervalDyadicReal.mem_Ioc {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) : (x ∈ Set.Ioc a b) ∈ (I.lt J).and (J.le K)

theorem Inclusion.IntervalDyadicReal.mem_Ioo {a b x : ℝ} {I J K : Interval Dyadic} (ha : a ∈ I) (hx : x ∈ J) (hb : b ∈ K) : (x ∈ Set.Ioo a b) ∈ (I.lt J).and (J.lt K)

def Inclusion.IntervalDyadicReal.roundOut (I : Interval Dyadic) (prec : ℕ) : Interval Dyadic

Round the lower endpoint of I down and the upper endpoint up, each to a multiple of 2 ^ (-prec). Infinite endpoints are left unchanged, so the result always contains I.

This drops surplus bits so that later computations don't have to carry them. For example, a large power of an interval (as in expPoint) has endpoints with very long binary expansions.

Equations

• Inclusion.IntervalDyadicReal.roundOut I prec = { lb := WithBot.map (fun (l : Dyadic) => l.roundDown ↑prec) I.lb, ub := WithTop.map (fun (u : Dyadic) => u.roundUp ↑prec) I.ub }

theorem Inclusion.IntervalDyadicReal.mem_roundOut_iff {x : ℝ} {I : Interval Dyadic} {prec : ℕ} : x ∈ roundOut I prec ↔ (∀ (J : Dyadic), I.lb = ↑J → (J.roundDown ↑prec).toReal ≤ x) ∧ ∀ (J : Dyadic), I.ub = ↑J → x ≤ (J.roundUp ↑prec).toReal

theorem Inclusion.IntervalDyadicReal.roundOut_mem {x : ℝ} {I : Interval Dyadic} (hx : x ∈ I) (prec : ℕ) : x ∈ roundOut I prec