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 = 0 → x = 0) ∧ (0 < y → x < 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

• LO.Arith.log a = Classical.choose! ⋯

@[simp]

theorem LO.Arith.log_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.log 0 = 0

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) : LO.Arith.log y < y

@[simp]

theorem LO.Arith.log_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : LO.Arith.log a ≤ a

theorem LO.Arith.log_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} : x = LO.Arith.log y ↔ (y = 0 → x = 0) ∧ (0 < y → x < y ∧ ∃ y' ≤ y, LO.Arith.Exponential x y' ∧ y < 2 * y')

def LO.FirstOrder.Arith.logDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.log_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₁ LO.Arith.log via LO.FirstOrder.Arith.logDef

@[simp]

theorem LO.Arith.log_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.logDef) ↔ v 0 = LO.Arith.log (v 1)

instance LO.Arith.log_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₁ LO.Arith.log

Equations

• ⋯ = ⋯

instance LO.Arith.instBounded₁Log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.FirstOrder.Arith.Bounded₁ LO.Arith.log

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') : LO.Arith.log y = x

@[simp]

theorem LO.Arith.log_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.log 1 = 0

@[simp]

theorem LO.Arith.log_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.log 2 = 1

theorem LO.Arith.log_two_mul_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) : LO.Arith.log (2 * y) = LO.Arith.log y + 1

theorem LO.Arith.log_two_mul_add_one_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {y : V} (pos : 0 < y) : LO.Arith.log (2 * y + 1) = LO.Arith.log y + 1

theorem LO.Arith.Exponential.log_eq_of_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (H : LO.Arith.Exponential x y) : LO.Arith.log y = x

theorem LO.Arith.exponential_of_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {p : V} (pp : LO.Arith.Pow2 p) : LO.Arith.Exponential (LO.Arith.log p) p

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) : LO.Arith.log (a * p + b) = LO.Arith.log a + LO.Arith.log 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) : LO.Arith.log (a * p) = LO.Arith.log a + LO.Arith.log p

theorem LO.Arith.log_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a ≤ b) : LO.Arith.log a ≤ LO.Arith.log b

def LO.Arith.binaryLength {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : V

Equations

• LO.Arith.binaryLength a = if 0 < a then LO.Arith.log a + 1 else 0

def LO.Arith.instLength {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : Length V

Equations

• LO.Arith.instLength = { length := LO.Arith.binaryLength }

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

@[simp]

theorem LO.Arith.length_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : ‖0‖ = 0

theorem LO.Arith.length_of_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (pos : 0 < a) : ‖a‖ = LO.Arith.log a + 1

@[simp]

theorem LO.Arith.length_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : ‖a‖ ≤ a

theorem LO.Arith.length_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {i : V} {a : V} : i = ‖a‖ ↔ (0 < a → ∃ k ≤ a, k = LO.Arith.log a ∧ i = k + 1) ∧ (a = 0 → i = 0)

def LO.FirstOrder.Arith.lengthDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.length_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₁ fun (x : V) => ‖x‖ via LO.FirstOrder.Arith.lengthDef

@[simp]

theorem LO.Arith.length_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.lengthDef) ↔ v 0 = ‖v 1‖

instance LO.Arith.length_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₁ fun (x : V) => ‖x‖

Equations

• ⋯ = ⋯

instance LO.Arith.instBounded₁Length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.FirstOrder.Arith.Bounded₁ fun (x : V) => ‖x‖

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.length_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : ‖1‖ = 1

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_two_mul_add_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : ‖2 * a + 1‖ = ‖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) : ‖a * p + b‖ = ‖a‖ + LO.Arith.log 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) : ‖a * p‖ = ‖a‖ + LO.Arith.log p

theorem LO.Arith.length_monotone {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : a ≤ b) : ‖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‖) : a ≤ LO.Arith.log 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_exponential_log_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : LO.Arith.Exponential (LO.Arith.log a) b) : a < 2 * b

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) : y ≤ a ↔ x ≤ LO.Arith.log 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) : a < y ↔ LO.Arith.log a < x

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 < ‖a‖ → y ≤ a

theorem LO.Arith.Exponential.le_log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (H : LO.Arith.Exponential x y) : x ≤ LO.Arith.log y

theorem LO.Arith.Exponential.lt_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {x : V} {y : V} (H : LO.Arith.Exponential x y) : x < ‖y‖

theorem LO.Arith.lt_exponential_length {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {b : V} (h : LO.Arith.Exponential ‖a‖ b) : a < b

theorem LO.Arith.sq_len_le_three_mul {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : ‖a‖ ^ 2 ≤ 3 * 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 < ‖a‖ → LO.Arith.Exponential x y) ∧ (‖a‖ ≤ x → y = 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

• LO.Arith.bexp a x = Classical.choose! ⋯

theorem LO.Arith.exp_bexp_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : LO.Arith.Exponential x (LO.Arith.bexp a x)

theorem LO.Arith.bexp_eq_zero_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : ‖a‖ ≤ x) : LO.Arith.bexp a x = 0

@[simp]

theorem LO.Arith.bexp_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (x : V) : LO.Arith.bexp 0 x = 0

@[simp]

theorem LO.Arith.exp_bexp_of_lt_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} : LO.Arith.Exponential x (LO.Arith.bexp a x) ↔ x < ‖a‖

@[simp]

theorem LO.Arith.bexp_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (x : V) : LO.Arith.bexp a x ≤ a

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 ↔ ∃ l ≤ a, l = ‖a‖ ∧ (x < l → LO.Arith.Exponential x y) ∧ (l ≤ x → y = 0)

def LO.FirstOrder.Arith.bexpDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.bexp_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ LO.Arith.bexp via LO.FirstOrder.Arith.bexpDef

@[simp]

theorem LO.Arith.bexp_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.bexpDef) ↔ v 0 = LO.Arith.bexp (v 1) (v 2)

instance LO.Arith.bexp_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ LO.Arith.bexp

Equations

• ⋯ = ⋯

instance LO.Arith.instBounded₂Bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.FirstOrder.Arith.Bounded₂ LO.Arith.bexp

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‖) : LO.Arith.bexp a i < LO.Arith.bexp a j ↔ i < j

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‖) : LO.Arith.bexp a i ≤ LO.Arith.bexp a j ↔ i ≤ j

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'‖) : LO.Arith.bexp a i = LO.Arith.bexp a' i

@[simp]

theorem LO.Arith.bexp_pow2 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : LO.Arith.Pow2 (LO.Arith.bexp a x)

@[simp]

theorem LO.Arith.lt_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : x < LO.Arith.bexp a x

@[simp]

theorem LO.Arith.bexp_pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : 0 < LO.Arith.bexp a x

theorem LO.Arith.lt_bexp_len {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : ‖x‖ < ‖a‖) : x < LO.Arith.bexp a ‖x‖

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) : LO.Arith.bexp a x = y

theorem LO.Arith.log_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : LO.Arith.log (LO.Arith.bexp a x) = x

theorem LO.Arith.len_bexp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {x : V} (h : x < ‖a‖) : ‖LO.Arith.bexp a x‖ = x + 1

@[simp]

theorem LO.Arith.bexp_zero_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.Arith.bexp 0 0 = 0

@[simp]

theorem LO.Arith.bexp_pos_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} (h : 0 < a) : LO.Arith.bexp a 0 = 1

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'‖) : LO.Arith.bexp a (2 * x) = LO.Arith.bexp a' x ^ 2

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

• LO.Arith.fbit a i = a / LO.Arith.bexp a i % 2

@[simp]

theorem LO.Arith.fbit_lt_two {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) : LO.Arith.fbit a i < 2

@[simp]

theorem LO.Arith.fbit_le_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) (i : V) : LO.Arith.fbit a i ≤ 1

theorem LO.Arith.fbit_eq_one_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} : LO.Arith.fbit a i = 1 ↔ LO.Arith.LenBit (LO.Arith.bexp a i) a

theorem LO.Arith.fbit_eq_zero_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} : LO.Arith.fbit a i = 0 ↔ ¬LO.Arith.LenBit (LO.Arith.bexp a i) a

theorem LO.Arith.fbit_eq_zero_of_le {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] {a : V} {i : V} (hi : ‖a‖ ≤ i) : LO.Arith.fbit a i = 0

def LO.FirstOrder.Arith.fbitDef : 𝚺₀.Semisentence 3

Equations

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

theorem LO.Arith.fbit_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ LO.Arith.fbit via LO.FirstOrder.Arith.fbitDef

@[simp]

theorem LO.Arith.fbit_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.fbitDef) ↔ v 0 = LO.Arith.fbit (v 1) (v 2)

instance LO.Arith.fbit_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Function₂ LO.Arith.fbit

Equations

• ⋯ = ⋯

instance LO.Arith.instBounded₂Fbit {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] : LO.FirstOrder.Arith.Bounded₂ LO.Arith.fbit

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.fbit_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (i : V) : LO.Arith.fbit 0 i = 0

@[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]

theorem LO.Arith.fbit_two_mul_zero_eq_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : LO.Arith.fbit (2 * a) 0 = 0

@[simp]

theorem LO.Arith.fbit_two_mul_add_one_zero_eq_one {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₀] (a : V) : LO.Arith.fbit (2 * a + 1) 0 = 1

@[simp]

theorem LO.Arith.log_exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : LO.Arith.log (exp a) = a

theorem LO.Arith.exp_log_le_self {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) : exp LO.Arith.log a ≤ a

theorem LO.Arith.lt_two_mul_exponential_log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) : a < 2 * exp LO.Arith.log a

@[simp]

theorem LO.Arith.length_exponential {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (a : V) : ‖exp a‖ = a + 1

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) : LO.Arith.log (a * exp i + b) = LO.Arith.log a + i

theorem LO.Arith.log_mul_exp {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {a : V} (pos : 0 < a) (i : V) : LO.Arith.log (a * exp i) = LO.Arith.log a + i

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) : ‖a * exp i‖ = ‖a‖ + i

theorem LO.Arith.exp_le_iff_le_log {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {a : V} (pos : 0 < a) : exp i ≤ a ↔ i ≤ LO.Arith.log a