Filter.Tendsto.cesaro_smul
theorem Filter.Tendsto.cesaro_smul :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {u : ℕ → E} {l : E},
Filter.Tendsto u Filter.atTop (nhds l) →
Filter.Tendsto (fun n => (↑n)⁻¹ • (Finset.range n).sum fun i => u i) Filter.atTop (nhds l)
The theorem `Filter.Tendsto.cesaro_smul` states that if a sequence `u` of elements in a normed additive commutative group `E` over the real numbers converges to a limit `l` as `n` approaches infinity, then the Cesàro average of the sequence also converges to the same limit `l` as `n` approaches infinity. Here, the Cesàro average of the sequence `u` is defined as the mean of the first `n` terms of the sequence, `(Finset.range n).sum fun i => u i)`, scaled by the reciprocal of `n`, `(↑n)⁻¹`. In other words, this theorem establishes that the limit of the averages of the initial segments of a sequence is the same as the limit of the sequence, given the sequence converges.
More concisely: If a sequence in a normed additive commutative group over the real numbers converges, then its Cesàro averages converge to the same limit.
|
Filter.Tendsto.cesaro
theorem Filter.Tendsto.cesaro :
∀ {u : ℕ → ℝ} {l : ℝ},
Filter.Tendsto u Filter.atTop (nhds l) →
Filter.Tendsto (fun n => (↑n)⁻¹ * (Finset.range n).sum fun i => u i) Filter.atTop (nhds l)
The theorem `Filter.Tendsto.cesaro` states that for any real-valued sequence `u` that converges to a real number `l` as `n` approaches infinity, the Cesaro average of the sequence (which is the average of the first `n` terms of the sequence) also converges to the same limit `l` as `n` approaches infinity. This is a formal mathematical statement about the property of Cesaro summability, which is a technique used to assign values to infinite series that might not have a conventional sum.
More concisely: If a real-valued sequence converges to a limit, then its Cesaro average also converges to the same limit.
|
Filter.IsBoundedUnder.isLittleO_sub_self_inv
theorem Filter.IsBoundedUnder.isLittleO_sub_self_inv :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : Norm E] {a : 𝕜} {f : 𝕜 → E},
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) (nhdsWithin a {a}ᶜ) (norm ∘ f) →
f =o[nhdsWithin a {a}ᶜ] fun x => (x - a)⁻¹
The theorem `Filter.IsBoundedUnder.isLittleO_sub_self_inv` states that if a function `f` from a normed field `𝕜` to a normed space `E` is bounded in a punctured neighborhood of a point `a` (i.e., the neighborhood of `a` excluding `a` itself), then the function `f(x)` is little-o of `(x - a)⁻¹` as `x` approaches `a`, but `x` is not equal to `a`. In other words, `f(x)` becomes insignificant compared to `(x - a)⁻¹` as `x` gets arbitrarily close to `a`, making `f(x)` grow at a much slower rate than `(x - a)⁻¹`.
More concisely: If a function `f` from a normed field to a normed space is bounded in a punctured neighborhood of a point `a`, then `f(x) = o((x - a)⁻¹)` as `x → a`, `x ≠ a`, where `o` denotes little-o notation.
|