Rational enclosures for interval_dyadic_real

This file defines inclusion operations for the interval_dyadic_real inclusion family which define dyadic interval enclosures for rational numbers.

def Inclusion.IntervalDyadicReal.precParam : InclusionParamDecl

The precision of dyadic approximations, defaulting to zero.

Equations

• Inclusion.IntervalDyadicReal.precParam = { name := `prec, type := q(ℕ), defaultValue? := some q(0) }

def Inclusion.IntervalDyadicReal.rat (x : ℚ) (prec : ℕ) : Interval Dyadic

Enclose a rational number in a dyadic interval with precision prec.

Equations

• Inclusion.IntervalDyadicReal.rat x prec = Inclusion.Interval.Icc ↑(x.toDyadic ↑prec) ↑(if (x.toDyadic ↑prec).toRat = x then x.toDyadic ↑prec else x.toDyadic ↑prec + Dyadic.step ↑prec)

theorem Inclusion.IntervalDyadicReal.ratCast_mem (q : ℚ) (prec : ℕ) : ↑q ∈ rat q prec

def Inclusion.IntervalDyadicReal.ratBall (c r : ℤ) (d prec : ℕ) : Interval Dyadic

The interval [(c - r) / d, (c + r) / d], rounded outward to precision prec.

Equations

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

theorem Inclusion.IntervalDyadicReal.ratBall_mem {x : ℝ} {c r : ℤ} {d : ℕ} (hx : |x - ↑c / ↑d| ≤ ↑r / ↑d) (prec : ℕ) : x ∈ ratBall c r d prec

def Inclusion.IntervalDyadicReal.natDiv (m d prec : ℕ) : Interval Dyadic

Efficiently enclose m / d in a dyadic interval with precision prec.

Equations

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

theorem Inclusion.IntervalDyadicReal.natDiv_eq_rat (m : ℕ) {d : ℕ} (prec : ℕ) (hd : 0 < d) : natDiv m d prec = rat (mkRat (↑m) d) prec

theorem Inclusion.IntervalDyadicReal.natDiv_mem (m : ℕ) {d : ℕ} (prec : ℕ) (hd : 0 < d) : ↑m / ↑d ∈ natDiv m d prec

def Inclusion.IntervalDyadicReal.scientific (m : ℕ) (s : Bool) (e prec : ℕ) : Interval Dyadic

Enclose a scientific literal in a dyadic interval with precision prec.

Equations

• Inclusion.IntervalDyadicReal.scientific m s e prec = if s = true then Inclusion.IntervalDyadicReal.natDiv m (10 ^ e) prec else Inclusion.Interval.singleton (↑m * 10 ^ e)

theorem Inclusion.IntervalDyadicReal.scientific_mem (m : ℕ) (s : Bool) (e prec : ℕ) : OfScientific.ofScientific m s e ∈ scientific m s e prec