Documentation

Arithmetization.ISigmaZero.Exponential.Log

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

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

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