Documentation

Foundation.FirstOrder.Arithmetic.Exponential.Pow2

On $\mathrm{Pow2}(x)$ and $\mathrm{BitLen}(x, y)$ #

$\mathrm{Pow2}(n)$ is a property that holds iff $n = 2^i$ for some $i$.

source
def LO.FirstOrder.Arithmetic.Pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) :
Prop
Equations
Instances For
    source
    def LO.FirstOrder.Arithmetic.pow2Def :
    𝚺₀.Semisentence 1
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance LO.FirstOrder.Arithmetic.pow2_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
      𝚺₀-Predicate Pow2 via pow2Def
      source
      instance LO.FirstOrder.Arithmetic.pow2_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
      𝚺₀-Predicate Pow2
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (h : Pow2 a) :
      0 < a
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (h : Pow2 a) {r : V} (hr : r ≤ a) :
      1 < r → r ∣ a → 2 ∣ r
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.pow2_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
      Pow2 1
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.not_pow2_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
      ¬Pow2 0
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.two_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (h : Pow2 a) (lt : 1 < a) :
      2 ∣ a
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.two_dvd' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (h : Pow2 a) (lt : a ≠ 1) :
      2 ∣ a
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.of_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a b : V} (h : b ∣ a) :
      Pow2 a → Pow2 b
      source
      theorem LO.FirstOrder.Arithmetic.pow2_mul_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} :
      Pow2 (2 * a) ↔ Pow2 a
      source
      theorem LO.FirstOrder.Arithmetic.pow2_mul_four {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} :
      Pow2 (4 * a) ↔ Pow2 a
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.elim {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {p : V} :
      Pow2 p ↔ p = 1 ∨ ∃ (q : V), p = 2 * q ∧ Pow2 q
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.pow2_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
      Pow2 2
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.div_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {p : V} (h : Pow2 p) (ne : p ≠ 1) :
      Pow2 (p / 2)
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.two_mul_div_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {p : V} (h : Pow2 p) (ne : p ≠ 1) :
      2 * (p / 2) = p
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.div_two_mul_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {p : V} (h : Pow2 p) (ne : p ≠ 1) :
      p / 2 * 2 = p
      source
      theorem LO.FirstOrder.Arithmetic.Pow2.elim' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {p : V} :
      Pow2 p ↔ p = 1 ∨ 1 < p ∧ ∃ (q : V), p = 2 * q ∧ Pow2 q
      source
      def LO.FirstOrder.Arithmetic.LenBit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (i a : V) :
      Prop

      $\mathrm{LenBit} (2^i, a) \iff \text{$i$th-bit of $a$ is $1$}$.

      Equations
      Instances For
        source
        def LO.FirstOrder.Arithmetic.lenbitDef :
        𝚺₀.Semisentence 2
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          instance LO.FirstOrder.Arithmetic.lenbit_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
          𝚺₀-Relation LenBit via lenbitDef
          source
          instance LO.FirstOrder.Arithmetic.lenbit_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] :
          𝚺₀-Relation LenBit
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a : V} (h : LenBit i a) :
          i ≤ a
          source
          theorem LO.FirstOrder.Arithmetic.not_lenbit_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a : V} (h : a < i) :
          ¬LenBit i a
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.LenBit.zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) :
          ¬LenBit 0 a
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.LenBit.on_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) :
          ¬LenBit a 0
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] (a : V) :
          LenBit 1 a ↔ ¬2 ∣ a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.iff_rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a : V} :
          LenBit i a ↔ a / i % 2 = 1
          source
          theorem LO.FirstOrder.Arithmetic.not_lenbit_iff_rem {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a : V} :
          ¬LenBit i a ↔ a / i % 2 = 0
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.LenBit.self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a : V} (pos : 0 < a) :
          LenBit a a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.mod {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a k : V} (h : 2 * i ∣ k) :
          LenBit i (a % k) ↔ LenBit i a
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.LenBit.mod_two_mul_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a i : V} :
          LenBit i (a % (2 * i)) ↔ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a b : V} (h : 2 * i ∣ b) :
          LenBit i (a + b) ↔ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {i a : V} (h : a < i) :
          LenBit i (a + i)
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add_self_of_not_lenbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a i : V} (pos : 0 < i) (h : ¬LenBit i a) :
          LenBit i (a + i)
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add_self_of_lenbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a i : V} (pos : 0 < i) (h : LenBit i a) :
          ¬LenBit i (a + i)
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.sub_self_of_lenbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝗢𝗽𝗲𝗻] {a i : V} (pos : 0 < i) (h : LenBit i a) :
          ¬LenBit i (a - i)
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          Pow2 (a * b)
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.Pow2.mul_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} :
          Pow2 (a * b) ↔ Pow2 a ∧ Pow2 b
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.Pow2.sq_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} :
          Pow2 (a ^ 2) ↔ Pow2 a
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.sq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} :
          Pow2 a → Pow2 (a ^ 2)
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.dvd_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≤ b → a ∣ b
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.le_iff_dvd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≤ b ↔ a ∣ b
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.two_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (pa : Pow2 a) (ne1 : a ≠ 1) :
          2 ≤ a
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.le_iff_lt_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a ≤ b ↔ a < 2 * b
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.lt_iff_two_mul_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (ha : Pow2 a) (hb : Pow2 b) :
          a < b ↔ 2 * a ≤ b
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.sq_or_dsq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (pa : Pow2 a) :
          ∃ (b : V), a = b ^ 2 ∨ a = 2 * b ^ 2
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.sqrt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (h : Pow2 a) (hsq : (√a) ^ 2 = a) :
          Pow2 (√a)
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.Pow2.not_three {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ¬Pow2 3
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.four_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i : V} (hi : Pow2 i) (lt : 2 < i) :
          4 ≤ i
          source
          theorem LO.FirstOrder.Arithmetic.Pow2.mul_add_lt_of_mul_lt_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b p q : V} (hp : Pow2 p) (hq : Pow2 q) (h : a * p < q) (hb : b < p) (hbq : b < q) :
          a * p + b < q
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.mod_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : i < j) :
          LenBit i (a % j) ↔ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : i < j) :
          LenBit i (a + j) ↔ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.LenBit.add_pow2_iff_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : a < j) :
          LenBit i (a + j) ↔ i = j ∨ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.lenbit_iff_add_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i a : V} (hi : Pow2 i) :
          LenBit i a ↔ ∃ (k : V), ∃ r < i, a = k * (2 * i) + i + r
          source
          theorem LO.FirstOrder.Arithmetic.not_lenbit_iff_add_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i a : V} (hi : Pow2 i) :
          ¬LenBit i a ↔ ∃ (k : V), ∃ r < i, a = k * (2 * i) + r
          source
          theorem LO.FirstOrder.Arithmetic.lenbit_mul_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i j a r : V} (pi : Pow2 i) (pj : Pow2 j) (hr : r < j) :
          LenBit (i * j) (a * j + r) ↔ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.lenbit_add_pow2_iff_of_not_lenbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : ¬LenBit j a) :
          LenBit i (a + j) ↔ i = j ∨ LenBit i a
          source
          theorem LO.FirstOrder.Arithmetic.lenbit_sub_pow2_iff_of_lenbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (pi : Pow2 i) (pj : Pow2 j) (h : LenBit j a) :
          LenBit i (a - j) ↔ i ≠ j ∧ LenBit i a