Int.lt_zpow_iff_log_lt
theorem Int.lt_zpow_iff_log_lt :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] {b : ℕ},
1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (r < ↑b ^ x ↔ Int.log b r < x)
The theorem `Int.lt_zpow_iff_log_lt` establishes a relationship between the functions `zpow b` and `Int.log b`, suggesting that they nearly form a Galois connection in the context of integer logarithms. It states that for any linearly ordered semifield `R` with a floor semiring structure, given a natural number `b` greater than 1, an integer `x`, and a positive element `r` of `R`, the inequality `r < b ^ x` holds if and only if `Int.log b r < x`. This essentially compares the value of `r` to a power of `b`, and the integer logarithm of `r` base `b` to `x`.
More concisely: For any linearly ordered semifield with a floor semiring structure and a natural number `b` greater than 1, `r < b^x` if and only if `Int.log b r < x`.
|
Int.zpow_log_le_self
theorem Int.zpow_log_le_self :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] {b : ℕ} {r : R},
1 < b → 0 < r → ↑b ^ Int.log b r ≤ r
This theorem states that for any linearly ordered semifield `R` that also forms a floor semiring, and any natural number `b` and real number `r`, if `b` is greater than 1 and `r` is positive, then the greatest power of `b` (given by the integer logarithm function `Int.log`) such that `b ^ log b r` is less than or equal to `r`. In other words, the greatest integer exponent to which `b` can be raised without exceeding `r` is given by the `Int.log` function in this context.
More concisely: For any linearly ordered semifield `R` that is also a floor semiring, and for any natural number `b` greater than 1 and positive real number `r`, the greatest integer `n` such that `b^n` is less than or equal to `r` is given by `Int.log b r`.
|
Int.log_of_one_le_right
theorem Int.log_of_one_le_right :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) {r : R},
1 ≤ r → Int.log b r = ↑(b.log ⌊r⌋₊)
The theorem `Int.log_of_one_le_right` states that for any type `R` which is a linear ordered semiring and has a floor function, and for any natural number `b` and any value `r` of type `R`, if `r` is greater than or equal to 1, then the integer logarithm of `r` in base `b` is equal to the natural logarithm of the floor of `r` in base `b`. In simpler terms, when `r` is at least 1, the maximum exponent to which you can raise `b` to get a number less than or equal to `r` is the same whether you're considering `r` as an integer or as a real number rounded down to the nearest integer.
More concisely: For any base `b` and type `R` being a linear ordered semiring with a floor function, if `R` value `r` is greater than or equal to 1, then the integer logarithm of `r` in base `b` equals the natural logarithm of the floor of `r` in base `b`.
|
Int.le_zpow_iff_clog_le
theorem Int.le_zpow_iff_clog_le :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] {b : ℕ},
1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (r ≤ ↑b ^ x ↔ Int.clog b r ≤ x)
The theorem `Int.le_zpow_iff_clog_le` establishes a relationship between the integer ceiling logarithm function `Int.clog` and the integer power function `^` (alias `zpow`), similar to a Galois connection, for any real number `r` greater than 0 and any integer `x`. Specifically, it states that for any semiring `R` which is a linearly ordered semifield and a floor semiring, and for any natural number `b` greater than 1, the real number `r` is less than or equal to `b` raised to the power of `x` if and only if the integer ceiling logarithm of `r` base `b` is less than or equal to `x`.
More concisely: For any real number $r > 0$, integer $x$, and base $b > 1$, in a semiring that is a linearly ordered semifield and a floor semiring, $r \leq b^x$ if and only if $\lceil\log_b(r)\rceil \leq x$.
|
Int.neg_log_inv_eq_clog
theorem Int.neg_log_inv_eq_clog :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) (r : R),
-Int.log b r⁻¹ = Int.clog b r
This theorem states that for any natural number `b` and any value `r` from a linear ordered semifield `R` that also forms a floor semiring, the negative logarithm base `b` of the inverse of `r` is equal to the ceiling logarithm base `b` of `r`. In simpler terms, it suggests an equivalence between the greatest power of `b` that is not greater than the inverse of `r`, and the smallest power of `b` that is not less than `r`, when the signs are flipped.
More concisely: For any natural number `b` and any element `r` in a linear ordered semigroup with floor semilattices, the ceiling logarithm base `b` of `r` equals the negative logarithm base `b` of `r^(-1)`.
|
Int.log_of_right_le_zero
theorem Int.log_of_right_le_zero :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) {r : R},
r ≤ 0 → Int.log b r = 0
The theorem `Int.log_of_right_le_zero` states that for any type `R` which is a linear ordered semifield and a floor semiring, and given a natural number `b` and a real number `r`, if `r` is less than or equal to zero, then the result of the function `Int.log` with parameters `b` and `r` is equal to zero. In other words, the greatest power of a natural number `b` such that `b` to the power of logarithm base `b` of `r` is less than or equal to `r`, is zero when `r` is less than or equal to zero.
More concisely: For any linear ordered semifield and floor semiring type R, and natural number b and real number r, if r ≤ 0 then Int.log b r = 0.
|
Int.clog_of_one_le_right
theorem Int.clog_of_one_le_right :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) {r : R},
1 ≤ r → Int.clog b r = ↑(b.clog ⌈r⌉₊)
The theorem `Int.clog_of_one_le_right` states that for any semifield `R` that is linearly ordered and a floor semiring, given a natural number `b` and a value `r` from `R` such that `r` is greater than or equal to 1, the least power of `b` such that `r` is less than or equal to `b` to the power of the logarithm of `r` with base `b` (represented by `Int.clog b r`) equals the upper logarithm of the ceiling of `r` in base `b` (represented by `Nat.clog b ⌈r⌉₊`). In other words, when `r` is at least 1, the integer logarithm function `Int.clog` behaves the same as the natural logarithm function `Nat.clog` applied to the ceiling of `r`.
More concisely: For any semifield `R` that is linearly ordered and a floor semiring, the integer logarithm `Int.clog b r` equals the upper logarithm `Nat.clog b ⌈r⌉₊` when `r` is a positive element in `R`.
|
Int.log_of_right_le_one
theorem Int.log_of_right_le_one :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) {r : R},
r ≤ 1 → Int.log b r = -↑(b.clog ⌈r⁻¹⌉₊)
The theorem `Int.log_of_right_le_one` states that for any type `R` that is a linearly ordered semiring and a floor semiring, and for any natural number `b` and value `r` of type `R`, if `r` is less than or equal to `1`, then the integer logarithm of `r` with base `b` (i.e., the greatest power of `b` such that `b` to the power of this logarithm is less than or equal to `r`) is equal to the negative of the ceiling of the reciprocal of `r`, taken to the upper logarithm in base `b` (i.e., the smallest `k` such that `r` inverse is less than or equal to `b` to the power of `k`).
More concisely: For any linearly ordered semiring and floor semiring type R, natural number b, and value r of type R, if 0 ≤ r in R, then log\_b (r) = -ceiling(1 / r)^(log\_b^(up) (1 / r)) where log\_b and ceiling are the integer logarithm and ceiling functions, respectively, with base b.
|
Int.clog_of_right_le_zero
theorem Int.clog_of_right_le_zero :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] (b : ℕ) {r : R},
r ≤ 0 → Int.clog b r = 0
This theorem states that for any type `R` that is a linearly ordered semifield and a floor semiring, and for any natural number `b` and any real number `r` from this type `R`, if `r` is less than or equal to 0, then the `Int.clog` of `b` and `r` is 0. In other words, if the real number is non-positive, then the least power of `b` that is greater than or equal to `r` is 0 since any number raised to the power 0 gives 1, which is greater than any non-positive number.
More concisely: For any linearly ordered semifield and floor semiring `R`, `Int.clog b 0 le 0 → Int.clog b R := 0`.
|
Int.zpow_lt_iff_lt_clog
theorem Int.zpow_lt_iff_lt_clog :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] {b : ℕ},
1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (↑b ^ x < r ↔ x < Int.clog b r)
The theorem `Int.zpow_lt_iff_lt_clog` states that for any linearly ordered semifield `R` that is also a floor semiring, and for any natural number `b` greater than 1, and for any integer `x` and any real number `r` greater than 0, the integer power of `b` is less than `r` if and only if `x` is less than the least power of `b` such that `r` is less than or equal to `b` to the power of `log b r`. In other words, `Int.clog b` and `zpow b` form a Galois connection with some conditions.
More concisely: For any linearly ordered semifield with floor semiring properties R, natural number b > 1, integer x, and real number r > 0, x < int(log(r) / log(b)) if and only if b^x < r.
|
Int.zpow_le_iff_le_log
theorem Int.zpow_le_iff_le_log :
∀ {R : Type u_1} [inst : LinearOrderedSemifield R] [inst_1 : FloorSemiring R] {b : ℕ},
1 < b → ∀ {x : ℤ} {r : R}, 0 < r → (↑b ^ x ≤ r ↔ x ≤ Int.log b r)
The theorem `Int.zpow_le_iff_le_log` states that for any type `R` that forms a Linear Ordered Semifield and a Floor Semifield, for any natural number `b` greater than 1, and for any integer `x` and any real number `r` greater than 0, the power of `b` raised to `x` being less than or equal to `r` is equivalent to `x` being less than or equal to the greatest power of `b` such that `b` to the power of the logarithm base `b` of `r` is less than or equal to `r`. This shows that the functions `zpow b` and `Int.log b` almost form a Galois connection.
More concisely: For any Linear Ordered Semifield and Floor Semifield type `R`, natural number `b > 1`, integer `x`, and real number `r > 0`, `b^x <= r` if and only if `x <= log_b (min 1 r)`.
|