summable_geometric_two
theorem summable_geometric_two : Summable fun n => (1 / 2) ^ n
The theorem `summable_geometric_two` states that the infinite geometric series where each term is `(1 / 2) ^ n` for a given n, is summable. In other words, it asserts that the sum of the terms `(1 / 2) ^ n` for all non-negative integers n, exists. The `Summable` function in Lean 4 is used to determine whether a given series or sequence has a finite sum, and this theorem proves that the given geometric series indeed has a finite sum.
More concisely: The theorem `summable_geometric_two` in Lean 4 asserts that the infinite geometric series with common ratio `1/2` is convergent.
|
hasSum_geometric_two'
theorem hasSum_geometric_two' : ∀ (a : ℝ), HasSum (fun n => a / 2 / 2 ^ n) a
This theorem states that for any real number `a`, the sum of the infinite series where each term is `a` divided by 2 and then divided by 2 to the power of `n` (where `n` is the index of the term in the series) is equal to `a`. In mathematical terms, this can be written as: for all `a` in ℝ, Σ (a / 2 / 2^n) = `a`.
More concisely: For any real number `a`, the sum of the infinite series where each term is `a / 2^(n+1)` equals `a`.
|
tendsto_const_div_atTop_nhds_0_nat
theorem tendsto_const_div_atTop_nhds_0_nat : ∀ (C : ℝ), Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0) := by
sorry
The theorem `tendsto_const_div_atTop_nhds_0_nat` states that for any real number `C`, the function which maps a natural number `n` to the quotient `C / n` tends to zero as `n` approaches infinity. In other words, as `n` gets larger and larger, the value of `C / n` gets closer and closer to zero. Here, `Filter.Tendsto` is used to express the limit of a function, `Filter.atTop` represents the limit going to infinity, and `nhds 0` represents the neighborhood filter of zero in a topological space.
More concisely: For any real number `C`, the sequence `{C / n | n ∈ ℕ}` converges to `0` as `n` approaches infinity.
|
cauchySeq_of_le_geometric_two
theorem cauchySeq_of_le_geometric_two :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (C : ℝ) {f : ℕ → α},
(∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) → CauchySeq f
The theorem `cauchySeq_of_le_geometric_two` states that for any sequence `f` of type `ℕ → α` in a pseudometric space `α`, if the distance between any two consecutive elements of the sequence `f` is bounded by `(C / 2) / 2^n` for a real number `C`, then the sequence `f` is a Cauchy sequence. In mathematical terms, this means if for every natural number `n`, the inequality `dist(f(n), f(n+1)) ≤ C / 2 / 2^n` holds, then `f` is a Cauchy sequence. A Cauchy sequence is a sequence where, intuitively, the elements get arbitrarily close to each other as we proceed through the sequence.
More concisely: If for all natural numbers n, the distance between consecutive terms of a sequence in a pseudometric space is bounded by C / 2^(n+1), then the sequence is a Cauchy sequence.
|
tendsto_one_div_add_atTop_nhds_0_nat
theorem tendsto_one_div_add_atTop_nhds_0_nat : Filter.Tendsto (fun n => 1 / (↑n + 1)) Filter.atTop (nhds 0)
This theorem, `tendsto_one_div_add_atTop_nhds_0_nat`, states that the function which takes a natural number `n` and maps it to `1 / (n + 1)` tends to `0` as `n` tends to infinity. In other words, for every open neighborhood of `0` in the real numbers, there exists a natural number `n` such that for all `m` greater than `n`, `1 / (m + 1)` is in that neighborhood.
More concisely: For every open neighborhood of 0 in the real numbers, there exists a natural number N such that |1 / (n + 1) - 0| < ε for all natural numbers n > N.
|
dist_le_of_le_geometric_of_tendsto
theorem dist_le_of_le_geometric_of_tendsto :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ),
r < 1 →
∀ {f : ℕ → α},
(∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ C * r ^ n / (1 - r)
This theorem states that if the distance between successive outputs of a function `f` (mapping natural numbers to any type in a pseudometric space) is bounded by `C * r^n` where `r` is less than `1`, then the distance from `f 0` to the limit of `f` is bounded above by `C / (1 - r)`. In other words, if the function `f` approaches a limit `a` (in the sense that as we take larger and larger natural numbers, the output of `f` gets arbitrarily close to `a`), and if the difference between `f n` and `f (n + 1)` can be controlled by the geometric sequence `C * r^n`, then the difference between `f n` and `a` can be controlled by `C * r^n / (1 - r)`. This is a statement about the rate of convergence of the function `f`, relating it to the rate of decrease of the differences between successive terms.
More concisely: If a function `f` mapping natural numbers to a pseudometric space satisfies the condition that the distance between `f n` and `f (n+1)` is bounded by `C * r^n` for some constant `C` and `r < 1`, then the distance from `f 0` to the limit `a` of `f` is bounded above by `C / (1 - r)`.
|
tendsto_inverse_atTop_nhds_0_nat
theorem tendsto_inverse_atTop_nhds_0_nat : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
This theorem, `tendsto_inverse_atTop_nhds_0_nat`, states that the function which maps a natural number `n` to its inverse `(↑n)⁻¹`, tends towards 0 as `n` tends towards infinity. More specifically, for every neighborhood of 0, there is a threshold beyond which all values of the function are within that neighborhood. This theorem is essentially capturing the mathematical limit concept: $\lim_{n \rightarrow \infty} \frac{1}{n} = 0$.
More concisely: For every neighborhood of 0 in the natural numbers, there exists a natural number `N` such that for all `n` greater than `N`, `(1/n)` is in that neighborhood.
|
summable_one_div_pow_of_le
theorem summable_one_div_pow_of_le :
∀ {m : ℝ} {f : ℕ → ℕ}, 1 < m → (∀ (i : ℕ), i ≤ f i) → Summable fun i => 1 / m ^ f i
This theorem states that for any real number `m` greater than 1 and any function `f` from natural numbers to natural numbers, where each natural number `i` is less than or equal to `f(i)`, the infinite series whose terms are given by `1 / m ^ f(i)` converges. In other words, if the terms of an infinite series are bounded by the terms of a converging geometric series, then that series also converges.
More concisely: If `m > 1` is a real number and `f` is a function from natural numbers to natural numbers such that `i <= f(i)` for all `i`, then the infinite series `sum i : nat (1 / m ^ (f i))` converges.
|
NNReal.tendsto_inverse_atTop_nhds_zero_nat
theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
This theorem states that the sequence of the reciprocals of natural numbers (which is expressed as the function `(fun n => (↑n)⁻¹)`) tends to zero as the numbers go to infinity, represented by `Filter.atTop`. More formally, for every neighborhood of zero, there exists a natural number such that the reciprocals of all natural numbers greater than or equal to it fall into that neighborhood. This is expressed in Lean 4 using the `Filter.Tendsto` predicate, with `(fun n => (↑n)⁻¹)` as the function, `Filter.atTop` denoting the domain filter (representing the sequence going to infinity), and `(nhds 0)` as the codomain filter (representing the neighborhood of zero).
More concisely: The sequence of reciprocals of natural numbers tends to zero as the numbers approach infinity. (Mathematically expressed as: For every neighborhood of zero, there exists a natural number such that the reciprocals of all natural numbers greater than or equal to it lie within that neighborhood.)
|
tendsto_pow_atTop_nhds_0_of_lt_1
theorem tendsto_pow_atTop_nhds_0_of_lt_1 :
∀ {𝕜 : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : OrderTopology 𝕜] {r : 𝕜}, 0 ≤ r → r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem, `tendsto_pow_atTop_nhds_0_of_lt_1`, states that for any linearly ordered field `𝕜` that also has Archimedean, topological and order topology properties, if `r` is a non-negative number in `𝕜` that is less than 1, then the function `(fun n => r ^ n)`, which maps each number `n` to `r` raised to the power `n`, tends to zero as `n` tends to infinity. Stated differently, for larger and larger `n`, `r` to the power of `n` will get closer and closer to zero.
More concisely: For any Archimedean linearly ordered field `𝕜` with topology, if `0 < r < 1` is in `𝕜`, then `r^n` converges to 0 as `n` approaches infinity.
|
dist_le_of_le_geometric_of_tendsto₀
theorem dist_le_of_le_geometric_of_tendsto₀ :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ),
r < 1 →
∀ {f : ℕ → α},
(∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ C / (1 - r)
The theorem `dist_le_of_le_geometric_of_tendsto₀` states that given a sequence of elements in a pseudo metric space, denoted by `f : ℕ → α`, and two real numbers `r` and `C` such that `r` is less than `1`, if the distance between any two consecutive elements of the sequence is bounded by `C * r^n`, then the distance from the first element of the sequence to the limit of the sequence (as `n` approaches infinity) is bounded by `C / (1 - r)`. Here, the limit of a function or sequence is defined in the sense of filter: the function `f` tends to the limit `a` as `n` goes to infinity.
More concisely: Given a sequence `f : ℕ → α` in a pseudo metric space and `r, C ∈ ℝ` with `0 < 1 - r`, if `∀ i, d(f i, f (i+1)) ≤ C * r^(i+1)`, then `d(f 0, ∃ (l : α), ∀₁^∞. i, f i =₁ l) ≤ C / (1 - r)`.
|
NNReal.tendsto_inverse_atTop_nhds_0_nat
theorem NNReal.tendsto_inverse_atTop_nhds_0_nat : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
This theorem, `NNReal.tendsto_inverse_atTop_nhds_0_nat`, states that the sequence of reciprocals of natural numbers tends to zero. In mathematical terms, it demonstrates that as `n` goes to infinity, the reciprocal of `n` (notated as `(↑n)⁻¹` in Lean 4) approaches zero. This is expressed in Lean 4 using the `Filter.Tendsto` function, which encapsulates the idea of a limit of a function. Here, the function is the reciprocal function applied to natural numbers, the starting filter, `Filter.atTop`, represents the limit `n → ∞`, and the target filter, `nhds 0`, represents the neighborhood filter at zero, meaning we are examining the behavior of the function as it approaches zero.
More concisely: The sequence of reciprocal natural numbers converges to zero.
|
dist_le_of_le_geometric_two_of_tendsto₀
theorem dist_le_of_le_geometric_two_of_tendsto₀ :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (C : ℝ) {f : ℕ → α},
(∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → dist (f 0) a ≤ C
The theorem `dist_le_of_le_geometric_two_of_tendsto₀` states that for any pseudo metric space `α`, a real number `C`, and a sequence of points `f : ℕ → α` in the space, if the distance between each point in the sequence and the next (`dist (f n) (f (n + 1))`) is bounded by `(C / 2) / 2^n`, then the distance from the first point in the sequence `f 0` to the limit of the sequence is less than or equal to `C`. The limit of the sequence is defined with respect to the topology of the space, with the theorem requiring the sequence to converge to the limit `a` as `n` goes to infinity (`Filter.Tendsto f Filter.atTop (nhds a)`).
More concisely: Given a pseudo metric space `α`, a real number `C`, and a sequence `f : ℕ → α` in `α` such that `dist (f n) (f (n + 1))` is bounded by `(C / 2) / 2^n` for all `n ∈ ℕ`, the sequence `f` converges to some `a ∈ α` and `dist (f 0, a) ≤ C`.
|
tendsto_pow_atTop_nhds_0_iff
theorem tendsto_pow_atTop_nhds_0_iff :
∀ {𝕜 : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : OrderTopology 𝕜] {r : 𝕜}, Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0) ↔ |r| < 1
This theorem, known as an alias of `tendsto_pow_atTop_nhds_zero_iff`, states that for any linear ordered field 𝕜 (with the necessary conditions of being Archimedean and having a topological space structure and order topology), and for any element `r` of 𝕜, the function that maps `n` to `r^n` tends to zero as `n` tends to infinity (expressed as `Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)`) if and only if the absolute value of `r` is less than 1 (`|r| < 1`). In simple terms, the power of `r` tends to zero as `n` goes to infinity if `r` lies strictly between -1 and 1.
More concisely: For any Archimedean linear ordered field 𝕜 with topological structure and order topology, the function `r ^ n` tends to 0 as `n` approaches infinity if and only if `|r| < 1`.
|
cauchySeq_of_le_geometric
theorem cauchySeq_of_le_geometric :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (r C : ℝ),
r < 1 → ∀ {f : ℕ → α}, (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) → CauchySeq f
The theorem `cauchySeq_of_le_geometric` states that for any pseudo metric space `α`, given a real number `r` that is less than `1`, and any other real number `C`, if we have a sequence of elements in `α`, denoted as `f : ℕ → α`, such that the distance between each consecutive pair of elements in the sequence is bounded by `C` times `r` to the power `n` (where `n` is the index in the sequence), then the sequence `f` is a Cauchy sequence. This theorem does not require `C` or `r` to be non-negative. In the context of this theorem, a Cauchy sequence is a sequence where the elements get arbitrarily close to each other as the sequence progresses.
More concisely: Given a pseudo metric space and a real sequence where the distance between consecutive elements is bounded by a constant multiplied by the previous elements' indices raised to the power of a real number less than 1, the sequence is a Cauchy sequence.
|
cauchySeq_of_edist_le_geometric_two
theorem cauchySeq_of_edist_le_geometric_two :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal),
C ≠ ⊤ → ∀ {f : ℕ → α}, (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) → CauchySeq f
This theorem states that for any given sequence `f` of elements in a pseudo emetric space `α`, if the extended metric distance between consecutive terms of the sequence `f` (`edist (f n) (f (n+1))`) is bounded by a geometric sequence with ratio `1/2` (`C * 2^-n`), where `C` is a non-infinite extended nonnegative real number, then `f` is a Cauchy sequence.
In simpler words, this theorem is saying that if the "distance" between each term in a sequence and the next one is getting smaller quickly enough (specifically, if it's decreasing at least as fast as the terms of a geometric sequence where each term is half the previous one), then the sequence is a Cauchy sequence. A Cauchy sequence is one where the terms get arbitrarily close to each other as we go further and further along the sequence.
More concisely: If a sequence `f` in a pseudo metric space satisfies `edist (f n) (f (n+1)) ≤ C * 2^-n` for some constant `C`, then `f` is a Cauchy sequence.
|
NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat
theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat :
∀ (𝕜 : Type u_4) [inst : Semiring 𝕜] [inst_1 : Algebra NNReal 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : TopologicalSemiring 𝕜] [inst_4 : ContinuousSMul NNReal 𝕜],
Filter.Tendsto (⇑(algebraMap NNReal 𝕜) ∘ fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
The theorem `NNReal.tendsto_algebraMap_inverse_atTop_nhds_0_nat` states that for any type 𝕜 with a Semiring, Algebra, TopologicalSpace, TopologicalSemiring, and ContinuousSMul structure, the function that first takes the reciprocal of a non-negative natural number and then applies the algebra map from non-negative real numbers to 𝕜, tends to zero as n tends to infinity. In other words, the function that maps each natural number to the inverse of its embedding in 𝕜 tends to zero in the topological space 𝕜 when the natural number tends to infinity.
More concisely: For any semiring 𝕜 with a continuous algebra map from non-negative real numbers, the function that maps each non-negative natural number to the reciprocal of its embedding in 𝕜 and then applies the algebra map tend to zero in the topology of 𝕜 as the natural number goes to infinity.
|
tsum_geometric_inv_two_ge
theorem tsum_geometric_inv_two_ge : ∀ (n : ℕ), (∑' (i : ℕ), if n ≤ i then 2⁻¹ ^ i else 0) = 2 * 2⁻¹ ^ n
The theorem states that for any natural number `n`, the sum of the series where each term is `2⁻¹ ^ i` for all `i` such that `i` is greater than or equal to `n`, and `0` otherwise, equals `2 * 2⁻¹ ^ n`. Essentially, it establishes that the sum of the tail ends of a geometric series with a common ratio of `2⁻¹`, starting from the nth term, is `2 * 2⁻¹ ^ n`.
More concisely: For any natural number `n`, the sum of the geometric series with common ratio `1/2` starting from term `n` is equal to `2 * (1/2)^n`.
|
dist_le_of_le_geometric_two_of_tendsto
theorem dist_le_of_le_geometric_two_of_tendsto :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] (C : ℝ) {f : ℕ → α},
(∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C / 2 / 2 ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), dist (f n) a ≤ C / 2 ^ n
This theorem states that for any sequence of points `f` in a pseudometric space, and given a real number `C`, if the distance between each point `f n` and the next point `f (n+1)` is bounded by `(C / 2) / 2^n`, and if the sequence `f` converges to some point `a` in the limit as `n` approaches infinity, then the distance from each point `f n` to the limit `a` is bounded above by `C / 2^n`.
More concisely: Given any sequence `(f\_n)` in a pseudometric space that converges to a limit `a`, if the distance `d(f\_n, f\_(n+1))` is bounded by `C / 2 * 2^(-n)` for all `n`, then `d(f\_n, a)` is bounded above by `C / 2^n`.
|
tendsto_algebraMap_inverse_atTop_nhds_0_nat
theorem tendsto_algebraMap_inverse_atTop_nhds_0_nat :
∀ (𝕜 : Type u_4) [inst : Semiring 𝕜] [inst_1 : Algebra ℝ 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : TopologicalSemiring 𝕜] [inst_4 : ContinuousSMul ℝ 𝕜],
Filter.Tendsto (⇑(algebraMap ℝ 𝕜) ∘ fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
The theorem `tendsto_algebraMap_inverse_atTop_nhds_0_nat` asserts that for any type `𝕜` which is a semiring, an algebra over the real numbers, a topological space, a topological semiring, and has continuous scalar multiplication by the real numbers, the function that takes a natural number `n`, inverts it (i.e., computes `1/n`), then applies the algebraic embedding from the reals to `𝕜`, tends towards zero as `n` goes to infinity. In other words, the image of the sequence `1/n` under the algebraic embedding approaches zero in the topology of `𝕜` as `n` increases to infinity.
More concisely: For any semiring `𝕜` that is an algebra over the real numbers, has continuous scalar multiplication by the real numbers, and is a topological space with a topology making inversion and algebraic embedding continuous, the sequence of algebraic embeddings of `1/n` converges to zero in `𝕜` as `n` approaches infinity.
|
tendsto_one_div_atTop_nhds_0_nat
theorem tendsto_one_div_atTop_nhds_0_nat : Filter.Tendsto (fun n => 1 / ↑n) Filter.atTop (nhds 0)
This theorem, `tendsto_one_div_atTop_nhds_0_nat`, states that the sequence `1 / n`, where `n` is a natural number, tends to zero as `n` tends to infinity. In other words, as `n` increases without bound (`atTop`), the value of the function `1 / n` approaches zero (`nhds 0`). The theorem uses the `Filter.Tendsto` predicate, which is a formal way to express the concept of a limit in mathematics.
More concisely: The sequence `1 / n` converges to `0` as `n` approaches infinity.
|
uniformity_basis_dist_pow_of_lt_1
theorem uniformity_basis_dist_pow_of_lt_1 :
∀ {α : Type u_4} [inst : PseudoMetricSpace α] {r : ℝ},
0 < r → r < 1 → (uniformity α).HasBasis (fun x => True) fun k => {p | dist p.1 p.2 < r ^ k}
This theorem, referred to as `uniformity_basis_dist_pow_of_lt_1`, states that for any type `α` that has a `PseudoMetricSpace` structure, and any real number `r` between 0 and 1 (exclusive), the uniformity on `α` has a basis given by the set of pairs `(p.1, p.2)`, where the distance between `p.1` and `p.2` in the pseudometric space is less than `r` to the power of `k` for any `k`. This basis is such that every set in the basis contains the whole space `α`, as indicated by the function `(fun x => True)`.
More concisely: For any type `α` with a `PseudoMetricSpace` structure and real number `r` (0 < r), the basis of its uniformity consists of sets containing the whole space `α` and pairs of points with distance less than `r^k` for any `k`.
|
tsum_geometric_of_lt_1
theorem tsum_geometric_of_lt_1 : ∀ {r : ℝ}, 0 ≤ r → r < 1 → ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
This theorem, `tsum_geometric_of_lt_1`, states that for any real number `r` between 0 and 1 (inclusive of 0 and exclusive of 1), the sum of the infinite geometric series where each term is `r` raised to the power of `n` (where `n` is a natural number starting from 0) equals the reciprocal of `(1 - r)`. In mathematical notation, this is $\sum_{n=0}^\infty r^n = \frac{1}{1 - r}$. It is an alias of the theorem `tsum_geometric_of_lt_one`.
More concisely: The infinite geometric series with first term `r` and common ratio `r` (where `0 < r < 1`) equals the reciprocal of `(1 - r)`.
|
tendsto_const_div_atTop_nhds_zero_nat
theorem tendsto_const_div_atTop_nhds_zero_nat : ∀ (C : ℝ), Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0) := by
sorry
The theorem `tendsto_const_div_atTop_nhds_zero_nat` states that for any real constant `C`, as `n` tends to infinity (represented by `Filter.atTop`), the function defined as `C / n` tends to zero in the neighborhood filter (represented by `(nhds 0)`). In other words, the value of a constant divided by a natural number gets arbitrarily close to zero as that number goes towards infinity.
More concisely: For any real constant C, the sequence C / n converges to 0 in the neighborhood filter of 0 as n approaches infinity.
|
ENNReal.tsum_geometric
theorem ENNReal.tsum_geometric : ∀ (r : ENNReal), ∑' (n : ℕ), r ^ n = (1 - r)⁻¹
The theorem `ENNReal.tsum_geometric` states that for any extended nonnegative real number `r`, the infinite series of `r` raised to the power of `n`, as `n` ranges over the natural numbers, converges to the reciprocal of `(1 - r)`. Specifically, if `r` is less than 1, the right-hand side is a finite number, while if `r` is equal to or greater than 1, the right-hand side equals infinity. This is an extension of the geometric series formula to the case where `r` is an extended nonnegative real number.
More concisely: For any extended nonnegative real number `r`, the infinite geometric series $\sum\_{n=0}^{\infty} r^n$ converges to $\frac{1}{1-r}$, with the value being a finite number if $r < 1$ and infinity if $r \ge 1$.
|
edist_le_of_edist_le_geometric_two_of_tendsto
theorem edist_le_of_edist_le_geometric_two_of_tendsto :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α},
(∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ 2 * C / 2 ^ n
This theorem states that if the extended distance between `f n` and `f (n+1)` of a sequence `f` of elements in a pseudo-extended metric space is bounded by `C * 2^-n` for some constant `C`, and `f` tends to some limit `a` as `n` goes to infinity, then the extended distance from `f n` to the limit `a` is bounded above by `2 * C * 2^-n`. In other words, if the sequence `f` satisfies a certain kind of geometric decay property, then the approach of `f` to its limit `a` is also controlled in a similar way by the same rate of decay.
More concisely: If `f` is a sequence in a pseudo-extended metric space with the property that the extended distance between `f (n+1)` and `f n` is bounded by `C * 2^-n` for some constant `C`, and `f` converges to a limit `a`, then `dist(f n, a)` is bounded above by `2 * C * 2^-n`.
|
tendsto_pow_atTop_atTop_of_one_lt
theorem tendsto_pow_atTop_atTop_of_one_lt :
∀ {α : Type u_1} [inst : LinearOrderedRing α] [inst_1 : Archimedean α] {r : α},
1 < r → Filter.Tendsto (fun n => r ^ n) Filter.atTop Filter.atTop
This theorem states that for any type `α` that is a linear ordered ring and Archimedean (i.e., there is no infinite element), given any element `r` from `α` such that `r` is greater than 1, the function that raises `r` to the power `n` tends to infinity as `n` tends to infinity. In mathematical terms, if $1 < r$ for an `r` in an Archimedean linear ordered ring, then the limit as `n` goes to infinity of `r^n` is also infinity.
More concisely: In an Archimedean linear ordered ring, if $1 < r$, then $\lim\_{n \to \infty} r^n = \infty$.
|
edist_le_of_edist_le_geometric_two_of_tendsto₀
theorem edist_le_of_edist_le_geometric_two_of_tendsto₀ :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (C : ENNReal) {f : ℕ → α},
(∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C / 2 ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ 2 * C
The theorem `edist_le_of_edist_le_geometric_two_of_tendsto₀` states the following: Given a pseudoemetric space `α` and a function `f` from natural numbers to `α`, if the extended distance between `f(n)` and `f(n+1)` is bounded by `C * 2^-n` for some extended nonnegative real number `C`, and if `f` tends to a limit `a` as `n` tends to infinity, then the extended distance between `f(0)` and the limit `a` is bounded above by `2 * C`.
This can be seen as a geometric convergence condition: if the distances between successive terms of the sequence decrease geometrically, and the sequence is converging, then we can bound the distance from the first term to the limit of the sequence.
More concisely: Given a pseudometric space and a sequence in it with geometrically decreasing extended distances between successive terms that converge, the extended distance from the first term to the limit is bounded by twice the common bound on the geometric decay.
|
summable_geometric_of_lt_1
theorem summable_geometric_of_lt_1 : ∀ {r : ℝ}, 0 ≤ r → r < 1 → Summable fun n => r ^ n
The theorem `summable_geometric_of_lt_1` asserts that for any real number `r` between 0 and 1 (inclusive of 0 but exclusive of 1), the infinite geometric series whose common ratio is `r` is summable. In other words, the series $\sum_{n=0}^{\infty} r^n$ converges to a specific sum.
More concisely: For any real number `r` with `0 <= r < 1`, the infinite geometric series $\sum\_{n=0}^{\infty} r^n$ converges.
|
edist_le_of_edist_le_geometric_of_tendsto
theorem edist_le_of_edist_le_geometric_of_tendsto :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α},
(∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ C * r ^ n / (1 - r)
This theorem states that if the extended distance (`edist`) between `f(n)` and `f(n+1)` for a sequence of points `{f(n)}` in a pseudo-emetric space is bounded by `C * r^n`, where `C` and `r` are extended nonnegative real numbers (`ENNReal`), then the extended distance between `f(n)` and the limit `a` of the sequence `{f(n)}` is bounded above by `C * r^n / (1 - r)`. This limit is approached as `n` tends to infinity (`Filter.atTop`), which is assumed by the hypothesis `Filter.Tendsto f Filter.atTop (nhds a)`. Essentially, it provides an upper bound on the distance from `f(n)` to the limit `a` of the sequence `{f(n)}` in terms of a geometric series.
More concisely: If a sequence `{f(n)}` in a pseudo-metric space converges to `a` (`Filter.Tendsto f Filter.atTop (nhds a)`) and the extended distance between `f(n)` and `f(n+1)` is bounded by `C * r^n`, then the extended distance between `f(n)` and `a` is bounded above by `C * r^n / (1 - r)`.
|
aux_hasSum_of_le_geometric
theorem aux_hasSum_of_le_geometric :
∀ {α : Type u_1} [inst : PseudoMetricSpace α] {r C : ℝ},
r < 1 →
∀ {f : ℕ → α}, (∀ (n : ℕ), dist (f n) (f (n + 1)) ≤ C * r ^ n) → HasSum (fun n => C * r ^ n) (C / (1 - r))
This theorem, `aux_hasSum_of_le_geometric`, states that for any type `α` in a pseudo metric space, given a real number `r` less than 1 and any real number `C`, for any function `f` from natural numbers to `α`, if the distance between `f(n)` and `f(n+1)` is less than or equal to `C * r^n` for all natural numbers `n`, then the series of `C * r^n` converges (or has a sum) and the sum is `C / (1 - r)`. This theorem essentially formalizes a particular case of the geometric series convergence condition in the context of a pseudo metric space.
More concisely: In a pseudo metric space, if the distance between successive terms of a function is less than or equal to a constant times the previous term raised to the power of each index, then the sum of the series formed by those terms converges to the constant divided by (1 minus the common ratio).
|
cauchySeq_of_edist_le_geometric
theorem cauchySeq_of_edist_le_geometric :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal),
r < 1 → C ≠ ⊤ → ∀ {f : ℕ → α}, (∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) → CauchySeq f
The theorem `cauchySeq_of_edist_le_geometric` states that for any sequence `f` of elements in a pseudo emetric space `α`, if the extended metric distance between consecutive elements of the sequence, `edist (f n) (f (n+1))`, is bounded above by `C * r^n`, where `C` is a non-infinite extended nonnegative real number and `r` is an extended nonnegative real number less than 1, then `f` is a Cauchy sequence. This is a generalization of the concept of a geometric sequence to sequences in pseudo emetric spaces.
More concisely: If in a pseudo metric space, the extended metric distance between consecutive terms of a sequence is bounded above by a constant times the previous term raised to the power of the position, then the sequence is Cauchy.
|
NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one
theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one :
∀ {r : NNReal}, r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem states that for any nonnegative real number `r` less than one, the sequence `r^n` tends to zero as `n` tends to infinity. In other words, as `n` increases without bound, the values of `r^n` get arbitrarily close to zero. This is a formalization of the mathematical result that a geometric sequence with a common ratio in the open interval `(0, 1)` converges to zero.
More concisely: For any non-negative real number `r` with `0 < r < 1`, the sequence `[r^n | n : ℕ]` converges to 0 as `n` approaches infinity.
|
ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1
theorem ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1 :
∀ {r : ENNReal}, r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem, `ENNReal.tendsto_pow_atTop_nhds_0_of_lt_1`, states that for every extended nonnegative real number `r` which is less than 1, the function that raises `r` to the power of `n` (written as `r ^ n`) converges to 0 as `n` approaches infinity. In other words, the sequence of `r ^ n` values tends towards 0 when `n` becomes very large, if `r` is a nonnegative real number less than 1. This is a formal way of expressing the mathematical concept that a fraction less than 1 raised to an increasingly large exponent becomes arbitrarily close to 0.
More concisely: For every non-negative real number `r` strictly less than 1, the sequence `[r ^ n]_n` converges to 0 as `n` approaches infinity.
|
tendsto_atTop_of_geom_le
theorem tendsto_atTop_of_geom_le :
∀ {v : ℕ → ℝ} {c : ℝ},
0 < v 0 → 1 < c → (∀ (n : ℕ), c * v n ≤ v (n + 1)) → Filter.Tendsto v Filter.atTop Filter.atTop
This theorem states that if a sequence `v` of real numbers satisfies the condition that `k * v n ≤ v (n+1)` where `k` is greater than 1, and the first term of the sequence is positive, then the sequence diverges to positive infinity. In other words, the sequence `v` increases exponentially such that for every term, the next term in the sequence is at least `k` times greater. The sequence does not have an upper bound, hence it tends to positive infinity.
More concisely: If `k > 1` and `v` is a sequence of real numbers with `v_0 > 0` such that `k * v_n <= v_(n+1)` for all `n`, then `v` is an unbounded sequence.
|
hasSum_geometric_of_lt_one
theorem hasSum_geometric_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
This theorem states that if `r` is a real number such that `r` is greater than or equal to zero and less than one, then the sum of the infinite geometric series `r^n` (where `n` is a non-negative integer) is equal to `(1 - r)⁻¹`, which is the multiplicative inverse of `1 - r`.
In mathematical terms, this theorem asserts the well-known result that the sum of an infinite geometric series `r + r^2 + r^3 + ...` with a common ratio `r` between 0 and 1 (exclusive) is given by `1/(1 - r)`.
More concisely: The sum of an infinite geometric series with common ratio `r` in the open interval (0, 1) is equal to the multiplicative inverse of `1 - r`.
|
tendsto_pow_atTop_nhds_zero_of_lt_one
theorem tendsto_pow_atTop_nhds_zero_of_lt_one :
∀ {𝕜 : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : OrderTopology 𝕜] {r : 𝕜}, 0 ≤ r → r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem, `tendsto_pow_atTop_nhds_zero_of_lt_one`, states that for any linearly ordered field `𝕜` (which also has the structures of an Archimedean ordered set and a topological space with an order topology), if we have a non-negative element `r` that is less than 1, the function which maps a number `n` to `r^n` converges to 0 as `n` tends to infinity. In other words, for any sequence where each term is `r` raised to the index of the term in the sequence (`r^n`), as the term index goes to infinity (`Filter.atTop`), the term values get arbitrarily close to zero (`nhds 0`).
More concisely: For any Archimedean ordered field endowed with an order topology, if $0 < r < 1$, then $r^n$ converges to $0$ as $n$ approaches infinity.
|
summable_geometric_of_lt_one
theorem summable_geometric_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → Summable fun n => r ^ n
The theorem `summable_geometric_of_lt_one` states that for any real number `r` that is non-negative (`0 ≤ r`) and less than one (`r < 1`), the function mapping any natural number `n` to `r` raised to the power of `n` (`r ^ n`) is summable. In other words, the infinite geometric series $\sum_{n=0}^{\infty} r^n$ converges to a finite sum when the common ratio `r` is a real number in the interval [0, 1).
More concisely: For any non-negative real number `r` with `r < 1`, the infinite geometric series $\sum_{n=0}^{\infty} r^n$ converges to a finite sum.
|
tendsto_pow_atTop_nhdsWithin_0_of_lt_1
theorem tendsto_pow_atTop_nhdsWithin_0_of_lt_1 :
∀ {𝕜 : Type u_4} [inst : LinearOrderedField 𝕜] [inst_1 : Archimedean 𝕜] [inst_2 : TopologicalSpace 𝕜]
[inst_3 : OrderTopology 𝕜] {r : 𝕜},
0 < r → r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhdsWithin 0 (Set.Ioi 0))
The theorem `tendsto_pow_atTop_nhdsWithin_0_of_lt_1` states that for any linear ordered field 𝕜 that is also archimedean, topological and has order topology, and for any real number `r` between 0 and 1 (0 < r < 1), the sequence where each term is `r` raised to the power of the term's index tends to 0 as the index tends to infinity. This is within the neighborhood of 0 that is also inside the set of all real numbers greater than 0.
More concisely: For any archimedean, ordered topological field 𝕜 with 0 < r < 1, the sequence of powers r^n converges to 0 in the neighborhood of 0 within the positive real numbers.
|
NNReal.tendsto_pow_atTop_nhds_0_of_lt_1
theorem NNReal.tendsto_pow_atTop_nhds_0_of_lt_1 :
∀ {r : NNReal}, r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
This theorem, `NNReal.tendsto_pow_atTop_nhds_0_of_lt_1`, states that for any non-negative real number `r` that is less than 1, the function which maps a natural number `n` to `r` raised to the power of `n` tends to 0 as `n` approaches infinity. This is expressed using the `Filter.Tendsto` predicate, with `Filter.atTop` representing the limit `n` approaching infinity, and `nhds 0` representing a neighborhood of 0, which is the limit of the function as `n` goes to infinity.
More concisely: For any non-negative real number `r` with `0 < r < 1`, the sequence `{r ^ n | n : ℕ}` converges to 0 as `n` approaches infinity.
|
tendsto_inverse_atTop_nhds_zero_nat
theorem tendsto_inverse_atTop_nhds_zero_nat : Filter.Tendsto (fun n => (↑n)⁻¹) Filter.atTop (nhds 0)
The theorem `tendsto_inverse_atTop_nhds_zero_nat` states that the function that takes an integer `n` to its inverse `(↑n)⁻¹` (where `↑n` denotes the real number corresponding to the integer `n`), tends to 0 as `n` tends to infinity. In other words, as the input `n` becomes larger and larger, the output `(↑n)⁻¹` comes arbitrarily close to 0. This fits with our intuitive understanding from calculus, where the reciprocal of a large number is a small number close to zero.
More concisely: The sequence of numbers given by the reciprocal of the real numbers corresponding to natural numbers tends to 0 as the natural numbers approach infinity.
|
NNReal.hasSum_geometric
theorem NNReal.hasSum_geometric : ∀ {r : NNReal}, r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
The theorem `NNReal.hasSum_geometric` states that for any non-negative real number `r` that is less than 1, the sum of the geometric series where each term is `r` to the power of `n`, converges to the value `(1 - r)⁻¹`. In other words, the sum of the infinite geometric series $\sum_{n=0}^{\infty} r^n$ is equal to $\frac{1}{1 - r}$, for 0 ≤ `r` < 1.
More concisely: The theorem asserts that the sum of the infinite geometric series $\sum\_{n=0}^{\infty} r^n$ equals $\frac{1}{1 - r}$ for $0 \leq r < 1$.
|
hasSum_geometric_of_lt_1
theorem hasSum_geometric_of_lt_1 : ∀ {r : ℝ}, 0 ≤ r → r < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
This theorem, `hasSum_geometric_of_lt_1`, states that for any real number `r` that is greater than or equal to 0 and less than 1, the sum of the geometric series where each term is `r` raised to the power of `n` (the index of the term in the series), has a sum equal to the inverse of `(1 - r)`. This is an alias of the theorem `hasSum_geometric_of_lt_one` in Lean. In mathematical notation, this can be written as $\sum_{n=0}^{\infty} r^n = \frac{1}{1 - r}$ for $0 \leq r < 1$.
More concisely: The sum of the geometric series with first term `r` and common ratio `r`, where `0 ≤ r < 1`, equals the inverse of `(1 - r)`. In mathematical notation, $\sum\_{n=0}^{\infty} r^n = \frac{1}{1 - r}$.
|
NNReal.tendsto_const_div_atTop_nhds_0_nat
theorem NNReal.tendsto_const_div_atTop_nhds_0_nat :
∀ (C : NNReal), Filter.Tendsto (fun n => C / ↑n) Filter.atTop (nhds 0)
This theorem, referred to as `NNReal.tendsto_const_div_atTop_nhds_0_nat`, states that for every nonnegative real number `C`, the sequence defined by `C` divided by the natural number `n` tends to zero as `n` approaches infinity. In more mathematical terms, if we have a sequence $(a_n)$ where $a_n = \frac{C}{n}$ for a nonnegative real number $C$ and $n \in \mathbb{N}$, then $\lim_{n \to \infty} a_n = 0$. This is a standard result in real analysis, expressing the fact that the reciprocals of the natural numbers tend to zero.
More concisely: For any non-negative real number C, the sequence C / n converges to 0 as n approaches infinity.
|
edist_le_of_edist_le_geometric_of_tendsto₀
theorem edist_le_of_edist_le_geometric_of_tendsto₀ :
∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (r C : ENNReal) {f : ℕ → α},
(∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n) →
∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → edist (f 0) a ≤ C / (1 - r)
This theorem states that in a pseudoemetric space, if the extended distance between successive terms of a sequence `f` is bounded by a geometric progression `C * r^n`, then the extended distance from the first term of the sequence `f 0` to the limit of the sequence `f` is less than or equal to `C / (1 - r)`. In other words, if the changes in a sequence `f` decrease geometrically, then the total change from the initial term to the limit is bounded by a specific value depending on the rate of geometric decrease and the initial bounding constant. This theorem is a generalization of the formula for the sum of an infinite geometric series to sequences in a pseudoemetric space.
More concisely: In a pseudometric space, if the extended distance between successive terms of a sequence is bounded by a geometric progression, then the extended distance from the first term to the limit is less than or equal to the constant times the reciprocal of (1 minus the common ratio of the progression).
|