Real.logb_rpow
theorem Real.logb_rpow : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → b.logb (b ^ x) = x
The theorem `Real.logb_rpow` states that for all real numbers `b` and `x`, if `b` is greater than 0 and `b` is not equal to 1, then the logarithm base `b` of `b` raised to the power of `x` is equal to `x`. In mathematical terms, this can be written as: for all \(b, x \in \mathbb{R}\) such that \(b > 0\) and \(b \neq 1\), we have \(\log_b(b^x) = x\).
More concisely: For all real numbers `b` greater than 0 and not equal to 1, `logb (b^x) = x`.
|
Real.logb_abs
theorem Real.logb_abs : ∀ {b : ℝ} (x : ℝ), b.logb |x| = b.logb x
The theorem `Real.logb_abs` states that for any real numbers `b` and `x`, the logarithm base `b` of the absolute value of `x` is equal to the logarithm base `b` of `x`. In other words, in the definition of the real logarithm `Real.logb` we have chosen, the absolute value operation doesn't affect the result of logarithm. This is similar to saying that $\log_b |x| = \log_b x$, for all real numbers `b` and `x`.
More concisely: For all real numbers `b` and `x`, `Real.logb (Abs x) = Real.logb x`.
|
Real.logb_one
theorem Real.logb_one : ∀ {b : ℝ}, b.logb 1 = 0
This theorem states that for any real number `b`, the logarithm base `b` of `1` is equal to `0`. In standard mathematical notation, this would be written as log_b(1) = 0 for all real numbers `b`. This is a well-known property of logarithms: any number raised to the power of 0 equals 1, therefore the logarithm (the power to which the base number must be raised to produce the number being logged) of 1 in any base is always 0.
More concisely: For all real numbers b, the logarithm base b of 1 equals 0.
|
Real.logb_zero
theorem Real.logb_zero : ∀ {b : ℝ}, b.logb 0 = 0
This theorem states that for any real number `b`, the base-`b` logarithm of `0` is `0`. In other words, regardless of what real number is chosen as the base, the logarithm, in that base, of `0` will always be `0`. This fact is denoted mathematically as `log_b(0) = 0` for all real numbers `b`.
More concisely: For all real numbers `b`, `log_b(0) = 0`.
|
Real.induction_Ico_mul
theorem Real.induction_Ico_mul :
∀ {P : ℝ → Prop} (x₀ r : ℝ),
1 < r →
0 < x₀ →
(∀ x ∈ Set.Ico x₀ (r * x₀), P x) →
(∀ n ≥ 1, (∀ z ∈ Set.Ico x₀ (r ^ n * x₀), P z) → ∀ z ∈ Set.Ico (r ^ n * x₀) (r ^ (n + 1) * x₀), P z) →
∀ x ≥ x₀, P x
This theorem is an induction principle for intervals of real numbers. It states that if a property `P` holds for the left-closed right-open interval from `x₀` to `r * x₀` (denoted as `[x₀, r * x₀)`), and if whenever `P` holds for the interval `[x₀, r^n * x₀)` it also holds for the interval `[r^n * x₀, r^(n+1) * x₀)`, then `P` holds for all `x` such that `x` is greater than or equal to `x₀`. The conditions for this theorem to apply are that `1` is less than `r` and `x₀` is positive.
More concisely: If `1 < r` and `x₀ > 0`, then a property `P` holds for all `x` in the interval `[x₀, ∞)` if it holds for `[x₀, r * x₀)` and for every `n`, `P` holds for `[r^n * x₀, r^(n+1) * x₀)`.
|
Real.rpow_logb
theorem Real.rpow_logb : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → 0 < x → b ^ b.logb x = x
The theorem `Real.rpow_logb` states that for all real numbers `b` and `x`, if `b` is positive, `b` is not equal to `1`, and `x` is positive, then raising `b` to the power of the logarithm base `b` of `x` is equal to `x`. In mathematical notation, this can be written as: for all real numbers `b` and `x`, if `b > 0`, `b ≠ 1`, and `x > 0`, then `b^(log_b(x)) = x`.
More concisely: For all positive real numbers `x` and `b` not equal to 1, `b^(log_b x) = x`.
|