Documentation

Mathlib.Tactic.Inclusion.Extension.IntervalDyadicReal.Dyadic

Dyadic rationals #

This file provides general API for Dyadic rationals that are used in Mathlib but not available in core.

source
@[instance_reducible]
instance Inclusion.IntervalDyadicReal.instLinearOrderDyadic :
LinearOrder Dyadic
Equations
  • One or more equations did not get rendered due to their size.
source
@[instance_reducible]
instance Inclusion.IntervalDyadicReal.instAddCommGroupDyadic :
AddCommGroup Dyadic
Equations
  • One or more equations did not get rendered due to their size.
source
def Inclusion.IntervalDyadicReal.Dyadic.step (prec : ℤ) :
Dyadic

One unit on the dyadic grid with precision prec.

Equations
Instances For
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.ofIntWithPrec_one (prec : ℤ) :
    Dyadic.ofIntWithPrec 1 prec = step prec
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.zero_shiftLeft (a : ℤ) :
    0 <<< a = 0
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.zero_shiftRight (a : ℤ) :
    0 >>> a = 0
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.ofOdd_shiftLeft {k e : ℤ} {hk : k % 2 = 1} {a : ℤ} :
    Dyadic.ofOdd k e hk <<< a = Dyadic.ofOdd k (e - a) hk
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.ofOdd_shiftRight {k e : ℤ} {hk : k % 2 = 1} {a : ℤ} :
    Dyadic.ofOdd k e hk >>> a = Dyadic.ofOdd k (e + a) hk
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_natCast (d : Dyadic) (m : ℕ) :
    d <<< ↑m = d <<< m
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_natCast (d : Dyadic) (m : ℕ) :
    d >>> ↑m = d >>> m
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_add_int (d : Dyadic) (a b : ℤ) :
    d <<< (a + b) = d <<< a <<< b
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_add_nat (d : Dyadic) (m n : ℕ) :
    d <<< (m + n) = d <<< m <<< n
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_add_int (d : Dyadic) (a b : ℤ) :
    d >>> (a + b) = d >>> a >>> b
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_add_nat (d : Dyadic) (m n : ℕ) :
    d >>> (m + n) = d >>> m >>> n
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_neg (d : Dyadic) (a : ℤ) :
    d <<< (-a) = d >>> a
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_neg (d : Dyadic) (a : ℤ) :
    d >>> (-a) = d <<< a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_shiftRight (d : Dyadic) (a b : ℤ) :
    d <<< a >>> b = d <<< (a - b)
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_shiftLeft (d : Dyadic) (a b : ℤ) :
    d >>> a <<< b = d >>> (a - b)
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_shiftRight' (d : Dyadic) (a b : ℤ) :
    d <<< a >>> b = d >>> (b - a)
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_shiftLeft' (d : Dyadic) (a b : ℤ) :
    d >>> a <<< b = d <<< (b - a)
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.toRat_shiftLeft (d : Dyadic) (a : ℤ) :
    (d <<< a).toRat = d.toRat * 2 ^ a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.toRat_shiftRight (d : Dyadic) (a : ℤ) :
    (d >>> a).toRat = d.toRat * 2 ^ (-a)
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.toRat_shiftRight' (d : Dyadic) (a : ℤ) :
    (d >>> a).toRat = d.toRat / 2 ^ a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.toRat_shiftLeft_nat (d : Dyadic) (n : ℕ) :
    (d <<< n).toRat = d.toRat * 2 ^ n
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.toRat_shiftRight_nat (d : Dyadic) (n : ℕ) :
    (d >>> n).toRat = d.toRat / 2 ^ n
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_inj (x y : Dyadic) (a : ℤ) :
    x <<< a = y <<< a ↔ x = y
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_inj (x y : Dyadic) (a : ℤ) :
    x >>> a = y >>> a ↔ x = y
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftLeft_eq_zero (d : Dyadic) (a : ℤ) :
    d <<< a = 0 ↔ d = 0
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.shiftRight_eq_zero (d : Dyadic) (a : ℤ) :
    d >>> a = 0 ↔ d = 0
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.neg_shiftLeft (d : Dyadic) (a : ℤ) :
    (-d) <<< a = -d <<< a
    source
    @[simp]
    theorem Inclusion.IntervalDyadicReal.Dyadic.neg_shiftRight (d : Dyadic) (a : ℤ) :
    (-d) >>> a = -d >>> a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.add_shiftLeft_int (x y : Dyadic) (a : ℤ) :
    (x + y) <<< a = x <<< a + y <<< a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.add_shiftLeft_nat (x y : Dyadic) (m : ℕ) :
    (x + y) <<< m = x <<< m + y <<< m
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.add_shiftRight_int (x y : Dyadic) (a : ℤ) :
    (x + y) >>> a = x >>> a + y >>> a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.add_shiftRight_nat (x y : Dyadic) (m : ℕ) :
    (x + y) >>> m = x >>> m + y >>> m
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.sub_shiftLeft_int (x y : Dyadic) (a : ℤ) :
    (x - y) <<< a = x <<< a - y <<< a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.sub_shiftLeft_nat (x y : Dyadic) (m : ℕ) :
    (x - y) <<< m = x <<< m - y <<< m
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.sub_shiftRight_int (x y : Dyadic) (a : ℤ) :
    (x - y) >>> a = x >>> a - y >>> a
    source
    theorem Inclusion.IntervalDyadicReal.Dyadic.sub_shiftRight_nat (x y : Dyadic) (m : ℕ) :
    (x - y) >>> m = x >>> m - y >>> m
    source
    def Inclusion.IntervalDyadicReal.Dyadic.toReal (d : Dyadic) :
    ℝ

    Interpret a dyadic rational as a real number.

    Equations
    Instances For
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_natCast (n : ℕ) :
      toReal ↑n = ↑n
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_ofNat (n : ℕ) [n.AtLeastTwo] :
      toReal (OfNat.ofNat n) = OfNat.ofNat n
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_intCast (z : ℤ) :
      toReal ↑z = ↑z
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_add (a b : Dyadic) :
      toReal (a + b) = toReal a + toReal b
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_mul (a b : Dyadic) :
      toReal (a * b) = toReal a * toReal b
      source
      @[simp]
      theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_pow (a : Dyadic) (n : ℕ) :
      toReal (a ^ n) = toReal a ^ n
      source
      def Inclusion.IntervalDyadicReal.Dyadic.toRealAddMonoidHom :
      Dyadic →+ ℝ

      Dyadic.toReal as an additive monoid homomorphism.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_le_toReal {a b : Dyadic} :
        toReal a ≤ toReal b ↔ a ≤ b
        source
        @[simp]
        theorem Inclusion.IntervalDyadicReal.Dyadic.toReal_lt_toReal {a b : Dyadic} :
        toReal a < toReal b ↔ a < b
        source
        def Inclusion.IntervalDyadicReal.Dyadic.toRealOrderEmbedding :
        Dyadic ↪o ℝ

        Dyadic.toReal as an order embedding.

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