Dyadic rationals approximate any field #

We want to do power series computations over Dyadic, where these approximate ℂ as a ring. This works because our spray series functions uses only ring operation and div2 on scalars.

Nice printing for dyadic rationals, using binary scientific notation #

source

@[instance_reducible]

instance instReprDyadic_interval :

Repr Dyadic

Equations

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

Dyadic rational basics #

source

@[instance_reducible]

instance instDiv2Dyadic :

Div2 Dyadic

Equations

instDiv2Dyadic = { div2 := fun (x : Dyadic) => x >>> 1 }

source

instance instDiv2ZeroDyadic :

Div2Zero Dyadic

source

theorem Dyadic.natCast_zero :

↑0 = 0

source

theorem Dyadic.intCast_zero :

↑0 = 0

source

theorem Dyadic.intCast_one :

↑1 = 1

source

@[simp]

theorem Dyadic.toRat_one :

toRat 1 = 1

source

@[simp]

theorem Dyadic.toRat_zero' :

zero.toRat = 0

source

theorem Dyadic.shiftRight_def (x : Dyadic) (i : ℤ) :

x >>> i = x.shiftRight i

x >>> i in terms of the underlying Dyadic.shiftRight.

source

@[simp]

theorem Dyadic.toRat_shiftRightInt {x : Dyadic} {s : ℤ} :

(x >>> s).toRat = x.toRat / 2 ^ s

source

@[simp]

theorem Dyadic.shiftRight_natCast {x : Dyadic} {n : ℕ} :

x >>> ↑n = x >>> n

source

@[simp]

theorem Dyadic.toRat_shiftRightNat {x : Dyadic} {n : ℕ} :

(x >>> n).toRat = x.toRat / 2 ^ n

source

@[simp]

theorem Dyadic.toRat_div2 {x : Dyadic} :

(div2 x).toRat = div2 x.toRat

source

theorem Dyadic.intCast_add (a b : ℤ) :

↑(a + b) = ↑a + ↑b

source

theorem Dyadic.intCast_add_one {s : ℤ} :

↑(s + 1) = ↑s + 1

source

theorem Dyadic.natCast_succ (n : ℕ) :

↑(n + 1) = ↑n + 1

source

theorem Dyadic.intCast_neg (n : ℤ) :

↑(-n) = -↑n

source

theorem Dyadic.neg_add (x y : Dyadic) :

-(x + y) = -x + -y

source

@[instance_reducible]

instance instCommRingDyadic_interval :

CommRing Dyadic

Equations

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

source

@[simp]

theorem Dyadic.toRat_nonneg (x : Dyadic) :

0 ≤ x.toRat ↔ 0 ≤ x

source

theorem Bound.dyadic_toRat_nonneg (x : Dyadic) :

0 ≤ x → 0 ≤ x.toRat

Alias of the reverse direction of Dyadic.toRat_nonneg.

source

theorem Bound.ratCast_nonneg {q : ℚ} {K : Type u_2} [Field K] [LinearOrder K] [IsStrictOrderedRing K] :

0 ≤ q → 0 ≤ ↑q

Alias of the reverse direction of Rat.cast_nonneg.

source

theorem Dyadic.div2_nonneg (x : Dyadic) (x0 : 0 ≤ x) :

0 ≤ div2 x