Nat.pow_le_of_le_log
theorem Nat.pow_le_of_le_log : ∀ {b x y : ℕ}, y ≠ 0 → x ≤ b.log y → b ^ x ≤ y
The theorem `Nat.pow_le_of_le_log` states that for any natural numbers `b`, `x`, and `y`, if `y` is not equal to zero and `x` is less than or equal to the logarithm of `y` in base `b` (i.e., `x ≤ Nat.log b y`), then `b` raised to the power `x` is less than or equal to `y` (i.e., `b ^ x ≤ y`). In mathematical terms, for $b, x, y \in \mathbb{N}$ with $y \neq 0$ and $x \leq \log_b y$, we have $b^x \leq y$.
More concisely: For any natural numbers $b$, $x$, and $y$ with $y \neq 0$ and $x \leq \log_b y$, we have $b^x \leq y$.
|
Nat.log_eq_iff
theorem Nat.log_eq_iff : ∀ {b m n : ℕ}, m ≠ 0 ∨ 1 < b ∧ n ≠ 0 → (b.log n = m ↔ b ^ m ≤ n ∧ n < b ^ (m + 1))
The theorem `Nat.log_eq_iff` states that for any natural numbers `b`, `m`, and `n`, given that `m` is not zero or `b` is greater than 1 and `n` is not zero, the logarithm of `n` in base `b` is equal to `m` if and only if `b` to the power of `m` is less than or equal to `n` and `n` is less than `b` to the power of `m + 1`. This defines the conditions under which the logarithm function in Lean 4 yields a certain value.
More concisely: For natural numbers `b`, `m`, and `n`, `log_b n = m` if and only if `b^m <= n` and `n < b^(m+1)`.
|
Nat.log_pos
theorem Nat.log_pos : ∀ {b n : ℕ}, 1 < b → b ≤ n → 0 < b.log n
The theorem `Nat.log_pos` states that for any natural numbers `b` and `n`, if `b` is greater than 1 and `b` is less than or equal to `n`, then the logarithm of `n` in base `b` (denoted as `Nat.log b n`) is always greater than 0. In other words, the logarithm of a natural number `n` in a base `b` that is greater than 1 and less than or equal to `n`, is a positive integer.
More concisely: For any natural numbers `b` greater than 1 and `n` such that `b` is less than or equal to `n`, `Nat.log b n` is a positive integer.
|
Nat.clog_of_left_le_one
theorem Nat.clog_of_left_le_one : ∀ {b : ℕ}, b ≤ 1 → ∀ (n : ℕ), b.clog n = 0
The theorem `Nat.clog_of_left_le_one` asserts that for any natural number `b` and `n`, if `b` is less than or equal to `1`, then the upper logarithm of `n` in base `b`, denoted here as `Nat.clog b n`, is equal to `0`. In other words, if the base of the logarithm is `1` or less, then the logarithm is `0`, regardless of the number for which the logarithm is taken.
More concisely: For any natural number `n`, `Nat.clog 1 le n` implies `Nat.clog 1 n = 0`.
|
Nat.clog_of_right_le_one
theorem Nat.clog_of_right_le_one : ∀ {n : ℕ}, n ≤ 1 → ∀ (b : ℕ), b.clog n = 0
The theorem `Nat.clog_of_right_le_one` states that for any natural number `n` and `b`, if `n` is less than or equal to 1, then the ceiling logarithm of `n` in base `b` is equal to 0. This is consistent with the definition of the ceiling logarithm, as any number raised to the power of 0 is 1, and if `n` is less or equal to 1, the smallest power of `b` that is greater than or equal to `n` is indeed zero.
More concisely: For all natural numbers `n` and base `b`, if `n` is less than or equal to 1, then the ceiling logarithm of `n` in base `b` equals 0.
|
Nat.le_pow_clog
theorem Nat.le_pow_clog : ∀ {b : ℕ}, 1 < b → ∀ (x : ℕ), x ≤ b ^ b.clog x
The theorem `Nat.le_pow_clog` states that for any natural number `b` greater than 1 and any natural number `x`, `x` is less than or equal to `b` raised to the power of the `clog` of `x` in base `b`. Here, `Nat.clog b x` represents the smallest natural number `k` such that `x` is less than or equal to `b` raised to the power `k`. This essentially captures the notion of an upper logarithm in base `b`.
More concisely: For all natural numbers `b` greater than 1 and `x`, `x` is less than or equal to `b` raised to the power of the logarithm base `b` of `x`.
|
Nat.le_pow_iff_clog_le
theorem Nat.le_pow_iff_clog_le : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, x ≤ b ^ y ↔ b.clog x ≤ y
The theorem `Nat.le_pow_iff_clog_le` states that for any given natural numbers `b`, `x`, and `y`, where `b` is greater than 1, the condition `x` being less than or equal to `b` raised to the power `y` is equivalent to the ceiling logarithm of `x` in base `b` being less than or equal to `y`. In other words, for a given base `b` greater than 1, the ceiling logarithm function `clog b` and the power function `pow b` form a Galois connection.
More concisely: For any base \(b > 1\), \(x \leqslant b^y\) if and only if \(\lceil \log\_b x \rceil \leqslant y\).
|
Nat.log_of_lt
theorem Nat.log_of_lt : ∀ {b n : ℕ}, n < b → b.log n = 0
The theorem `Nat.log_of_lt` states that for any two natural numbers `b` and `n`, if `n` is less than `b`, then the logarithm of `n` with base `b` (`Nat.log b n`) is equal to zero. This result is intuitive since logarithms measure how many times we need to multiply the base `b` to obtain `n`, and if `n` is less than `b`, we don't need to multiply `b` at all. Therefore, the logarithm is zero.
More concisely: For all natural numbers `b` and `n`, if `n` < `b`, then `Nat.log b n` equals zero.
|
Nat.pow_le_iff_le_log
theorem Nat.pow_le_iff_le_log : ∀ {b : ℕ}, 1 < b → ∀ {x y : ℕ}, y ≠ 0 → (b ^ x ≤ y ↔ x ≤ b.log y)
The theorem `Nat.pow_le_iff_le_log` establishes a relationship between the power function `pow` and the logarithm function `log` in the realm of natural numbers. Specifically, for any natural number `b` greater than 1, and any non-zero natural numbers `x` and `y`, the condition that `b` to the power of `x` is less than or equal to `y` is equivalent to the condition that `x` is less than or equal to the logarithm base `b` of `y`. This can be seen as expressing a form of Galois connection between the `pow` and `log` operations. For detailed implications under weaker assumptions, refer to `Nat.pow_le_of_le_log` and `Nat.le_log_of_pow_le`.
More concisely: For any natural number `b` greater than 1 and non-zero natural numbers `x` and `y`, `b^x <= y` if and only if `x <= log_b y`.
|
Nat.clog_one_right
theorem Nat.clog_one_right : ∀ (b : ℕ), b.clog 1 = 0
The theorem `Nat.clog_one_right` states that for any natural number `b`, the upper logarithm of `1` in base `b` is `0`. In other words, it reveals that the smallest `k : ℕ` such that `1 ≤ b^k` is always `0`, regardless of the base `b`. This is consistent with the mathematical notion that any number to the power of `0` equals `1`.
More concisely: The theorem `Nat.clog_one_right` asserts that the upper logarithm of 1 with respect to any base is 0 in Lean.
|
Nat.log_eq_zero_iff
theorem Nat.log_eq_zero_iff : ∀ {b n : ℕ}, b.log n = 0 ↔ n < b ∨ b ≤ 1
This theorem states that for any two natural numbers `b` and `n`, the logarithm of `n` to the base `b` (denoted as `Nat.log b n` in Lean 4) equals zero if and only if `n` is less than `b` or `b` is less than or equal to one. In other words, the logarithm of a number to a specific base is zero when the number is smaller than the base or when the base is one or less.
More concisely: The logarithm of a natural number `n` to base `b` is equal to zero if and only if `n` is less than `b` or `b` is less than or equal to one.
|
Nat.le_log_of_pow_le
theorem Nat.le_log_of_pow_le : ∀ {b x y : ℕ}, 1 < b → b ^ x ≤ y → x ≤ b.log y
The theorem `Nat.le_log_of_pow_le` states that for all natural numbers `b`, `x`, and `y`, if `b` is greater than 1 and `b` to the power `x` is less than or equal to `y`, then `x` is less than or equal to the logarithm of `y` in base `b`. In mathematical notation, this can be written as: if $1 < b$ and $b^x \leq y$, then $x \leq \log_b y$. This theorem provides a condition under which the power of a base is less than or equal to a given number, and relates the power to the base logarithm of that number.
More concisely: If $1 < b$ and $b^x \leq y$, then $x \leq \log_b y$. (The logarithm base $b$ of $y$ is less than or equal to $x$.)
|
Nat.pow_log_le_self
theorem Nat.pow_log_le_self : ∀ (b : ℕ) {x : ℕ}, x ≠ 0 → b ^ b.log x ≤ x
The theorem `Nat.pow_log_le_self` states that for any natural number `b` and any non-zero natural number `x`, the `b` raised to the power of the logarithm base `b` of `x` is less than or equal to `x`. In other words, it verifies the fundamental property of logarithms that the exponent to which one number must be raised to produce another number is less than or equal to the original number when the base of the logarithm is a natural number.
More concisely: For all natural numbers x and b where b > 0, b^(log\_b x) ≤ x.
|
Nat.log_of_left_le_one
theorem Nat.log_of_left_le_one : ∀ {b : ℕ}, b ≤ 1 → ∀ (n : ℕ), b.log n = 0
The theorem `Nat.log_of_left_le_one` states that for any natural numbers `b` and `n`, if `b` is less than or equal to 1, then the logarithm of `n` in base `b` is equal to 0. In other words, this theorem says that the logarithm, in base `b`, of any natural number `n` is 0 when the base `b` is 1 or less.
More concisely: For any natural number `n`, if `b` is 1 or less, then the logarithm of `n` in base `b` equals 0.
|
Nat.log_zero_right
theorem Nat.log_zero_right : ∀ (b : ℕ), b.log 0 = 0
The theorem `Nat.log_zero_right` states that for any natural number `b`, the logarithm of `0` in base `b` is `0`. In other words, regardless of what the base `b` is, log base `b` of `0` always equals `0`.
More concisely: For all natural numbers b, log base b of 0 equals 0.
|
Nat.log_one_right
theorem Nat.log_one_right : ∀ (b : ℕ), b.log 1 = 0
This theorem, `Nat.log_one_right`, states that for any given natural number `b`, the logarithm of `1` in base `b` is always `0`. This is due to the mathematical property that any number raised to the power of `0` is `1`, including the base `b`. Thus, the largest `k : ℕ` such that `b^k ≤ 1` will always be `0` when `n` is `1`.
More concisely: The logarithm of 1 with respect to any base is equal to 0.
|