Real.log_pos_iff
theorem Real.log_pos_iff : ∀ {x : ℝ}, 0 < x → (0 < x.log ↔ 1 < x)
This theorem states that for any real number `x`, if `x` is greater than `0`, then the real logarithm of `x` is positive if and only if `x` is greater than `1`. This establishes a connection between the positivity of logarithm values and the magnitude of their inputs in relation to `1`, given the precondition that these inputs are positive.
More concisely: For any real number `x` greater than `0`, the natural logarithm of `x` is positive if and only if `x` is greater than `1`.
|
Real.continuousAt_log
theorem Real.continuousAt_log : ∀ {x : ℝ}, x ≠ 0 → ContinuousAt Real.log x
This theorem states that the real logarithm function is continuous at any point `x` in the real numbers, given that `x` is not equal to 0. In mathematical terms, this means that for any real number `x` different from 0, the real logarithm function `log(x)` approaches the limit of `log(x₀)` when `x` approaches `x₀`. This continuity statement is a fundamental property of the logarithm function in real analysis.
More concisely: For any non-zero real number `x`, the real logarithm function is continuous at `x`.
|
Real.tendsto_log_nhdsWithin_zero
theorem Real.tendsto_log_nhdsWithin_zero : Filter.Tendsto Real.log (nhdsWithin 0 {0}ᶜ) Filter.atBot
This theorem states that the real logarithm function tends to negative infinity as its argument approaches zero from the positive side. Specifically, for any open interval of negative numbers, there exists an open interval of positive numbers centered around zero such that the logarithm of any number in this positive interval falls within the given negative interval. This captures the intuitive idea that as we take the logarithm of smaller and smaller positive numbers, we get larger and larger (in magnitude) negative numbers.
More concisely: For any open negative interval, there exists an open positive interval around 0 such that the logarithm of every number in the positive interval has logarithmic value in the given negative interval.
|
Real.log_nonpos
theorem Real.log_nonpos : ∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → x.log ≤ 0
The theorem `Real.log_nonpos` states that for all real numbers `x`, if `x` is greater than or equal to 0 and less than or equal to 1, then the logarithm of `x` (as defined by the function `Real.log`) is less than or equal to 0. This is consistent with the properties of the logarithm function in real analysis, where the logarithm of a number between 0 and 1 (exclusive) is negative.
More concisely: For all real numbers `x` with `0 ≤ x < 1`, `Real.log x ≤ 0`.
|
Real.log_neg
theorem Real.log_neg : ∀ {x : ℝ}, 0 < x → x < 1 → x.log < 0
The theorem `Real.log_neg` states that for every real number `x` that is greater than `0` and less than `1`, the real logarithm of `x` is less than `0`. In other words, it asserts that the logarithm of any real number between `0` and `1` (exclusive) is negative.
More concisely: For all real numbers `x` with `0 < x < 1`, the logarithm of `x` is negative.
|
Real.log_pow
theorem Real.log_pow : ∀ (x : ℝ) (n : ℕ), (x ^ n).log = ↑n * x.log
This theorem states that for every real number `x` and natural number `n`, the logarithm of `x` to the power of `n` is equal to `n` times the logarithm of `x`. In mathematical notation, this would be written as: $\log(x^n) = n \cdot \log(x)$. This property is essential in simplifying logarithmic expressions and is widely used in mathematical analysis and computations.
More concisely: For all real numbers x and natural numbers n, log(x^n) = n * log(x).
|
Real.log_one
theorem Real.log_one : Real.log 1 = 0
The theorem `Real.log_one` states that the logarithm of 1 in the real numbers is equal to 0. This is a standard result in mathematics, as any number raised to the power of 0 is 1, so the logarithm, being the inverse operation to exponentiation, must give 0 when applied to 1. This result holds true under the definition of the real logarithm function in Lean 4 whether 1 is considered a positive real number, or when it's equal to 0.
More concisely: The logarithm of 1 in the real numbers equals 0.
|
Real.log_neg_iff
theorem Real.log_neg_iff : ∀ {x : ℝ}, 0 < x → (x.log < 0 ↔ x < 1)
The theorem `Real.log_neg_iff` states that for any real number `x`, if `x` is greater than zero, then the logarithm of `x` is less than zero if and only if `x` is less than 1. This theorem connects the properties of the real logarithm function and the size of a real number in relation to 1.
More concisely: For any real number `x`, `Log x < 0 <-> x > 0 && x < 1`.
|
Real.exp_log_eq_abs
theorem Real.exp_log_eq_abs : ∀ {x : ℝ}, x ≠ 0 → x.log.exp = |x|
This theorem states that for any real number `x` that is not zero, applying the real exponential function to the real logarithm of `x` will yield the absolute value of `x`. In mathematical terms, for all real `x ≠ 0`, we have `exp(log(x)) = |x|`. This encapsulates the property that the exponential and logarithm functions are inverse of each other, with the absolute value involved due to the definition of real logarithm function in the negative real number territory.
More concisely: For any non-zero real number `x`, the exponential function of the logarithm of `x` equals the absolute value of `x`: `exp(log(x)) = |x|`.
|
Real.log_le_log_iff
theorem Real.log_le_log_iff : ∀ {x y : ℝ}, 0 < x → 0 < y → (x.log ≤ y.log ↔ x ≤ y)
This theorem states that for all real numbers `x` and `y` which are greater than 0, the logarithm of `x` is less than or equal to the logarithm of `y` if and only if `x` is less than or equal to `y`. This statement essentially captures the order preserving property of the logarithm function on the positive real numbers.
More concisely: For all real numbers `x` and `y` greater than 0, `log x <= log y` if and only if `x <= y`.
|
Mathlib.Analysis.SpecialFunctions.Log.Basic._auxLemma.3
theorem Mathlib.Analysis.SpecialFunctions.Log.Basic._auxLemma.3 : ∀ {x : ℝ}, (x.log = 0) = (x = 0 ∨ x = 1 ∨ x = -1)
This theorem states that for any real number 'x', the logarithm of 'x' equals to zero if and only if 'x' equals to zero, one, or negative one. This means, apart from 0, 1 and -1, the logarithm of any other real number will not be zero. This is in the context of the Real.log function in Lean 4, which is defined as the inverse of the exponential for positive numbers, the logarithm of the absolute value for negative numbers, and zero for zero.
More concisely: For any real number x, x = 0, 1, or -1 if and only if log(x) = 0.
|
Real.log_abs
theorem Real.log_abs : ∀ (x : ℝ), |x|.log = x.log
This theorem states that for every real number `x`, the real logarithm of the absolute value of `x` is equal to the real logarithm of `x` itself. In mathematical notation, this would be expressed as ∀x ∈ ℝ, log(|x|) = log(x). The theorem is applicable under the unconventional extension of the logarithm function to `(-∞, 0]` in Lean, which allows the logarithm function to retain some important properties, such as `log(x * y) = log(x) + log(y)` for all nonzero `x` and `y`, and the derivative of `log` being `1/x` away from `0`.
More concisely: The theorem asserts that for all real numbers x, the absolute value of x's logarithm is equal to x's logarithm: log(|x|) = log(x).
|
Real.log_neg_eq_log
theorem Real.log_neg_eq_log : ∀ (x : ℝ), (-x).log = x.log
This theorem states that for all real numbers `x`, the logarithm of the negative of `x` is equal to the logarithm of `x`. In mathematical terms, it expresses the property that `log(-x) = log(x)`. This is a manifestation of the way the real logarithm function is defined in Lean 4: it maps negative inputs to the logarithm of their absolute value, and thus doesn't distinguish between positive and negative arguments.
More concisely: The real logarithm function is defined such that for all real numbers `x`, `log(-x) = log(|x|)`. Therefore, `log(-x) = log(x)` since `|x|` is the absolute value of `x`.
|
Real.log_inv
theorem Real.log_inv : ∀ (x : ℝ), x⁻¹.log = -x.log
This theorem states that for every real number 'x', the logarithm of the reciprocal of 'x' is equal to the negation of the logarithm of 'x'. In other words, the logarithm of the inverse of a real number equals the negative of the logarithm of the number itself, formally written as $\log(x^{-1}) = -\log(x)$. This property is crucial in the manipulation and simplification of logarithmic expressions.
More concisely: The logarithm function satisfies the property that that $\log(x^{-1}) = -\log(x)$ for all real numbers $x$.
|
Real.log_ne_zero_of_pos_of_ne_one
theorem Real.log_ne_zero_of_pos_of_ne_one : ∀ {x : ℝ}, 0 < x → x ≠ 1 → x.log ≠ 0
This theorem states that for any real number `x`, if `x` is greater than zero and `x` is not equal to one, then the real logarithm of `x` is not equal to zero. In other words, the log of any positive real number that is not one is always non-zero.
More concisely: For any real number `x > 0` with `x ≠ 1`, the logarithm `log x` is non-zero.
|
Real.log_injOn_pos
theorem Real.log_injOn_pos : Set.InjOn Real.log (Set.Ioi 0)
This theorem states that the real logarithm function (`Real.log`) is injective (or one-to-one) on the set of all real numbers greater than zero (`Set.Ioi 0`). In other words, if we have two positive real numbers `x` and `y`, and their logarithms are equal (`Real.log x = Real.log y`), then `x` must be equal to `y`. This property is important for calculations involving the logarithmic function on the positive real numbers.
More concisely: The real logarithm function is injective on the set of positive real numbers.
|
Real.exp_log
theorem Real.exp_log : ∀ {x : ℝ}, 0 < x → x.log.exp = x
The theorem `Real.exp_log` states that for any real number `x` that is greater than zero, the exponential of the logarithm of `x` equals `x` itself. In mathematical notation, this is expressed as ∀x ∈ ℝ, x > 0 → exp(log(x)) = x. In simpler words, it states that the exponential function and the logarithm function are inverses of each other for positive real numbers.
More concisely: For all real numbers x > 0, exp(log x) = x. (The exponential function and logarithm function are inverses for positive real numbers.)
|
Real.log_zero
theorem Real.log_zero : Real.log 0 = 0
This theorem states that the real logarithm of zero is equal to zero. More specifically, when the `Real.log` function, which is defined as the real logarithm function (with a particular extension to `(-∞, 0]` to maintain the property `log(x * y) = log(x) + log(y)` for all nonzero `x` and `y` and the derivative of `log` being `1/x` away from `0`), is applied to `0`, the result is `0`.
More concisely: The real logarithm of 0 is equal to 0. (log(0) = 0)
|
Real.log_lt_log
theorem Real.log_lt_log : ∀ {x y : ℝ}, 0 < x → x < y → x.log < y.log
The theorem `Real.log_lt_log` states that for any two real numbers `x` and `y`, if `x` is positive and less than `y`, then the real logarithm of `x` is less than the real logarithm of `y`. This means that the real logarithm is a strictly increasing function on the positive real numbers.
More concisely: For all real numbers `x` and `y` with `x > 0` and `x < y`, we have `log x < log y` where `log` denotes the real logarithm function.
|
Real.le_log_iff_exp_le
theorem Real.le_log_iff_exp_le : ∀ {x y : ℝ}, 0 < y → (x ≤ y.log ↔ x.exp ≤ y)
This theorem states that for every pair of real numbers `x` and `y`, given `y` is greater than 0, `x` is less than or equal to the logarithm of `y` if and only if the exponential of `x` is less than or equal to `y`. In other words, it establishes a relationship between the exponential and logarithmic functions on the real numbers: if the exponential of a number is bounded by another positive number, then the original number is bounded by the logarithm of the second number, and vice versa.
More concisely: For all real numbers x and y with y > 0, x <= log y if and only if exp x <= y.
|
Real.log_ne_zero
theorem Real.log_ne_zero : ∀ {x : ℝ}, x.log ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
The theorem `Real.log_ne_zero` states that the real logarithm of a real number `x` is not equal to zero if and only if `x` is not equal to zero, `x` is not equal to one, and `x` is not equal to negative one. In other words, the logarithm of a number `x` will be non-zero only when `x` is any real number except 0, 1, and -1.
More concisely: The real logarithm of a non-zero real number is never equal to zero.
|
Real.log_mul
theorem Real.log_mul : ∀ {x y : ℝ}, x ≠ 0 → y ≠ 0 → (x * y).log = x.log + y.log
This theorem states that for all real numbers `x` and `y`, given that neither `x` nor `y` are zero, the logarithm of the product of `x` and `y` is equal to the sum of the logarithm of `x` and the logarithm of `y`. In other words, `log(x * y) = log(x) + log(y)` for all non-zero real numbers `x` and `y`. This property is a well-known logarithmic identity, often referred to as the product rule of logarithms.
More concisely: For all non-zero real numbers `x` and `y`, `log(x * y) = log(x) + log(y)`.
|
Real.log_div
theorem Real.log_div : ∀ {x y : ℝ}, x ≠ 0 → y ≠ 0 → (x / y).log = x.log - y.log
This theorem states that for any two non-zero real numbers `x` and `y`, the logarithm of their quotient (`x / y`) is equal to the difference of their individual logarithms (`Real.log x - Real.log y`). This follows the logarithmic property `log(a/b) = log(a) - log(b)`. This property holds true for all non-zero real numbers `x` and `y`, as dictated by the conditions `x ≠ 0` and `y ≠ 0` in the theorem.
More concisely: For any non-zero real numbers `x` and `y`, `Real.log (x / y) = Real.log x - Real.log y`.
|
Real.log_lt_log_iff
theorem Real.log_lt_log_iff : ∀ {x y : ℝ}, 0 < x → 0 < y → (x.log < y.log ↔ x < y)
This theorem states that, for any two real numbers `x` and `y` that are positive, the logarithm of `x` is less than the logarithm of `y` if and only if `x` is less than `y`. In other words, the logarithm function preserves the order of positive real numbers.
More concisely: For all positive real numbers x and y, x < y if and only if log (x) < log (y).
|
Real.continuousOn_log
theorem Real.continuousOn_log : ContinuousOn Real.log {0}ᶜ
The theorem `Real.continuousOn_log` states that the real logarithm function is continuous at all points except zero. This means that for all real numbers, with the exception of zero, the logarithm function transitions smoothly without any sudden jumps or discontinuities. This continuity is in line with the extension of the real logarithm function from negative infinity to zero, maintaining the formula `log (x * y) = log x + log y` for all nonzero `x` and `y`, and ensuring that the derivative of `log` is `1/x` away from `0`.
More concisely: The logarithm function is continuous for all real numbers except zero.
|
Real.log_le_log
theorem Real.log_le_log : ∀ {x y : ℝ}, 0 < x → x ≤ y → x.log ≤ y.log
This theorem states that for any two real numbers `x` and `y`, if `x` is positive and `x` is less than or equal to `y`, then the logarithm of `x` is less than or equal to the logarithm of `y`. In other words, the real logarithm function `Real.log` is non-decreasing for positive inputs.
More concisely: For all real numbers `x` and `y` with `x > 0`, if `x <= y`, then `Real.log x <= Real.log y`.
|
Real.log_nonneg
theorem Real.log_nonneg : ∀ {x : ℝ}, 1 ≤ x → 0 ≤ x.log
This is a theorem about the real logarithm function. It states that for all real numbers `x`, if `x` is greater than or equal to 1, then the logarithm of `x` is nonnegative. In other words, the logarithm of any real number that is 1 or more will always be a number that is 0 or greater.
More concisely: For all real numbers `x` with `x >= 1`, the logarithm of `x` is non-negative. In mathematical notation: `∀x : ℝ, x ≥ 1 → 0 ≤ log x`.
|
Real.log_pos
theorem Real.log_pos : ∀ {x : ℝ}, 1 < x → 0 < x.log
The theorem `Real.log_pos` states that for all real numbers `x`, if `x` is greater than 1, then the logarithm of `x` is greater than 0. This aligns with the properties of the logarithm function in mathematics, where log(x) increases from negative infinity to positive infinity as x increases from 0 to infinity, passing through 0 at x = 1.
More concisely: For all real numbers `x` greater than 1, `log x` is positive.
|
Real.abs_log_mul_self_lt
theorem Real.abs_log_mul_self_lt : ∀ (x : ℝ), 0 < x → x ≤ 1 → |x.log * x| < 1
This theorem states that for any real number `x` in the interval `(0, 1]`, the absolute value of the logarithm of `x` multiplied by `x` itself is strictly less than 1. In mathematical terms, it ensures that for any `x` such that `0 < x ≤ 1`, we have `|log(x) * x| < 1`.
More concisely: For any real number `x` in the interval `(0, 1]`, `|log(x) * x|` is strictly less than 1.
|
Real.log_exp
theorem Real.log_exp : ∀ (x : ℝ), x.exp.log = x
This theorem states that for any real number `x`, the logarithm of the exponential of `x` is equal to `x` itself. In mathematical terms, this is expressing the property `log(exp(x)) = x` for all real `x`. This reflects the inverse relationship between the logarithm and exponential functions in real numbers.
More concisely: The logarithm function is the inverse of the exponential function for real numbers, that is, log(exp(x)) = x for all real x.
|
Real.tendsto_log_atTop
theorem Real.tendsto_log_atTop : Filter.Tendsto Real.log Filter.atTop Filter.atTop
This theorem states that the real logarithm function tends to positive infinity as the input approaches positive infinity. In other words, as we take larger and larger positive real numbers as inputs to the logarithm function, the output of the function also grows without bound. Formally, the theorem asserts that for every set of real numbers that extends indefinitely towards positive infinity, the preimage of this set under the logarithm function also extends indefinitely towards positive infinity. This is a formal way of saying that the limit of the logarithm function is positive infinity as its argument approaches positive infinity.
More concisely: The limit of the real logarithm function is positive infinity as its argument approaches positive infinity.
|