Mathlib.Analysis.PSeries._auxLemma.10
theorem Mathlib.Analysis.PSeries._auxLemma.10 : ∀ {p : ℝ}, (Summable fun n => (↑n ^ p)⁻¹) = (1 < p)
This theorem, `Mathlib.Analysis.PSeries._auxLemma.10`, states that for any real number `p`, the function `f(n) = (n^p)^-1` is summable if and only if `p` is greater than 1. Here, 'summable' means that the infinite series sum of `f(n)` exists. In mathematical notation, this would be equivalent to saying: the series $\sum_{n=1}^{\infty} n^{-p}$ converges if and only if $p > 1$.
More concisely: The series $\sum\_{n=1}^{\infty} n^{-p}$ converges if and only if $p > 1$.
|
NNReal.summable_condensed_iff
theorem NNReal.summable_condensed_iff :
∀ {f : ℕ → NNReal},
(∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) → ((Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f)
This theorem presents the Cauchy condensation test for a series of non-negative real numbers (`NNReal`). Specifically, it states that for any function `f` from the natural numbers to the non-negative real numbers, given that `f` is monotonically non-increasing (i.e., for any natural numbers `m` and `n` where `m` is positive and less than or equal to `n`, `f(n)` is less than or equal to `f(m)`), the series formed by the function `f` is summable if and only if the series formed by the function where each term is the product of `2^k` and `f(2^k)` is summable. In other words, the summability of the function `f` can be tested by checking the summability of the condensed series `2^k * f(2^k)`.
More concisely: For a monotonically decreasing function `f` from natural numbers to non-negative real numbers, the series `∑(f(n))` is convergent if and only if the series `∑(2^k * f(2^k))` is convergent.
|
Real.tendsto_sum_range_one_div_nat_succ_atTop
theorem Real.tendsto_sum_range_one_div_nat_succ_atTop :
Filter.Tendsto (fun n => (Finset.range n).sum fun i => 1 / (↑i + 1)) Filter.atTop Filter.atTop
This theorem states the divergence of the harmonic series. It says that if you take the sum of the reciprocals of the natural numbers starting from 1 (also known as the harmonic series) up to a certain number `n` and let `n` tend to infinity, the sum will also tend to infinity. More formally, the function given by the sum from `i=0` to `n` of `1/(i+1)` tends to infinity as `n` tends to infinity.
More concisely: The limit of the sum of the reciprocals of the first `n` natural numbers as `n` approaches infinity is infinity.
|
Real.summable_one_div_nat_rpow
theorem Real.summable_one_div_nat_rpow : ∀ {p : ℝ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
This theorem is a test for the convergence of the `p-series`. It states that the real-valued series `∑' n : ℕ, 1 / n ^ p` (sum of `1 / n ^ p` for `n` in natural numbers) converges if and only if `p` is greater than `1`. Here, `Summable` is a function that checks if a given series has a sum, and `p` is a real number.
More concisely: The `p-series` `∑' n : ℕ, 1 / n ^ p` converges if and only if `p > 1`.
|
Real.summable_nat_rpow_inv
theorem Real.summable_nat_rpow_inv : ∀ {p : ℝ}, (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
The theorem `Real.summable_nat_rpow_inv` establishes a test for the convergence of the `p`-series, specifically for the series of inverse powers of natural numbers. It states that for any real number `p`, the series `∑' n : ℕ, (n ^ p)⁻¹`, in other words, the sum of the reciprocals of the `p`th powers of all natural numbers, converges if and only if `p` is greater than 1. This series is also known as the `p`-series in mathematics.
More concisely: The `p-series` of inverse natural number powers, `∑' n : ℕ, (n ^ p)⁻¹`, converges if and only if `p` is strictly greater than 1.
|
Real.summable_one_div_nat_pow
theorem Real.summable_one_div_nat_pow : ∀ {p : ℕ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
This theorem states that the `p`-series, which is a real-valued series defined as the sum over all natural numbers `n` of the quantity `1 / n ^ p`, converges if and only if `p` is greater than 1. Here, "converges" means that the series has some finite sum. We express this in Lean 4 using the `Summable` predicate.
More concisely: The `p`-series, defined as the sum of `1 / n^p` over all natural numbers `n`, converges if and only if `p` is greater than 1.
|
summable_condensed_iff_of_nonneg
theorem summable_condensed_iff_of_nonneg :
∀ {f : ℕ → ℝ},
(∀ (n : ℕ), 0 ≤ f n) →
(∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) → ((Summable fun k => 2 ^ k * f (2 ^ k)) ↔ Summable f)
The theorem `summable_condensed_iff_of_nonneg` states the Cauchy condensation test for series of nonnegative real numbers that are decreasing. Given a function `f` from natural numbers to nonnegative real numbers, if `f` is non-increasing (meaning for any two natural numbers `m` and `n` where `m` is positive and less than or equal to `n`, `f(n)` is less than or equal to `f(m)`), then the function `f` is summable (meaning it has an infinite sum) if and only if the function `k => 2^k * f(2^k)` is summable. This theorem provides a criterion for determining the convergence of certain infinite series.
More concisely: A real-valued, non-increasing function of natural numbers is summable if and only if the function defining the Cauchy condensation of the sequence is summable.
|
Real.summable_nat_pow_inv
theorem Real.summable_nat_pow_inv : ∀ {p : ℕ}, (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
This theorem is a test for the convergence of the `p`-series. It states that the real-valued series `∑' n : ℕ, (n ^ p)⁻¹`, where each term is the reciprocal of the `p`-th power of `n` (with `n` ranging over natural numbers), converges if and only if `p` is greater than 1.
More concisely: The `p`-series `∑' n : ℕ, (n ^ p)⁻¹` converges if and only if `p > 1`.
|
Real.summable_one_div_int_pow
theorem Real.summable_one_div_int_pow : ∀ {p : ℕ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p
This theorem states that a `p`-series over the set of integers `ℤ` is summable if and only if `p` is greater than 1. Here, summability refers to the series having a finite sum, and a `p`-series is a series of the form 1/n^p. In mathematical notation, this is expressed as `∑ (1/n^p) converges iff p > 1`.
More concisely: A p-series ∑ (1/n^p) over the integers ℤ converges if and only if p > 1.
|