tsum_coe_mul_geometric_of_norm_lt_one
theorem tsum_coe_mul_geometric_of_norm_lt_one :
β {π : Type u_4} [inst : NormedDivisionRing π] [inst_1 : CompleteSpace π] {r : π},
βrβ < 1 β β' (n : β), βn * r ^ n = r / (1 - r) ^ 2
This theorem states that for any value `r` from a complete normed division ring `π`, if the norm of `r` is less than 1, then the sum of the series where each term is the product of a natural number `n` and `r` raised to the power `n` is equal to `r` divided by the square of `(1 - r)`. In mathematical terms, if `βrβ < 1`, then `β' n : β, n * r ^ n = r / (1 - r) ^ 2`.
More concisely: For any `r` in a complete normed division ring with norm less than 1, the infinite series `ββ n:β, n * rβΏ` converges to `r / (1 - r)Β²`.
|
isLittleO_coe_const_pow_of_one_lt
theorem isLittleO_coe_const_pow_of_one_lt :
β {R : Type u_4} [inst : NormedRing R] {r : β}, 1 < r β Nat.cast =o[Filter.atTop] fun n => r ^ n
This theorem states that for any real number `r` greater than 1, the function that maps a natural number `n` to `n` is little-o of the function that maps `n` to `r^n` as `n` approaches infinity. In other words, in terms of growth rates as `n` goes to infinity, `n` grows significantly slower than `r^n` for any `r` greater than 1. This is expressed using the little-o notation (`=o[Filter.atTop]`), which formalizes the concept of one function growing much slower than another in the limit.
More concisely: For any real number `r` > 1, the function `fn => n` is little-o of `fr => r^n` as `n` approaches infinity.
|
tendsto_pow_const_mul_const_pow_of_abs_lt_one
theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one :
β (k : β) {r : β}, |r| < 1 β Filter.Tendsto (fun n => βn ^ k * r ^ n) Filter.atTop (nhds 0)
The theorem `tendsto_pow_const_mul_const_pow_of_abs_lt_one` states that for any natural number `k` and a real number `r` where the absolute value of `r` is less than one, the function `f(n) = n^k * r^n` tends to zero as `n` approaches infinity. In other words, the sequence `f(n)` gets arbitrarily close to zero for sufficiently large values of `n`.
More concisely: For any natural number `k` and real number `r` with absolute value `|r| < 1, the sequence `n => n^k * r^n` converges to zero as `n` approaches infinity.`
|
summable_geometric_iff_norm_lt_1
theorem summable_geometric_iff_norm_lt_1 :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, (Summable fun n => ΞΎ ^ n) β βΞΎβ < 1
The theorem `summable_geometric_iff_norm_lt_1` states that for any type `K` which is a normed division ring and any element `ΞΎ` of `K`, the geometric series $\sum_{n=0}^{\infty} \xi^{n}$ is summable if and only if the norm of `ΞΎ` is less than one. In other words, an infinite geometric series in a normed division ring converges if the absolute value of the common ratio is less than one.
More concisely: A geometric series in a normed division ring converges if and only if the norm of the common ratio is less than 1.
|
hasSum_geometric_of_abs_lt_1
theorem hasSum_geometric_of_abs_lt_1 : β {r : β}, |r| < 1 β HasSum (fun n => r ^ n) (1 - r)β»ΒΉ
This theorem, `hasSum_geometric_of_abs_lt_1`, is an alias of `hasSum_geometric_of_abs_lt_one`. It states that for any real number `r` with absolute value less than 1, the sum of the infinite geometric series `r^n` (where `n` ranges over all nonnegative integers) is equal to `(1 - r)β»ΒΉ`. In simpler terms, if you have a real number `r` that is strictly between -1 and 1, the sum of the series where each term is `r` raised to the power of the term's position, starting from zero, is equal to the reciprocal of `(1 - r)`.
More concisely: For any real number `r` with absolute value less than 1, the infinite geometric series `β(r^n | n β β)` equals `(1 - r)β»ΒΉ`.
|
tsum_coe_mul_geometric_of_norm_lt_1
theorem tsum_coe_mul_geometric_of_norm_lt_1 :
β {π : Type u_4} [inst : NormedDivisionRing π] [inst_1 : CompleteSpace π] {r : π},
βrβ < 1 β β' (n : β), βn * r ^ n = r / (1 - r) ^ 2
The theorem `tsum_coe_mul_geometric_of_norm_lt_1` states that for any normed division ring `π` which is a complete space, and for any element `r` of `π` such that the norm of `r` is less than one, the sum of the series `n * r ^ n` for all natural numbers `n` is equal to `r / (1 - r) ^ 2`. This is essentially a specific case of the geometric series sum formula, applied to a series where each term is multiplied by its index.
More concisely: For any complete normed division ring `π` and any element `r` in `π` with norm less than 1, the sum of the series $\sum\_{n=0}^\infty n\cdot r^n$ equals $r / (1-r) ^ 2$.
|
Real.summable_pow_div_factorial
theorem Real.summable_pow_div_factorial : β (x : β), Summable fun n => x ^ n / βn.factorial
The theorem `Real.summable_pow_div_factorial` asserts that for every real number `x`, the series `β' n, x ^ n / n!` is summable. In other words, it says that the infinite series where each term is `x` raised to the power `n` divided by the factorial of `n`, for all natural numbers `n`, has a finite sum. There are also similar versions of this theorem that hold in the field of complex numbers (`β`) and for any normed algebra over the real or complex numbers.
More concisely: The theorem asserts that the series β(_n_: _nat_), _x_\_^(_n_) / _n!_ is convergent for every real number \(x\).
|
Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded
theorem Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded :
β {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E] {b : β} {f : β β β} {z : β β E},
Antitone f β
Filter.Tendsto f Filter.atTop (nhds 0) β
(β (n : β), β(Finset.range n).sum fun i => z iβ β€ b) β
CauchySeq fun n => (Finset.range n).sum fun i => f i β’ z i
**Dirichlet's Test for Antitone Sequences**
This theorem states that for any normed additive commutative group `E` with a normed space over the real numbers, given a real number `b`, a sequence of real numbers `f`, and a sequence of elements `z` from `E`, if `f` is an antitone function (a function where if `a` is less than or equal to `b` then `f(b)` is less than or equal to `f(a)`), `f` tends to zero at infinity, and the norm of the sum of the sequence `z` up to `n` is always less than or equal to `b` for every natural number `n`, then the series obtained by multiplying `f` and `z` term-by-term and summing the results up to `n` is a Cauchy sequence (a sequence where the distance between terms gets arbitrarily small as the sequence progresses to infinity).
More concisely: If `E` is a normed additive commutative group over the real numbers, `b` is a real number, `f` is an antitone function tending to zero at infinity, and the norm of the partial sums of sequence `z` in `E` is bounded by `b` for all natural numbers `n`, then the sequence obtained by multiplying `f` and `z` term-by-term is a Cauchy sequence.
|
summable_geometric_of_norm_lt_1
theorem summable_geometric_of_norm_lt_1 :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β Summable fun n => ΞΎ ^ n
The theorem `summable_geometric_of_norm_lt_1` states that for any element `ΞΎ` of a normed division ring `K`, if the norm of `ΞΎ` is less than 1, then the series formed by taking powers of `ΞΎ` (i.e., the series ΞΎ^n for n in β) is summable. In plain English, it implies that a geometric series with ratio whose absolute value is less than one will always converge or have a finite sum.
More concisely: If `ΞΎ` is an element in a normed division ring `K` with norm less than 1, then the series `β(ΞΎ^n : n in β)` converges.
|
isLittleO_pow_const_const_pow_of_one_lt
theorem isLittleO_pow_const_const_pow_of_one_lt :
β {R : Type u_4} [inst : NormedRing R] (k : β) {r : β}, 1 < r β (fun n => βn ^ k) =o[Filter.atTop] fun n => r ^ n
This theorem states that for any natural number `k` and a real number `r` greater than `1`, the function `n ^ k` (where `n` is a natural number) is dominated by `r ^ n` as `n` approaches infinity. This is to say that the growth rate of `n ^ k` is less than the growth rate of `r ^ n` for large `n`. The domination is expressed using the little-o notation (`=o[Filter.atTop]`), which is a mathematical notation used to describe limiting behavior. The `Filter.atTop` indicates that we are considering the behavior as `n` goes to infinity. The context is a normed ring `R`.
More concisely: For any natural number `k` and real number `r` > 1 in a normed ring `R`, `n ^ k = o[Filter.atTop] (r ^ n)` as `n` approaches infinity.
|
tendsto_self_mul_const_pow_of_lt_one
theorem tendsto_self_mul_const_pow_of_lt_one :
β {r : β}, 0 β€ r β r < 1 β Filter.Tendsto (fun n => βn * r ^ n) Filter.atTop (nhds 0)
The theorem `tendsto_self_mul_const_pow_of_lt_one` states that if `r` is a real number such that `0 β€ r < 1`, then the function `n * r ^ n` tends to zero as `n` tends to infinity. Here, the function `n * r ^ n` is taken to be a function of the natural number `n`, which is implicitly extended to a function on the real numbers. This is a specialized version of another theorem `tendsto_self_mul_const_pow_of_abs_lt_one`, and is provided for ease of application.
More concisely: If `0 β€ r < 1`, then `n * r^n` approaches 0 as `n` approaches infinity.
|
tendsto_norm_atTop_atTop
theorem tendsto_norm_atTop_atTop : Filter.Tendsto norm Filter.atTop Filter.atTop
The theorem `tendsto_norm_atTop_atTop` states that the norm function has a limit of positive infinity (`atTop`) when its argument tends to positive infinity (`atTop`). More precisely, for every unbounded set in the codomain, the preimage under the norm function is an unbounded set in the domain. This captures the intuitive notion that as the input values grow without bound, so do their norms.
More concisely: For every unbounded set in the codomain of the norm function, its preimage in the domain is also unbounded.
|
cauchySeq_finset_of_geometric_bound
theorem cauchySeq_finset_of_geometric_bound :
β {Ξ± : Type u_1} [inst : SeminormedAddCommGroup Ξ±] {r C : β} {f : β β Ξ±},
r < 1 β (β (n : β), βf nβ β€ C * r ^ n) β CauchySeq fun s => s.sum fun x => f x
This theorem states that if there exists some real number `r` less than 1 and `C` such that the norm `βf nβ` of a function `f : β β Ξ±` is less than or equal to `C * r^n` for all natural numbers `n`, then the partial sums of `f` form a Cauchy sequence. Here, `Ξ±` is a type with a seminormed additively commutative group structure. This theorem does not make any assumptions about `r` or `C` being nonnegative. A Cauchy sequence is a sequence whose terms become arbitrarily close to each other as the sequence progresses.
More concisely: If a real-valued function `f` on natural numbers satisfies `βf nβ β€ C * r^n` for some `r < 1` and `C`, then the partial sums of `f` form a Cauchy sequence.
|
summable_pow_mul_geometric_of_norm_lt_1
theorem summable_pow_mul_geometric_of_norm_lt_1 :
β {R : Type u_4} [inst : NormedRing R] [inst_1 : CompleteSpace R] (k : β) {r : R},
βrβ < 1 β Summable fun n => βn ^ k * r ^ n
The theorem `summable_pow_mul_geometric_of_norm_lt_1` states that for any normed ring `R` that is a complete space, any natural number `k`, and any element `r` of `R` such that the norm of `r` is less than 1, the series formed by the function `n => n^k * r^n` is summable. In other words, the infinite sum of the terms `n^k * r^n` (where `n` is a natural number) exists and is finite when the norm of `r` is strictly less than 1.
More concisely: For any complete normed ring R and natural number k, if the norm of r in R is strictly less than 1, then the series sum of n => n^k * r^n is convergent.
|
Antitone.cauchySeq_alternating_series_of_tendsto_zero
theorem Antitone.cauchySeq_alternating_series_of_tendsto_zero :
β {f : β β β},
Antitone f β
Filter.Tendsto f Filter.atTop (nhds 0) β CauchySeq fun n => (Finset.range n).sum fun i => (-1) ^ i * f i
The theorem, known as the alternating series test for antitone sequences, states that for every function `f` from natural numbers to real numbers, if `f` is antitone (i.e., `a β€ b` implies `f(b) β€ f(a)`) and `f` tends to zero as it approaches infinity (formally, `Filter.Tendsto f Filter.atTop (nhds 0)`), then the sequence formed by the sum of the terms `(-1)^i * f(i)` for `i` in the range from `0` to `n-1` (expressed as `fun n => (Finset.range n).sum fun i => (-1) ^ i * f i`) is a Cauchy sequence. A Cauchy sequence is a sequence where the difference between any two sequence elements becomes arbitrarily small as you go farther out in the sequence. The alternating series test is a crucial tool in real analysis for determining the convergence of series.
More concisely: If a function `f` from natural numbers to real numbers is antitone and tends to zero at infinity, then the sequence formed by the alternating sum of `(-1)^i * f(i)` is Cauchy.
|
tendsto_self_mul_const_pow_of_abs_lt_one
theorem tendsto_self_mul_const_pow_of_abs_lt_one :
β {r : β}, |r| < 1 β Filter.Tendsto (fun n => βn * r ^ n) Filter.atTop (nhds 0)
This theorem states that for any real number `r` whose absolute value is less than one, the sequence `n * r^n` tends to zero as `n` approaches infinity. In other words, as `n` becomes larger and larger, the value of `n * r^n` gets closer and closer to zero. This is a common result in analysis related to the behavior of geometric sequences.
More concisely: For any real number `r` with `|r| < 1`, the sequence `(n : β) β n * r^n` converges to zero as `n` goes to infinity.
|
tendsto_pow_atTop_nhds_zero_of_norm_lt_one
theorem tendsto_pow_atTop_nhds_zero_of_norm_lt_one :
β {R : Type u_4} [inst : NormedRing R] {x : R}, βxβ < 1 β Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
The theorem `tendsto_pow_atTop_nhds_zero_of_norm_lt_one` states that for any normed ring `R` and any element `x` of `R`, if the norm of `x` is less than 1, then the powers of `x` tend to zero as `n` goes to infinity. In other words, for larger and larger values of `n`, `x^n` gets closer and closer to zero. This is described within the context of filters and neighborhoods, using the `Filter.Tendsto` predicate to express the limit, with `Filter.atTop` representing `n` going to infinity, and `nhds 0` representing the neighborhood of 0.
More concisely: For any normed ring `R` and element `x` of norm less than 1, the sequence `{x^n : n is nat}` converges to zero as `n` approaches infinity.
|
summable_powerSeries_of_norm_lt_one
theorem summable_powerSeries_of_norm_lt_one :
β {Ξ± : Type u_1} [inst : NormedDivisionRing Ξ±] [inst_1 : CompleteSpace Ξ±] {f : β β Ξ±} {z : Ξ±},
(CauchySeq fun n => (Finset.range n).sum fun i => f i) β βzβ < 1 β Summable fun n => f n * z ^ n
The theorem `summable_powerSeries_of_norm_lt_one` states that for any normed division ring `Ξ±` that is also a complete space, given a sequence of elements `f` from `Ξ±` and an element `z` from `Ξ±`, if the sequence `f` forms a Cauchy sequence when summed over all the natural numbers less than `n` for all `n` (which essentially means the power series of `f` converges at 1), and the norm of `z` is less than 1, then the power series of `f` multiplied by `z` to the power of `n` is summable, meaning it has a finite sum.
In mathematical terms, this theorem states that if a power series converges at 1, then it absolutely converges for all complex numbers `z` with a norm less than 1.
More concisely: If a power series over a complete normed division ring converges at 1 and the norm of the multiplicative argument is less than 1, then the power series is absolutely convergent.
|
norm_sub_le_of_geometric_bound_of_hasSum
theorem norm_sub_le_of_geometric_bound_of_hasSum :
β {Ξ± : Type u_1} [inst : SeminormedAddCommGroup Ξ±] {r C : β} {f : β β Ξ±},
r < 1 β
(β (n : β), βf nβ β€ C * r ^ n) β
β {a : Ξ±}, HasSum f a β β (n : β), β((Finset.range n).sum fun x => f x) - aβ β€ C * r ^ n / (1 - r)
This theorem states that if we have a sequence of elements `f` from a seminormed additively commutative group (a type of mathematical structure), and the norm of the nth element of `f` is less than or equal to `C * r ^ n` for all natural numbers `n` and some constant `r` that is less than 1, then the difference between the sum of the first `n` elements of `f` and the total sum of the sequence `f` is bounded by `C * r ^ n / (1 - r)`. This statement holds regardless of the signs of `r` and `C`. The total sum of the sequence `f` is denoted by `a` and it is assumed that the sequence `f` sums up to `a`, which is a pre-requisite condition expressed by `HasSum f a`.
More concisely: If `f` is a sequence in a seminormed additively commutative group with `HasSum f a`, and the norm of the `n`-th element is bounded by `C * r ^ n` for all `n` and some `r` with `|r| < 1`, then the error in approximating the sum `a` by the sum of the first `n` elements is bounded by `C * r ^ n / (1 - r)`.
|
Antitone.tendsto_alternating_series_of_tendsto_zero
theorem Antitone.tendsto_alternating_series_of_tendsto_zero :
β {f : β β β},
Antitone f β
Filter.Tendsto f Filter.atTop (nhds 0) β
β l, Filter.Tendsto (fun n => (Finset.range n).sum fun i => (-1) ^ i * f i) Filter.atTop (nhds l)
This theorem is known as the **alternating series test** for antitone sequences. It states that if you have a sequence of real numbers `f` that is antitone (meaning that if `a β€ b`, then `f(b) β€ f(a)`), and `f` tends to `0` as `n` goes to infinity (`Filter.Tendsto f Filter.atTop (nhds 0)`), then there exists a limit `l`. This limit `l` is such that the series obtained by summing up the terms `(-1) ^ i * f i` for `i` in the range from `0` to `n` (represented by `(Finset.range n).sum fun i => (-1) ^ i * f i`) tends to `l` as `n` goes to infinity. This theorem is a fundamental result in calculus and analysis, used for determining the convergence of certain types of infinite series.
More concisely: If `f` is a real-valued, antitone function that tends to 0 at infinity, then the alternating series `β(i <- Finset.range n) (-1)^i * f i` converges to the limit `l` as `n` goes to infinity.
|
tsum_geometric_of_norm_lt_one
theorem tsum_geometric_of_norm_lt_one :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β β' (n : β), ΞΎ ^ n = (1 - ΞΎ)β»ΒΉ
The theorem `tsum_geometric_of_norm_lt_one` states that for any normed field `K` and any element `ΞΎ` in `K` with a norm less than one, the infinite sum of `ΞΎ` raised to the power of `n` over all `n` in natural numbers (which essentially forms a geometric series) is equal to `(1 - ΞΎ)β»ΒΉ` (i.e., the inverse of `1 - ΞΎ`). This is a result from calculus known as the sum of an infinite geometric series, where the common ratio lies between -1 and 1.
More concisely: For any normed field `K` and `ΞΎ` in `K` with norm less than one, the infinite geometric series `β(ΞΎβ± : β) where i : β, i != 0 := ΞΎβ±` equals `(1 - ΞΎ)β»ΒΉ`.
|
hasSum_geometric_of_norm_lt_1
theorem hasSum_geometric_of_norm_lt_1 :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β HasSum (fun n => ΞΎ ^ n) (1 - ΞΎ)β»ΒΉ
This theorem, `hasSum_geometric_of_norm_lt_1`, is an alias of `hasSum_geometric_of_norm_lt_one`. It states that for any normed division ring `K` and any element `ΞΎ` in `K`, if the norm of `ΞΎ` is less than 1, then the sum of the infinite geometric series where each term is `ΞΎ` raised to the power `n` (with `n` ranging over all non-negative integers) equals the inverse of `(1 - ΞΎ)`.
More concisely: For any normed division ring K and any element ΞΎ in K with norm less than 1, the infinite geometric series sum is equal to the multiplicative inverse of (1 - ΞΎ).
|
isLittleO_pow_pow_of_lt_left
theorem isLittleO_pow_pow_of_lt_left :
β {rβ rβ : β}, 0 β€ rβ β rβ < rβ β (fun n => rβ ^ n) =o[Filter.atTop] fun n => rβ ^ n
This theorem states that for any real numbers `rβ` and `rβ` with `rβ` nonnegative and less than `rβ`, the function that takes an integer `n` to `rβ^n` is `little o` (is dominated by) the function that takes `n` to `rβ^n` as `n` goes to infinity. In mathematical terms, this means that `rβ^n = o(rβ^n)` as `n β β`, which is to say, the growth rate of `rβ^n` is strictly less than the growth rate of `rβ^n` when `rβ < rβ` and `rβ` is nonnegative.
More concisely: For any nonnegative real number `rβ` less than `rβ`, `rβ^n = o(rβ^n)` as `n β β`.
|
tsum_geometric_of_norm_lt_1
theorem tsum_geometric_of_norm_lt_1 :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β β' (n : β), ΞΎ ^ n = (1 - ΞΎ)β»ΒΉ
This theorem, `tsum_geometric_of_norm_lt_1`, states that for any normed division ring `K` and any element `ΞΎ` of `K`, if the norm of `ΞΎ` is less than 1, then the infinite sum of the series formed by raising `ΞΎ` to the power of each natural number `n` (`β' (n : β), ΞΎ ^ n`) equals the reciprocal of `1 - ΞΎ` (i.e., `(1 - ΞΎ)β»ΒΉ`). In other words, it proves the convergence of a geometric series where the common ratio has a norm less than 1.
More concisely: For any normed division ring `K` and element `ΞΎ` in `K` with norm strictly less than 1, the infinite geometric series `β' (n : β), ΞΎ ^ n` converges to the reciprocal of `(1 - ΞΎ)`.
|
summable_norm_pow_mul_geometric_of_norm_lt_1
theorem summable_norm_pow_mul_geometric_of_norm_lt_1 :
β {R : Type u_4} [inst : NormedRing R] (k : β) {r : R}, βrβ < 1 β Summable fun n => ββn ^ k * r ^ nβ
The theorem `summable_norm_pow_mul_geometric_of_norm_lt_1` states that for any normed ring `R`, any natural number `k`, and any element `r` of `R` such that the norm of `r` is less than 1, the sequence formed by taking the norm of `n` raised to the power `k` multiplied by `r` raised to the power `n` for every natural number `n` is summable. In other words, it affirms the convergency of the series defined by the norms of the terms of a geometric sequence whose ratio has a norm less than 1, where each term is also multiplied by the natural number raised to the power `k`.
More concisely: For any normed ring R, natural number k, and element r in R with norm less than 1, the series sum of the norms of r raised to the power of n multiplied by n raised to the power of k for all natural numbers n converges.
|
tendsto_pow_const_mul_const_pow_of_lt_one
theorem tendsto_pow_const_mul_const_pow_of_lt_one :
β (k : β) {r : β}, 0 β€ r β r < 1 β Filter.Tendsto (fun n => βn ^ k * r ^ n) Filter.atTop (nhds 0)
This theorem states that if we have a non-negative real number `r` that is less than one, then for any natural number `k`, the sequence given by the function `n ^ k * r ^ n` tends to zero as `n` tends to infinity. In other words, the product of `n` to the power `k` and `r` to the power `n` gets arbitrarily close to zero when `n` becomes large enough, given that `r` is in the interval `[0, 1)`. This is a specialized version of a more general theorem, `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, and is singled out for its ease of use.
More concisely: For any non-negative real number `r` with `r < 1` and natural number `k`, the sequence `n => r^n * n^k` converges to zero as `n` approaches infinity.
|
summable_geometric_iff_norm_lt_one
theorem summable_geometric_iff_norm_lt_one :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, (Summable fun n => ΞΎ ^ n) β βΞΎβ < 1
The theorem `summable_geometric_iff_norm_lt_one` in Lean 4 states that, for any normed field `K` and any element `ΞΎ` from `K`, the geometric series `ΞΎ ^ n` (for all `n`) is summable if and only if the norm of the common ratio `ΞΎ` is less than one. In other words, the geometric series converges when the norm of the ratio between successive terms is less than one, and diverges otherwise. This is a well-known result in the field of series in analysis.
More concisely: A geometric series over a normed field converges if and only if the norm of the common ratio is less than one.
|
NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded
theorem NormedField.tendsto_zero_smul_of_tendsto_zero_of_bounded :
β {ΞΉ : Type u_4} {π : Type u_5} {πΈ : Type u_6} [inst : NormedDivisionRing π] [inst_1 : NormedAddCommGroup πΈ]
[inst_2 : Module π πΈ] [inst_3 : BoundedSMul π πΈ] {l : Filter ΞΉ} {Ξ΅ : ΞΉ β π} {f : ΞΉ β πΈ},
Filter.Tendsto Ξ΅ l (nhds 0) β
Filter.IsBoundedUnder (fun x x_1 => x β€ x_1) l (norm β f) β Filter.Tendsto (Ξ΅ β’ f) l (nhds 0)
This theorem states that for a sequence `Ξ΅` which approaches 0 (expressed as `Filter.Tendsto Ξ΅ l (nhds 0)`) and a bounded sequence `f` (expressed as `Filter.IsBoundedUnder (fun x x_1 => x β€ x_1) l (norm β f)`), the sequence resulting from the scalar multiplication of `Ξ΅` and `f` (denoted as `Ξ΅ β’ f`) also approaches 0 (expressed as `Filter.Tendsto (Ξ΅ β’ f) l (nhds 0)`). The sequences are defined over some arbitrary filter `l`, taking values in a normed division ring `π` and a normed additive commutative group `πΈ` respectively, with `π` acting as a module over `πΈ`. The boundedness of the sequence `f` is with respect to the norm function.
More concisely: If a sequence `Ξ΅` tends to 0 and is bounded in norm, and `f` is a bounded sequence in norm, then the sequence of their scalar multiplications `Ξ΅ β’ f` tends to the zero sequence in norm.
|
hasSum_geometric_of_norm_lt_one
theorem hasSum_geometric_of_norm_lt_one :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β HasSum (fun n => ΞΎ ^ n) (1 - ΞΎ)β»ΒΉ
This theorem states that for any type `K` that is a normed field and any element `ΞΎ` of `K`, if the norm of `ΞΎ` is less than one, then the sum of the infinite geometric series where each term is `ΞΎ` to the power of `n` converges to the value `(1 - ΞΎ)β»ΒΉ`. A geometric series is a series for which each term after the first is found by multiplying the previous term by a fixed, non-zero number called the common ratio. In this case, `ΞΎ` is the common ratio.
More concisely: For any normed field `K` and element `ΞΎ` of norm less than 1 in `K`, the infinite geometric series `β(ΞΎ^n)` converges to `(1 - ΞΎ)β»ΒΉ`.
|
tendsto_pow_atTop_nhds_0_of_abs_lt_1
theorem tendsto_pow_atTop_nhds_0_of_abs_lt_1 :
β {r : β}, |r| < 1 β Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem, `tendsto_pow_atTop_nhds_0_of_abs_lt_1`, states that for any real number `r` with its absolute value less than one, the function which takes a natural number `n` and maps it to `r` to the power of `n` tends to zero as `n` approaches infinity. In mathematical terms, if $|r| < 1$, then $r^n$ tends to 0 as $n β β$. This is an important result in analysis that characterizes the behavior of powers of real numbers that are strictly between -1 and 1.
More concisely: For any real number `r` with absolute value less than 1, `r^n` converges to 0 as `n` approaches infinity.
|
isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt
theorem isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt :
β {R : Type u_4} [inst : NormedRing R] (k : β) {rβ : R} {rβ : β},
βrββ < rβ β (fun n => βn ^ k * rβ ^ n) =o[Filter.atTop] fun n => rβ ^ n
This theorem states that in a normed ring `R`, if the norm of `rβ` is less than `rβ` (i.e., `βrββ < rβ`), then for any natural number `k`, the function defined by `n` to the power of `k` times `rβ` to the power of `n` (i.e., `βn ^ k * rβ ^ n`) is little-o of `rβ` to the power of `n` (i.e., `rβ ^ n`) when `n` tends to infinity. In other words, the growth rate of `βn ^ k * rβ ^ n` is significantly smaller than the growth rate of `rβ ^ n` as `n` approaches infinity.
More concisely: In a normed ring, for any `rβ, rβ in R` with `βrββ < rβ`, the power series `x => x ^ k * rβ ^ x` is little-o of `x => rβ ^ x` as `x` tends to infinity.
|
hasSum_coe_mul_geometric_of_norm_lt_1
theorem hasSum_coe_mul_geometric_of_norm_lt_1 :
β {π : Type u_4} [inst : NormedDivisionRing π] [inst_1 : CompleteSpace π] {r : π},
βrβ < 1 β HasSum (fun n => βn * r ^ n) (r / (1 - r) ^ 2)
This theorem, named `hasSum_coe_mul_geometric_of_norm_lt_1`, states that for any type `π` which is a normed division ring and complete space, and any element `r` of this type such that the norm of `r` is less than 1, the infinite sum of the series `n * r ^ n` (for `n` ranging over natural numbers) converges and equals `r / (1 - r) ^ 2`. This is the `HasSum` version of a series with geometric progression where the ratio's norm is less than one.
More concisely: For any normed division ring and complete space π, and any element r in π with norm less than 1, the infinite geometric series r + r^2 + r^3 + ... converges to r / (1 - r)^2.
|
NormedRing.summable_geometric_of_norm_lt_one
theorem NormedRing.summable_geometric_of_norm_lt_one :
β {R : Type u_4} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : R), βxβ < 1 β Summable fun n => x ^ n := by
sorry
This theorem states that a geometric series in a complete normed ring is summable. Specifically, for any element `x` in a type `R` that is a complete normed ring, if the norm of `x` (denoted as βxβ) is less than 1, then the function defined by raising `x` to the power `n` (i.e., `x ^ n`) is summable. A function is deemed summable if it has some infinite sum. This result has been proved earlier for normed fields that may not necessarily be complete.
More concisely: In a complete normed ring, if the norm of an element is less than 1, then the geometric series formed by summing the powers of that element converges.
|
summable_geometric_of_abs_lt_1
theorem summable_geometric_of_abs_lt_1 : β {r : β}, |r| < 1 β Summable fun n => r ^ n
The theorem `summable_geometric_of_abs_lt_1` states that for any real number `r` with an absolute value less than 1, the function `fun n => r ^ n` (which represents the geometric sequence with ratio `r`) is summable. In other words, if `|r| < 1`, the infinite series $\sum_{n=0}^{\infty} r^n$ converges to a finite sum. This is a fundamental result in real analysis and is often referred to as the convergence of a geometric series.
More concisely: For any real number `r` with an absolute value less than 1, the infinite series $\sum\_{n=0}^{\infty} r^n$ converges to a finite sum.
|
NormedRing.tsum_geometric_of_norm_lt_one
theorem NormedRing.tsum_geometric_of_norm_lt_one :
β {R : Type u_4} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : R),
βxβ < 1 β ββ' (n : β), x ^ nβ β€ β1β - 1 + (1 - βxβ)β»ΒΉ
This theorem states that for any element `x` in a normed ring `R` (which needn't satisfy `β1β = 1`), if the norm of `x` is less than one, then the norm of the sum of the infinite geometric series with terms `x^n` is less than or equal to `β1β - 1 + (1 - βxβ)β»ΒΉ`. Here the normed ring is also assumed to be complete (i.e., all Cauchy sequences in `R` converge in `R`).
More concisely: In a complete normed ring satisfying `β1β β 1`, if `βxβ < 1` for some `x`, then `βββ xβ± β β€ β1β - 1 + 1/(1 - βxβ)` where the sum is the infinite geometric series with first term `x` and common ratio `x`.
|
summable_geometric_of_norm_lt_one
theorem summable_geometric_of_norm_lt_one :
β {K : Type u_4} [inst : NormedDivisionRing K] {ΞΎ : K}, βΞΎβ < 1 β Summable fun n => ΞΎ ^ n
The theorem `summable_geometric_of_norm_lt_one` states that for any normed field `K` and any element `ΞΎ` of `K`, if the norm of `ΞΎ` is strictly less than 1, then the infinite geometric series `ΞΎ^n` is summable. Here, summability refers to the existence of a finite sum to which the infinite series converges. In the context of this theorem, the infinite series is the sequence of terms `ΞΎ^n` as `n` ranges over all nonnegative integers.
More concisely: For any normed field K and any element ΞΎ in K with norm strictly less than 1, the geometric series Ξ£(ΞΎ^n. LEAN: β i, xi < power i 1) converges.
|
Monotone.tendsto_alternating_series_of_tendsto_zero
theorem Monotone.tendsto_alternating_series_of_tendsto_zero :
β {f : β β β},
Monotone f β
Filter.Tendsto f Filter.atTop (nhds 0) β
β l, Filter.Tendsto (fun n => (Finset.range n).sum fun i => (-1) ^ i * f i) Filter.atTop (nhds l)
The theorem `Monotone.tendsto_alternating_series_of_tendsto_zero` states the alternating series test for monotone sequences. Specifically, it says that for any monotone real-valued function `f` on the natural numbers, if `f` tends to zero as its argument goes to infinity, then there exists a limit `l` such that the alternating series given by summing `(-1)^i * f(i)` over the range of natural numbers less than `n`, also tends to `l` as `n` approaches infinity. In simpler terms, if the terms in a monotone sequence are approaching zero, the alternating series composed of these terms converges to some limit.
More concisely: If a monotonic real sequence `f(i)` converges to 0, then the alternating series `β(-1)^i * f(i)` converges to the same limit.
|
TFAE_exists_lt_isLittleO_pow
theorem TFAE_exists_lt_isLittleO_pow :
β (f : β β β) (R : β),
[β a β Set.Ioo (-R) R, f =o[Filter.atTop] fun x => a ^ x, β a β Set.Ioo 0 R, f =o[Filter.atTop] fun x => a ^ x,
β a β Set.Ioo (-R) R, f =O[Filter.atTop] fun x => a ^ x, β a β Set.Ioo 0 R, f =O[Filter.atTop] fun x => a ^ x,
β a < R, β C, (0 < C β¨ 0 < R) β§ β (n : β), |f n| β€ C * a ^ n,
β a β Set.Ioo 0 R, β C > 0, β (n : β), |f n| β€ C * a ^ n, β a < R, βαΆ (n : β) in Filter.atTop, |f n| β€ a ^ n,
β a β Set.Ioo 0 R, βαΆ (n : β) in Filter.atTop, |f n| β€ a ^ n].TFAE
This theorem, `TFAE_exists_lt_isLittleO_pow`, establishes a list of equivalent conditions related to the growth rate of a function `f : β β β` in comparison to exponential functions. Specifically, these conditions are in terms of asymptotic analysis with little-o notation (`=o`) and big-O notation (`=O`) at infinity (`Filter.atTop`).
The conditions include: the function `f` is `o(a^n)` for some `a` in an open interval around `R` or only considering positive `a`; the function `f` is `O(a^n)` under the same interval conditions; there exist constants `a` and `C` (with either `C` or `R` being positive) such that `|f(n)| β€ C*a^n` for all `n`; there's `a` in the same intervals such that `|f(n)| β€ a^n` for sufficiently large `n`.
The theorem states that these conditions are all equivalent to each other, i.e., any of these conditions implies all the others. The proof is omitted in this excerpt.
More concisely: The theorem `TFAE_exists_lt_isLittleO_pow` in Lean 4 states that for a function `f : β β β`, the conditions of being `o(a^n)` for some `a > 0`, being `O(a^n)`, having a constant `C` and `a > 0` such that `|f(n)| β€ C*a^n` for all `n`, and having an `a > 0` such that `|f(n)| β€ a^n` for sufficiently large `n`, are all equivalent.
|
Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded
theorem Monotone.cauchySeq_series_mul_of_tendsto_zero_of_bounded :
β {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace β E] {b : β} {f : β β β} {z : β β E},
Monotone f β
Filter.Tendsto f Filter.atTop (nhds 0) β
(β (n : β), β(Finset.range n).sum fun i => z iβ β€ b) β
CauchySeq fun n => (Finset.range n).sum fun i => f i β’ z i
**Dirichlet's Test for Monotone Sequences**
The theorem states that for any normed additive commutative group `E` and any normed space `E` over the real numbers, given a real number `b`, a function `f` from natural numbers to real numbers, and a function `z` from natural numbers to `E`, if `f` is a monotone function and it tends to 0 as the argument tends to infinity, and for every natural number `n`, the norm of the sum of the function `z` over the range less than `n` is less than or equal to `b`, then the sequence defined by the sum of the scaled values `f i β’ z i` (where `β’` represents scalar multiplication) over the range less than `n` is a Cauchy sequence.
In mathematical notation, the theorem says: if function `f` is monotone and `lim_{nββ} f(n) = 0`, and `βn, ||Ξ£_{i
More concisely: If a monotonic, convergent to 0 function `f` and a bounded sequence `z` satisfy `||Ξ£β
|
hasSum_coe_mul_geometric_of_norm_lt_one
theorem hasSum_coe_mul_geometric_of_norm_lt_one :
β {π : Type u_4} [inst : NormedDivisionRing π] [inst_1 : CompleteSpace π] {r : π},
βrβ < 1 β HasSum (fun n => βn * r ^ n) (r / (1 - r) ^ 2)
This theorem states that for any element `r` of a complete normed division ring `π` (a type of mathematical structure that includes fields like the real or complex numbers, endowed with a norm), if the norm of `r` is less than 1, then the sum of the series given by `n * r ^ n` (where `n` ranges over the natural numbers) converges and its sum is `r / (1 - r) ^ 2`. This is known as a geometric series, and the theorem gives a condition for its convergence and the value to which it converges.
More concisely: In a complete normed division ring, if the norm of an element is less than 1, then the geometric series `β(n: nat) (n * r ^ n)` converges to `r / (1 - r) ^ 2`.
|
exists_norm_le_of_cauchySeq
theorem exists_norm_le_of_cauchySeq :
β {Ξ± : Type u_1} [inst : SeminormedAddCommGroup Ξ±] {f : β β Ξ±},
(CauchySeq fun n => (Finset.range n).sum fun k => f k) β β C, β (n : β), βf nβ β€ C
The theorem `exists_norm_le_of_cauchySeq` states that if we have a Cauchy sequence formed by the partial sums of a series (over the natural numbers) in a seminormed additive commutative group, then there exists a constant `C` such that the norm of each term in the series is less than or equal to `C`. Essentially, this means that the sequence of norms of the terms of any convergent series is bounded.
More concisely: If `(s_n)` is a Cauchy sequence of partial sums of a series in a seminormed additive commutative group, then there exists a constant `C` such that `||s_n|| β€ C` for all `n`.
|
summable_powerSeries_of_norm_lt
theorem summable_powerSeries_of_norm_lt :
β {Ξ± : Type u_1} [inst : NormedDivisionRing Ξ±] [inst_1 : CompleteSpace Ξ±] {f : β β Ξ±} {w z : Ξ±},
(CauchySeq fun n => (Finset.range n).sum fun i => f i * w ^ i) β βzβ < βwβ β Summable fun n => f n * z ^ n
The theorem `summable_powerSeries_of_norm_lt` states that for any normed division ring `Ξ±` that is also a complete space, given a sequence of elements `f` from `Ξ±`, and two elements `w` and `z` of `Ξ±`, if the Cauchy sequence defined by the partial sums of the power series of `f` and `w` exists, then if the norm of `z` is strictly less than the norm of `w`, the power series of `f` and `z` is summable. In other words, if a power series converges at a point `w`, it will also converge absolutely at all points `z` with smaller norm.
More concisely: If `Ξ±` is a complete, normed division ring, `f` is a sequence in `Ξ±`, `w` and `z` are elements of `Ξ±` with `norm w > norm z`, and the Cauchy sequence of partial sums of the power series of `f` and `w` exists, then the power series of `f` is absolutely summable at `z`.
|
Monotone.cauchySeq_alternating_series_of_tendsto_zero
theorem Monotone.cauchySeq_alternating_series_of_tendsto_zero :
β {f : β β β},
Monotone f β
Filter.Tendsto f Filter.atTop (nhds 0) β CauchySeq fun n => (Finset.range n).sum fun i => (-1) ^ i * f i
This theorem states the **alternating series test** for monotone sequences. Given a sequence `f` of real numbers that is monotone and tends to 0 as it approaches infinity, the theorem asserts that the sequence formed by the sum of `(-1)^i * f(i)` for each `i` in the range from 0 to `n` is a Cauchy sequence. This means that for every positive real number `Ξ΅`, there exists a positive integer `N` such that for all `m, n > N`, the absolute difference between the `m`-th term and the `n`-th term of the sequence is less than `Ξ΅`.
More concisely: The alternating series formed by summing `(-1)^i * f(i)` from `i=0` to `n` of a monotone, convergent sequence `f(i)` to 0 is a Cauchy sequence.
|
NormedRing.tsum_geometric_of_norm_lt_1
theorem NormedRing.tsum_geometric_of_norm_lt_1 :
β {R : Type u_4} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : R),
βxβ < 1 β ββ' (n : β), x ^ nβ β€ β1β - 1 + (1 - βxβ)β»ΒΉ
This theorem, known as an alias of `NormedRing.tsum_geometric_of_norm_lt_one`, provides a bound for the sum of a geometric series in a normed ring, where the norm of the common ratio is less than one. It is worth noting that this theorem does not assume the norm of 1 is equal to 1. Specifically, for any normed ring `R` that is also a complete space, and any element `x` of `R` with a norm less than one, the norm of the sum of the geometric series with `x` as the common ratio is bounded from above by the norm of 1 minus 1, plus the reciprocal of (1 minus the norm of `x`).
More concisely: For any normed ring R that is complete, and any x in R with norm less than 1, the norm of the sum of the geometric series with common ratio x is bounded by 1 + 1/(|1 - norm x|).
|
tendsto_pow_atTop_nhds_0_of_norm_lt_1
theorem tendsto_pow_atTop_nhds_0_of_norm_lt_1 :
β {R : Type u_4} [inst : NormedRing R] {x : R}, βxβ < 1 β Filter.Tendsto (fun n => x ^ n) Filter.atTop (nhds 0)
This theorem, known as `tendsto_pow_atTop_nhds_0_of_norm_lt_1`, states that in a normed ring R, for any element `x` in R, if the norm of `x` (`βxβ`) is less than 1, then the sequence of its powers (`x ^ n` for all natural numbers `n`) tends to zero as `n` goes to infinity. This is expressed in the theorem through the use of `Filter.Tendsto`, which signifies the limit of a function or sequence, `Filter.atTop`, which represents the limit going to infinity, and `nhds 0`, representing the neighborhood of 0 in a topological space.
More concisely: In a normed ring, if the norm of an element is less than 1, then its sequence of powers converges to zero as n goes to infinity.
|
tsum_geometric_of_abs_lt_1
theorem tsum_geometric_of_abs_lt_1 : β {r : β}, |r| < 1 β β' (n : β), r ^ n = (1 - r)β»ΒΉ
This theorem, `tsum_geometric_of_abs_lt_1`, states that for any real number `r` whose absolute value is less than 1, the sum of the infinite geometric series where each term is `r` raised to the power of `n` (where `n` is a non-negative integer) is equal to the reciprocal of `(1 - r)`. In mathematical terms, if |r| < 1, then the sum from n=0 to infinity of r^n equals 1/(1 - r). This theorem is an alias of another theorem, `tsum_geometric_of_abs_lt_one`.
More concisely: For any real number `r` with |r| < 1, the sum of the infinite geometric series with first term `r` and common ratio `r` equals the reciprocal of `(1 - r)`.
|
NormedRing.summable_geometric_of_norm_lt_1
theorem NormedRing.summable_geometric_of_norm_lt_1 :
β {R : Type u_4} [inst : NormedRing R] [inst_1 : CompleteSpace R] (x : R), βxβ < 1 β Summable fun n => x ^ n := by
sorry
The theorem `NormedRing.summable_geometric_of_norm_lt_1` states that for any given complete normed ring `R` and an element `x` in `R`, if the norm of `x` is less than 1, then the geometric series formed by raising `x` to the power `n` (where `n` is a natural number), is summable. The term "summable" means that the infinite series has a sum. This theorem has been previously proven for normed fields that are not necessarily complete.
More concisely: For any complete normed ring `R` and element `x` with norm less than 1, the geometric series `β (x^n : R)` from `n = 0` to `β` is convergent.
|