Real.hasSum_log_sub_log_of_abs_lt_one
theorem Real.hasSum_log_sub_log_of_abs_lt_one :
∀ {x : ℝ}, |x| < 1 → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) ((1 + x).log - (1 - x).log) := by
sorry
The theorem `Real.hasSum_log_sub_log_of_abs_lt_one` states that for any real number `x` with absolute value less than one, the power series sum of `2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1)` converges to the value of `(1 + x).log - (1 - x).log`. In other words, it provides the power series expansion of the difference between the logarithm of `1 + x` and the logarithm of `1 - x` when `|x| < 1`.
More concisely: For any real number `x` with absolute value less than 1, the power series sum of `2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1)` converges to `(1 + x).log - (1 - x).log`.
|
Real.hasSum_log_sub_log_of_abs_lt_1
theorem Real.hasSum_log_sub_log_of_abs_lt_1 :
∀ {x : ℝ}, |x| < 1 → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * x ^ (2 * k + 1)) ((1 + x).log - (1 - x).log) := by
sorry
This theorem, named `Real.hasSum_log_sub_log_of_abs_lt_1`, states that for any real number `x` with an absolute value less than 1, the power series `2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1)` has a sum equal to the difference of the natural logarithm of `1 + x` and the natural logarithm of `1 - x`. In other words, it describes the power series expansion of `log(1 + x) - log(1 - x)` for `|x| < 1`.
More concisely: For any real number `x` with an absolute value less than 1, the sum of the power series `Σ[k: ℕ] (2 * (1 / (2 * k + 1)) * x ^ (2 * k + 1))` equals `log(1 + x) - log(1 - x)`.
|
Real.hasDerivAt_log
theorem Real.hasDerivAt_log : ∀ {x : ℝ}, x ≠ 0 → HasDerivAt Real.log x⁻¹ x
The theorem `Real.hasDerivAt_log` states that for any real number `x` that is not equal to zero, the real logarithm function `Real.log` has a derivative at the point `x`, and this derivative is equal to the reciprocal of `x` (expressed as `x⁻¹` in Lean 4). In mathematical terms, if `x` is non-zero, the derivative of `log(x)` is `1/x`.
More concisely: For any non-zero real number `x`, the derivative of the logarithm function `Real.log` at `x` is equal to `1/x`.
|
Real.deriv_log'
theorem Real.deriv_log' : deriv Real.log = Inv.inv
This theorem states that the derivative of the real logarithmic function is the inverse function. In mathematical terms, if `Real.log` represents the log function and `Inv.inv` represents the inverse function, then the derivative of the log function (`deriv Real.log`) is equal to the inverse function (`Inv.inv`). This corresponds to the well-known calculus result that the derivative of ln(x) is 1/x.
More concisely: The derivative of the real logarithmic function is equal to its inverse. (i.e., `deriv Real.log = Inv.inv`)
|
Real.differentiableAt_log
theorem Real.differentiableAt_log : ∀ {x : ℝ}, x ≠ 0 → DifferentiableAt ℝ Real.log x
This theorem states that for all real numbers `x`, provided `x` is not equal to zero, the real logarithm function `Real.log` is differentiable at `x`. Differentiability, in this context, means that the function has a derivative (possibly non-unique) at that point. The derivative of a function at a point gives the slope of the tangent line to the function's graph at that point, effectively capturing the instantaneous rate of change of the function at that point. The condition `x ≠ 0` is necessary because the logarithm function is not defined at `x = 0`.
More concisely: For all non-zero real numbers `x`, the real logarithm function `Real.log` is differentiable at `x`.
|
Real.hasSum_log_one_add_inv
theorem Real.hasSum_log_one_add_inv :
∀ {a : ℝ}, 0 < a → HasSum (fun k => 2 * (1 / (2 * ↑k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)) (1 + a⁻¹).log := by
sorry
This theorem states that for every real number `a` that is greater than zero, the infinite series with terms given by `2 * (1 / (2 * k + 1)) * (1 / (2 * a + 1)) ^ (2 * k + 1)` converges (has a sum), and this sum is equivalent to the natural logarithm of `(1 + a⁻¹)`. Here, `k` is the index of the terms in the series, starting from zero and increasing by one with each term. Essentially, this theorem presents an expansion of the expression `log (1 + a⁻¹)` as a power series in terms of `1 / (2 * a + 1)`.
More concisely: For every positive real number `a`, the infinite series $\sum\_{k=0}^\infty \frac{2}{(2k+1)(2a+1)} \cdot \left(\frac{1}{2a+1}\right)^{(2k+1)}$ converges and equals $\log(1+\frac{1}{a})$.
|
Real.hasSum_pow_div_log_of_abs_lt_1
theorem Real.hasSum_pow_div_log_of_abs_lt_1 :
∀ {x : ℝ}, |x| < 1 → HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-(1 - x).log)
This theorem, `Real.hasSum_pow_div_log_of_abs_lt_1`, states that for any real number `x` with absolute value less than 1, the infinite series resulting from the function which takes an integer `n` to the nth power of `x` divided by `n+1` (considering n starting from 0), sum up to the negative logarithm of `1 - x`. This is essentially the power series expansion of the natural logarithm function around `1`.
More concisely: For any real number `x` with absolute value less than 1, the infinite series $\sum\_{n=0}^{\infty} \frac{x^n}{n+1} = -\log(1-x)$.
|
HasDerivAt.log
theorem HasDerivAt.log :
∀ {f : ℝ → ℝ} {x f' : ℝ}, HasDerivAt f f' x → f x ≠ 0 → HasDerivAt (fun y => (f y).log) (f' / f x) x
The theorem `HasDerivAt.log` states that for any real-valued function `f` from the real numbers, and for any real numbers `x` and `f'`, if the function `f` has the derivative `f'` at the point `x` and `f(x)` is nonzero, then the derivative at `x` of the function which maps `y` to the logarithm (in the extended sense defined by `Real.log`) of `f(y)` is `f' / f(x)`. This theorem provides a rule for differentiating the composition of the logarithm function with any differentiable function that does not vanish at the point of differentiation.
More concisely: If real-valued function `f` has nonzero derivative `f'` at `x`, then the logarithm function of `f(x)` has derivative `f' / f(x)` at `x`.
|
Real.tendsto_mul_log_one_plus_div_atTop
theorem Real.tendsto_mul_log_one_plus_div_atTop :
∀ (t : ℝ), Filter.Tendsto (fun x => x * (1 + t / x).log) Filter.atTop (nhds t)
The theorem `Real.tendsto_mul_log_one_plus_div_atTop` states that for any real number `t`, the function `x * log(1 + t / x)` tends towards `t` as `x` approaches positive infinity. In other words, as `x` gets larger and larger, the value of the function `x * log(1 + t / x)` gets closer and closer to `t`. This theorem is about the limit behavior of a specific function involving a logarithmic expression and a multiplication operation.
More concisely: As x approaches positive infinity, x * log(1 + t / x) tends to t.
|
Real.hasSum_pow_div_log_of_abs_lt_one
theorem Real.hasSum_pow_div_log_of_abs_lt_one :
∀ {x : ℝ}, |x| < 1 → HasSum (fun n => x ^ (n + 1) / (↑n + 1)) (-(1 - x).log)
This theorem states that for any real number `x` whose absolute value is less than one, the power series expansion of the logarithm function around `1` exists. More specifically, the sum of the series where each term is `x` to the power of `(n + 1)` divided by `(n + 1)`, for all natural numbers `n`, is equal to the negative logarithm of `(1 - x)`. This is a formal way of expressing the power series expansion for the logarithm function in the domain of `x` where absolute `x` is less than one.
More concisely: For any real number `x` with abs(x) < 1, the logarithm function around 1 has the power series expansion given by the sum of `x^(n+1)/(n+1)` for all natural numbers `n`.
|
Real.abs_log_sub_add_sum_range_le
theorem Real.abs_log_sub_add_sum_range_le :
∀ {x : ℝ},
|x| < 1 →
∀ (n : ℕ), |((Finset.range n).sum fun i => x ^ (i + 1) / (↑i + 1)) + (1 - x).log| ≤ |x| ^ (n + 1) / (1 - |x|)
This theorem states that for any real number `x` with absolute value less than 1, for any natural number `n`, the absolute difference between `log(1-x)` and its Taylor series expansion up to the `n`th term is less than or equal to the expression `|x|^(n+1) / (1 - |x|)`. Here, the Taylor series expansion of `log(1-x)` up to the `n`th term is given by the sum of `x^(i + 1) / (i + 1)` for `i` in the range from `0` to `n-1`. The main significance of this bound is that it approaches `0` as `n` tends to infinity, which is a key step in deriving the series expansion of the logarithm function when `|x|` is less than 1.
More concisely: For any real number `x` with `|x| < 1`, the absolute error in approximating `log(1-x)` with its Taylor series expansion up to the `n`th term is bounded by `|x|^{n+1} / (1 - |x|)`.
|
Real.hasStrictDerivAt_log
theorem Real.hasStrictDerivAt_log : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt Real.log x⁻¹ x
This theorem states that for all real numbers `x` that are not equal to zero, the function `Real.log` (which represents the real logarithm function) has a strict derivative at the point `x` which is equal to the reciprocal of `x` (i.e., `x⁻¹`). In mathematical terms, this means the derivative of `log(x)` is `1/x` for all `x ≠ 0`. In terms of the strict differentiability definition provided, the change in `log(y)` and `log(z)` approximates to `(y - z) * f'` plus a term that goes to zero as `y, z → x`, where `f'` is `1/x`.
More concisely: The real logarithm function `Real.log` has a strict derivative equal to `1/x` for all non-zero real numbers `x`.
|