Theorems · Theorem · real analysis

tendsto_tsum_of_dominated_convergence

∀ {α : Type u_1} {β : Type u_2} {G : Type u_3} {𝓕 : Filter α} [inst : NormedAddCommGroup G] [CompleteSpace G]
  {f : α → β → G} {g : β → G} {bound : β → ℝ},
  Summable bound →
    (∀ (k : β), Filter.Tendsto (fun x => f x k) 𝓕 (nhds (g k))) →
      (∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k) →
        Filter.Tendsto (fun x => ∑' (k : β), f x k) 𝓕 (nhds (∑' (k : β), g k))

Tannery's theorem: topological sums commute with termwise limits, when the norms of the summands are eventually uniformly bounded by a summable function. (This is the special case of the Lebesgue dominated convergence theorem for the counting measure on a discrete set. However, we prove it under somewhat weaker assumptions than the general measure-theoretic result, e.g. G is not assumed to be an ℝ-vector space or second countable, and the limit is along an arbitrary filter rather than atTop ℕ.) See also: * MeasureTheory.tendsto_integral_of_dominated_convergence (for general integrals, but with more assumptions on G) * continuous_tsum (continuity of infinite sums in a parameter)

Defined in

Mathlib.Analysis.Normed.Group.Tannery

Cited by

2 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupCompleteSpace