Documentation

Arithmetization.ISigmaZero.Exponential.Log

theorem LO.Arith.log_exists_unique_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (hy : 0 < y) :
∃! x : V, x < y y'y, LO.Arith.Exponential x y' y < 2 * y'
theorem LO.Arith.log_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (y : V) :
∃! x : V, (y = 0x = 0) (0 < yx < y y'y, LO.Arith.Exponential x y' y < 2 * y')
def LO.Arith.log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) :
V
Equations
Instances For
    theorem LO.Arith.log_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) :
    y'y, LO.Arith.Exponential (LO.Arith.log y) y' y < 2 * y'
    theorem LO.Arith.log_lt_self_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) :
    @[simp]
    theorem LO.Arith.log_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} :
    x = LO.Arith.log y (y = 0x = 0) (0 < yx < y y'y, LO.Arith.Exponential x y' y < 2 * y')
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      Equations
      • =
      theorem LO.Arith.log_eq_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (pos : 0 < y) {y' : V} (H : LO.Arith.Exponential x y') (hy' : y' y) (hy : y < 2 * y') :
      theorem LO.Arith.log_two_mul_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) :
      theorem LO.Arith.log_two_mul_add_one_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) :
      theorem LO.Arith.log_mul_pow2_add_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {p : V} {b : V} (pos : 0 < a) (pp : LO.Arith.Pow2 p) (hb : b < p) :
      theorem LO.Arith.log_mul_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {p : V} (pos : 0 < a) (pp : LO.Arith.Pow2 p) :
      theorem LO.Arith.log_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a b) :
      Equations
      Instances For
        Equations
        • LO.Arith.instLength = { length := LO.Arith.binaryLength }
        Instances For
          theorem LO.Arith.length_eq_binaryLength {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) :
          a = if 0 < a then LO.Arith.log a + 1 else 0
          theorem LO.Arith.length_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (pos : 0 < a) :
          @[simp]
          theorem LO.Arith.length_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) :
          theorem LO.Arith.length_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {a : V} :
          i = a (0 < aka, k = LO.Arith.log a i = k + 1) (a = 0i = 0)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • =
            theorem LO.Arith.Exponential.length_eq {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (H : LO.Arith.Exponential x y) :
            y = x + 1
            theorem LO.Arith.length_two_mul_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (pos : 0 < a) :
            2 * a = a + 1
            theorem LO.Arith.length_mul_pow2_add_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {p : V} {b : V} (pos : 0 < a) (pp : LO.Arith.Pow2 p) (hb : b < p) :
            theorem LO.Arith.length_mul_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {p : V} (pos : 0 < a) (pp : LO.Arith.Pow2 p) :
            theorem LO.Arith.length_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a b) :
            theorem LO.Arith.pos_of_lt_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a < b) :
            0 < b
            @[simp]
            theorem LO.Arith.length_pos_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} :
            0 < a 0 < a
            @[simp]
            theorem LO.Arith.length_eq_zero_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} :
            a = 0 a = 0
            theorem LO.Arith.le_log_of_lt_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a < b) :
            theorem LO.Arith.exponential_log_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (pos : 0 < a) (h : LO.Arith.Exponential (LO.Arith.log a) b) :
            b a
            theorem LO.Arith.lt_exp_len_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : LO.Arith.Exponential a b) :
            a < b
            theorem LO.Arith.le_iff_le_log_of_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} {a : V} (H : LO.Arith.Exponential x y) (pos : 0 < a) :
            theorem LO.Arith.le_iff_lt_length_of_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} {a : V} (H : LO.Arith.Exponential x y) :
            y a x < a
            theorem LO.Arith.Exponential.lt_iff_log_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} {a : V} (H : LO.Arith.Exponential x y) (pos : 0 < a) :
            theorem LO.Arith.Exponential.lt_iff_len_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} {a : V} (H : LO.Arith.Exponential x y) :
            a < y a x
            theorem LO.Arith.Exponential.le_of_lt_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} {a : V} (H : LO.Arith.Exponential x y) :
            x < ay a
            theorem LO.Arith.brange_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (x : V) :
            x < a∃! y : V, LO.Arith.Exponential x y
            theorem LO.Arith.bexp_exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (x : V) :
            ∃! y : V, (x < aLO.Arith.Exponential x y) (a xy = 0)
            def LO.Arith.bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (x : V) :
            V

            bexp a x = exp x if x < ‖a‖; = 0 o.w.

            Equations
            Instances For
              theorem LO.Arith.bexp_eq_zero_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : a x) :
              @[simp]
              theorem LO.Arith.bexp_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) :
              @[simp]
              theorem LO.Arith.bexp_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (x : V) :
              theorem LO.Arith.bexp_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {a : V} {x : V} :
              y = LO.Arith.bexp a x la, l = a (x < lLO.Arith.Exponential x y) (l xy = 0)
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                Equations
                • =
                theorem LO.Arith.bexp_monotone_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (hi : i < a) (hj : j < a) :
                theorem LO.Arith.bexp_monotone_le_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} {j : V} (hi : i < a) (hj : j < a) :
                theorem LO.Arith.bexp_eq_of_lt_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {a : V} {a' : V} (ha : i < a) (ha' : i < a') :
                @[simp]
                theorem LO.Arith.bexp_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                @[simp]
                theorem LO.Arith.lt_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                @[simp]
                theorem LO.Arith.bexp_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                theorem LO.Arith.lt_bexp_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                theorem LO.Arith.bexp_eq_of_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} {a : V} {x : V} (h : x < a) (H : LO.Arith.Exponential x y) :
                theorem LO.Arith.log_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                theorem LO.Arith.len_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < a) :
                @[simp]
                theorem LO.Arith.bexp_pos_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (h : 0 < a) :
                theorem LO.Arith.bexp_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a₁ : V} {x₁ : V} {a₂ : V} {x₂ : V} (h₁ : x₁ < a₁) (h₂ : x₂ < a₂) :
                LO.Arith.bexp a₁ x₁ < LO.Arith.bexp a₂ x₂ x₁ < x₂
                theorem LO.Arith.bexp_monotone_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a₁ : V} {x₁ : V} {a₂ : V} {x₂ : V} (h₁ : x₁ < a₁) (h₂ : x₂ < a₂) :
                LO.Arith.bexp a₁ x₁ LO.Arith.bexp a₂ x₂ x₁ x₂
                theorem LO.Arith.bexp_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x₁ : V} {x₂ : V} {a : V} (h : x₁ + x₂ < a) :
                LO.Arith.bexp a (x₁ + x₂) = LO.Arith.bexp a x₁ * LO.Arith.bexp a x₂
                theorem LO.Arith.bexp_two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {a' : V} {x : V} (hx : 2 * x < a) (hx' : x < a') :
                theorem LO.Arith.bexp_two_mul_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} :
                LO.Arith.bexp (2 * a) (i + 1) = 2 * LO.Arith.bexp a i
                theorem LO.Arith.bexp_two_mul_add_one_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} :
                LO.Arith.bexp (2 * a + 1) (i + 1) = 2 * LO.Arith.bexp a i
                def LO.Arith.fbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) :
                V
                Equations
                Instances For
                  @[simp]
                  theorem LO.Arith.fbit_lt_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) :
                  @[simp]
                  theorem LO.Arith.fbit_le_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) :
                  theorem LO.Arith.fbit_eq_zero_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} (hi : a i) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    Equations
                    • =
                    @[simp]
                    theorem LO.Arith.fbit_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) :
                    @[simp]
                    theorem LO.Arith.fbit_mul_two_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) :
                    LO.Arith.fbit (2 * a) (i + 1) = LO.Arith.fbit a i
                    @[simp]
                    theorem LO.Arith.fbit_mul_two_add_one_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) :
                    LO.Arith.fbit (2 * a + 1) (i + 1) = LO.Arith.fbit a i
                    @[simp]
                    @[simp]
                    theorem LO.Arith.exp_log_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) :
                    @[simp]
                    theorem LO.Arith.exp_add {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) (b : V) :
                    exp (a + b) = exp a * exp b
                    theorem LO.Arith.log_mul_exp_add_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (pos : 0 < a) (i : V) (hb : b < exp i) :
                    theorem LO.Arith.log_mul_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) (i : V) :
                    theorem LO.Arith.length_mul_exp_add_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} {b : V} (pos : 0 < a) (i : V) (hb : b < exp i) :
                    a * exp i + b = a + i
                    theorem LO.Arith.length_mul_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) (i : V) :
                    theorem LO.Arith.exp_le_iff_le_log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (pos : 0 < a) :