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

instance instReprDyadic_interval : Repr Dyadic

Equations

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

Dyadic rational basics

instance instDiv2Dyadic : Div2 Dyadic

Equations

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

instance instDiv2ZeroDyadic : Div2Zero Dyadic

theorem Dyadic.natCast_zero : ↑0 = 0

theorem Dyadic.intCast_zero : ↑0 = 0

theorem Dyadic.intCast_one : ↑1 = 1

@[simp]

theorem Dyadic.toRat_one : toRat 1 = 1

@[simp]

theorem Dyadic.toRat_zero' : zero.toRat = 0

@[simp]

theorem Dyadic.toRat_shiftRightInt {x : Dyadic} {s : ℤ} : (x >>> s).toRat = x.toRat / 2 ^ s

@[simp]

theorem Dyadic.shiftRight_natCast {x : Dyadic} {n : ℕ} : x >>> ↑n = x >>> n

@[simp]

theorem Dyadic.toRat_shiftRightNat {x : Dyadic} {n : ℕ} : (x >>> n).toRat = x.toRat / 2 ^ n

@[simp]

theorem Dyadic.toRat_div2 {x : Dyadic} : (div2 x).toRat = div2 x.toRat

theorem Dyadic.intCast_add (a b : ℤ) : ↑(a + b) = ↑a + ↑b

theorem Dyadic.intCast_add_one {s : ℤ} : ↑(s + 1) = ↑s + 1

theorem Dyadic.natCast_succ (n : ℕ) : ↑(n + 1) = ↑n + 1

theorem Dyadic.intCast_neg (n : ℤ) : ↑(-n) = -↑n

theorem Dyadic.neg_add (x y : Dyadic) : -(x + y) = -x + -y

instance instCommRingDyadic_interval : CommRing Dyadic

Equations

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

@[simp]

theorem Dyadic.monoidPow_eq_instPowNat : Monoid.toNatPow = instPowNat

@[simp]

theorem Dyadic.toRat_nonneg (x : Dyadic) : 0 ≤ x.toRat ↔ 0 ≤ x

theorem Bound.dyadic_toRat_nonneg (x : Dyadic) : 0 ≤ x → 0 ≤ x.toRat

Alias of the reverse direction of Dyadic.toRat_nonneg.

theorem Bound.ratCast_nonneg {q : ℚ} {K : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : 0 ≤ q → 0 ≤ ↑q

Alias of the reverse direction of Rat.cast_nonneg.

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

Dyadic rationals approximate any field

instance Dyadic.instApproxRing {𝕜 : Type} [Field 𝕜] : Approx Dyadic 𝕜

Equations

• Dyadic.instApproxRing = { approx := fun (x : Dyadic) (x' : 𝕜) => ↑x.toRat = x' }

theorem Dyadic.approx {𝕜 : Type} {x : Dyadic} {x' : 𝕜} [Field 𝕜] : Approx.approx x x' ↔ ↑x.toRat = x'

instance instApproxZeroDyadic {𝕜 : Type} [Field 𝕜] : ApproxZero Dyadic 𝕜

instance instApproxZeroIffDyadic {𝕜 : Type} [Field 𝕜] : ApproxZeroIff Dyadic 𝕜

instance instApproxOneDyadic {𝕜 : Type} [Field 𝕜] : ApproxOne Dyadic 𝕜

instance instApproxNegDyadic {𝕜 : Type} [Field 𝕜] : ApproxNeg Dyadic 𝕜

instance instApproxAddDyadic {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxAdd Dyadic 𝕜

instance instApproxSubDyadic {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxSub Dyadic 𝕜

instance instApproxMulDyadic {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxMul Dyadic 𝕜

instance instApproxNatCastDyadic {𝕜 : Type} [Field 𝕜] : ApproxNatCast Dyadic 𝕜

instance instApproxIntCastDyadic {𝕜 : Type} [Field 𝕜] : ApproxIntCast Dyadic 𝕜

instance instApproxDiv2Dyadic {𝕜 : Type} [Field 𝕜] [CharZero 𝕜] : ApproxDiv2 Dyadic 𝕜