Documentation

Foundation.FirstOrder.Arithmetic.Exponential.Log

Logarithmic function #

source
theorem LO.FirstOrder.Arithmetic.log_exists_unique_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (hy : 0 < y) :
∃! x : V, x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y'
source
theorem LO.FirstOrder.Arithmetic.log_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (y : V) :
∃! x : V, (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
source
noncomputable def LO.FirstOrder.Arithmetic.log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
V
Equations
Instances For
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.log_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
    log 0 = 0
    source
    theorem LO.FirstOrder.Arithmetic.log_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (pos : 0 < y) :
    ∃ y' ≤ y, Exponential (log y) y' ∧ y < 2 * y'
    source
    theorem LO.FirstOrder.Arithmetic.log_lt_self_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (pos : 0 < y) :
    log y < y
    source
    @[simp]
    theorem LO.FirstOrder.Arithmetic.log_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
    log a ≤ a
    source
    theorem LO.FirstOrder.Arithmetic.log_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} :
    x = log y ↔ (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, Exponential x y' ∧ y < 2 * y')
    source
    def LO.FirstOrder.Arithmetic.logDef :
    𝚺₀.Semisentence 2
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance LO.FirstOrder.Arithmetic.log_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      𝚺₀-Function₁ log via logDef
      source
      instance LO.FirstOrder.Arithmetic.log_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      𝚺₀-Function₁ log
      source
      instance LO.FirstOrder.Arithmetic.instBounded₁Log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      Bounded₁ log
      source
      theorem LO.FirstOrder.Arithmetic.log_eq_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (pos : 0 < y) {y' : V} (H : Exponential x y') (hy' : y' ≤ y) (hy : y < 2 * y') :
      log y = x
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.log_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      log 1 = 0
      source
      @[simp]
      theorem LO.FirstOrder.Arithmetic.log_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
      log 2 = 1
      source
      theorem LO.FirstOrder.Arithmetic.log_two_mul_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (pos : 0 < y) :
      log (2 * y) = log y + 1
      source
      theorem LO.FirstOrder.Arithmetic.log_two_mul_add_one_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y : V} (pos : 0 < y) :
      log (2 * y + 1) = log y + 1
      source
      theorem LO.FirstOrder.Arithmetic.Exponential.log_eq_of_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (H : Exponential x y) :
      log y = x
      source
      theorem LO.FirstOrder.Arithmetic.exponential_of_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {p : V} (pp : Pow2 p) :
      Exponential (log p) p
      source
      theorem LO.FirstOrder.Arithmetic.log_mul_pow2_add_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a p b : V} (pos : 0 < a) (pp : Pow2 p) (hb : b < p) :
      log (a * p + b) = log a + log p
      source
      theorem LO.FirstOrder.Arithmetic.log_mul_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a p : V} (pos : 0 < a) (pp : Pow2 p) :
      log (a * p) = log a + log p
      source
      theorem LO.FirstOrder.Arithmetic.log_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : a ≤ b) :
      log a ≤ log b
      source
      noncomputable def LO.FirstOrder.Arithmetic.binaryLength {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
      V
      Equations
      Instances For
        source
        @[implicit_reducible]
        noncomputable def LO.FirstOrder.Arithmetic.instLength {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
        Length V
        Equations
        Instances For
          source
          theorem LO.FirstOrder.Arithmetic.length_eq_binaryLength {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
          ‖a‖ = if 0 < a then log a + 1 else 0
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.length_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
          ‖0‖ = 0
          source
          theorem LO.FirstOrder.Arithmetic.length_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (pos : 0 < a) :
          ‖a‖ = log a + 1
          source
          @[simp]
          theorem LO.FirstOrder.Arithmetic.length_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
          ‖a‖ ≤ a
          source
          theorem LO.FirstOrder.Arithmetic.length_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i a : V} :
          i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = log a ∧ i = k + 1) ∧ (a = 0 → i = 0)
          source
          def LO.FirstOrder.Arithmetic.lengthDef :
          𝚺₀.Semisentence 2
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            instance LO.FirstOrder.Arithmetic.length_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
            𝚺₀-Function₁ Length.length via lengthDef
            source
            instance LO.FirstOrder.Arithmetic.length_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
            𝚺₀-Function₁ fun (x : V) => ‖x‖
            source
            instance LO.FirstOrder.Arithmetic.instBounded₁Length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
            Bounded₁ fun (x : V) => ‖x‖
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.length_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
            ‖1‖ = 1
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.length_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (H : Exponential x y) :
            ‖y‖ = x + 1
            source
            theorem LO.FirstOrder.Arithmetic.length_two_mul_of_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (pos : 0 < a) :
            ‖2 * a‖ = ‖a‖ + 1
            source
            theorem LO.FirstOrder.Arithmetic.length_two_mul_add_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
            ‖2 * a + 1‖ = ‖a‖ + 1
            source
            theorem LO.FirstOrder.Arithmetic.length_mul_pow2_add_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a p b : V} (pos : 0 < a) (pp : Pow2 p) (hb : b < p) :
            ‖a * p + b‖ = ‖a‖ + log p
            source
            theorem LO.FirstOrder.Arithmetic.length_mul_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a p : V} (pos : 0 < a) (pp : Pow2 p) :
            ‖a * p‖ = ‖a‖ + log p
            source
            theorem LO.FirstOrder.Arithmetic.length_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : a ≤ b) :
            ‖a‖ ≤ ‖b‖
            source
            theorem LO.FirstOrder.Arithmetic.pos_of_lt_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : a < ‖b‖) :
            0 < b
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.length_pos_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} :
            0 < ‖a‖ ↔ 0 < a
            source
            @[simp]
            theorem LO.FirstOrder.Arithmetic.length_eq_zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} :
            ‖a‖ = 0 ↔ a = 0
            source
            theorem LO.FirstOrder.Arithmetic.le_log_of_lt_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : a < ‖b‖) :
            a ≤ log b
            source
            theorem LO.FirstOrder.Arithmetic.exponential_log_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (pos : 0 < a) (h : Exponential (log a) b) :
            b ≤ a
            source
            theorem LO.FirstOrder.Arithmetic.lt_exponential_log_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : Exponential (log a) b) :
            a < 2 * b
            source
            theorem LO.FirstOrder.Arithmetic.lt_exp_len_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : Exponential ‖a‖ b) :
            a < b
            source
            theorem LO.FirstOrder.Arithmetic.le_iff_le_log_of_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y a : V} (H : Exponential x y) (pos : 0 < a) :
            y ≤ a ↔ x ≤ log a
            source
            theorem LO.FirstOrder.Arithmetic.le_iff_lt_length_of_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y a : V} (H : Exponential x y) :
            y ≤ a ↔ x < ‖a‖
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.lt_iff_log_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y a : V} (H : Exponential x y) (pos : 0 < a) :
            a < y ↔ log a < x
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.lt_iff_len_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y a : V} (H : Exponential x y) :
            a < y ↔ ‖a‖ ≤ x
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.le_of_lt_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y a : V} (H : Exponential x y) :
            x < ‖a‖ → y ≤ a
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.le_log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (H : Exponential x y) :
            x ≤ log y
            source
            theorem LO.FirstOrder.Arithmetic.Exponential.lt_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x y : V} (H : Exponential x y) :
            x < ‖y‖
            source
            theorem LO.FirstOrder.Arithmetic.lt_exponential_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a b : V} (h : Exponential ‖a‖ b) :
            a < b
            source
            theorem LO.FirstOrder.Arithmetic.sq_len_le_three_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
            ‖a‖ ^ 2 ≤ 3 * a
            source
            theorem LO.FirstOrder.Arithmetic.brange_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a x : V) :
            x < ‖a‖ → ∃! y : V, Exponential x y
            source
            theorem LO.FirstOrder.Arithmetic.bexp_exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a x : V) :
            ∃! y : V, (x < ‖a‖ → Exponential x y) ∧ (‖a‖ ≤ x → y = 0)
            source
            noncomputable def LO.FirstOrder.Arithmetic.bexp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a x : V) :
            V

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

            Equations
            Instances For
              source
              theorem LO.FirstOrder.Arithmetic.exp_bexp_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
              Exponential x (bexp a x)
              source
              theorem LO.FirstOrder.Arithmetic.bexp_eq_zero_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : ‖a‖ ≤ x) :
              bexp a x = 0
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.bexp_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (x : V) :
              bexp 0 x = 0
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.exp_bexp_of_lt_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} :
              Exponential x (bexp a x) ↔ x < ‖a‖
              source
              @[simp]
              theorem LO.FirstOrder.Arithmetic.bexp_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a x : V) :
              bexp a x ≤ a
              source
              theorem LO.FirstOrder.Arithmetic.bexp_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y a x : V} :
              y = bexp a x ↔ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → Exponential x y) ∧ (l ≤ x → y = 0)
              source
              def LO.FirstOrder.Arithmetic.bexpDef :
              𝚺₀.Semisentence 3
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                instance LO.FirstOrder.Arithmetic.bexp_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                𝚺₀-Function₂ bexp via bexpDef
                source
                instance LO.FirstOrder.Arithmetic.bexp_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                𝚺₀-Function₂ bexp
                source
                instance LO.FirstOrder.Arithmetic.instBounded₂Bexp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                Bounded₂ bexp
                source
                theorem LO.FirstOrder.Arithmetic.bexp_monotone_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (hi : i < ‖a‖) (hj : j < ‖a‖) :
                bexp a i < bexp a j ↔ i < j
                source
                theorem LO.FirstOrder.Arithmetic.bexp_monotone_le_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i j : V} (hi : i < ‖a‖) (hj : j < ‖a‖) :
                bexp a i ≤ bexp a j ↔ i ≤ j
                source
                theorem LO.FirstOrder.Arithmetic.bexp_eq_of_lt_length {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {i a a' : V} (ha : i < ‖a‖) (ha' : i < ‖a'‖) :
                bexp a i = bexp a' i
                source
                @[simp]
                theorem LO.FirstOrder.Arithmetic.bexp_pow2 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
                Pow2 (bexp a x)
                source
                @[simp]
                theorem LO.FirstOrder.Arithmetic.lt_bexp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
                x < bexp a x
                source
                @[simp]
                theorem LO.FirstOrder.Arithmetic.bexp_pos {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
                0 < bexp a x
                source
                theorem LO.FirstOrder.Arithmetic.lt_bexp_len {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : ‖x‖ < ‖a‖) :
                x < bexp a ‖x‖
                source
                theorem LO.FirstOrder.Arithmetic.bexp_eq_of_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {y a x : V} (h : x < ‖a‖) (H : Exponential x y) :
                bexp a x = y
                source
                theorem LO.FirstOrder.Arithmetic.log_bexp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
                log (bexp a x) = x
                source
                theorem LO.FirstOrder.Arithmetic.len_bexp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a x : V} (h : x < ‖a‖) :
                ‖bexp a x‖ = x + 1
                source
                @[simp]
                theorem LO.FirstOrder.Arithmetic.bexp_zero_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                bexp 0 0 = 0
                source
                @[simp]
                theorem LO.FirstOrder.Arithmetic.bexp_pos_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a : V} (h : 0 < a) :
                bexp a 0 = 1
                source
                theorem LO.FirstOrder.Arithmetic.bexp_monotone {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a₁ x₁ a₂ x₂ : V} (h₁ : x₁ < ‖a₁‖) (h₂ : x₂ < ‖a₂‖) :
                bexp a₁ x₁ < bexp a₂ x₂ ↔ x₁ < x₂
                source
                theorem LO.FirstOrder.Arithmetic.bexp_monotone_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a₁ x₁ a₂ x₂ : V} (h₁ : x₁ < ‖a₁‖) (h₂ : x₂ < ‖a₂‖) :
                bexp a₁ x₁ ≤ bexp a₂ x₂ ↔ x₁ ≤ x₂
                source
                theorem LO.FirstOrder.Arithmetic.bexp_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {x₁ x₂ a : V} (h : x₁ + x₂ < ‖a‖) :
                bexp a (x₁ + x₂) = bexp a x₁ * bexp a x₂
                source
                theorem LO.FirstOrder.Arithmetic.bexp_two_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a a' x : V} (hx : 2 * x < ‖a‖) (hx' : x < ‖a'‖) :
                bexp a (2 * x) = bexp a' x ^ 2
                source
                theorem LO.FirstOrder.Arithmetic.bexp_two_mul_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i : V} :
                bexp (2 * a) (i + 1) = 2 * bexp a i
                source
                theorem LO.FirstOrder.Arithmetic.bexp_two_mul_add_one_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i : V} :
                bexp (2 * a + 1) (i + 1) = 2 * bexp a i
                source
                noncomputable def LO.FirstOrder.Arithmetic.fbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a i : V) :
                V
                Equations
                Instances For
                  source
                  @[simp]
                  theorem LO.FirstOrder.Arithmetic.fbit_lt_two {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a i : V) :
                  fbit a i < 2
                  source
                  @[simp]
                  theorem LO.FirstOrder.Arithmetic.fbit_le_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a i : V) :
                  fbit a i ≤ 1
                  source
                  theorem LO.FirstOrder.Arithmetic.fbit_eq_one_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i : V} :
                  fbit a i = 1 ↔ LenBit (bexp a i) a
                  source
                  theorem LO.FirstOrder.Arithmetic.fbit_eq_zero_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i : V} :
                  fbit a i = 0 ↔ ¬LenBit (bexp a i) a
                  source
                  theorem LO.FirstOrder.Arithmetic.fbit_eq_zero_of_le {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] {a i : V} (hi : ‖a‖ ≤ i) :
                  fbit a i = 0
                  source
                  def LO.FirstOrder.Arithmetic.fbitDef :
                  𝚺₀.Semisentence 3
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    instance LO.FirstOrder.Arithmetic.fbit_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                    𝚺₀-Function₂ fbit via fbitDef
                    source
                    instance LO.FirstOrder.Arithmetic.fbit_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                    𝚺₀-Function₂ fbit
                    source
                    instance LO.FirstOrder.Arithmetic.instBounded₂Fbit {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] :
                    Bounded₂ fbit
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.fbit_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (i : V) :
                    fbit 0 i = 0
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.fbit_mul_two_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a i : V) :
                    fbit (2 * a) (i + 1) = fbit a i
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.fbit_mul_two_add_one_mul {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a i : V) :
                    fbit (2 * a + 1) (i + 1) = fbit a i
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.fbit_two_mul_zero_eq_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
                    fbit (2 * a) 0 = 0
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.fbit_two_mul_add_one_zero_eq_one {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₀] (a : V) :
                    fbit (2 * a + 1) 0 = 1
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.log_exponential {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) :
                    log (Exp.exp a) = a
                    source
                    theorem LO.FirstOrder.Arithmetic.exp_log_le_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (pos : 0 < a) :
                    Exp.exp (log a) ≤ a
                    source
                    theorem LO.FirstOrder.Arithmetic.lt_two_mul_exponential_log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (pos : 0 < a) :
                    a < 2 * Exp.exp (log a)
                    source
                    @[simp]
                    theorem LO.FirstOrder.Arithmetic.length_exponential {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a : V) :
                    ‖Exp.exp a‖ = a + 1
                    source
                    theorem LO.FirstOrder.Arithmetic.exp_add {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) :
                    Exp.exp (a + b) = Exp.exp a * Exp.exp b
                    source
                    theorem LO.FirstOrder.Arithmetic.log_mul_exp_add_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (pos : 0 < a) (i : V) (hb : b < Exp.exp i) :
                    log (a * Exp.exp i + b) = log a + i
                    source
                    theorem LO.FirstOrder.Arithmetic.log_mul_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (pos : 0 < a) (i : V) :
                    log (a * Exp.exp i) = log a + i
                    source
                    theorem LO.FirstOrder.Arithmetic.length_mul_exp_add_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a b : V} (pos : 0 < a) (i : V) (hb : b < Exp.exp i) :
                    ‖a * Exp.exp i + b‖ = ‖a‖ + i
                    source
                    theorem LO.FirstOrder.Arithmetic.length_mul_exp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {a : V} (pos : 0 < a) (i : V) :
                    ‖a * Exp.exp i‖ = ‖a‖ + i
                    source
                    theorem LO.FirstOrder.Arithmetic.exp_le_iff_le_log {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i a : V} (pos : 0 < a) :
                    Exp.exp i ≤ a ↔ i ≤ log a