Dominated convergence in Lᵖ

For a finite nonzero exponent q, if the functions f n converge to g almost everywhere and the errors ‖f n - g‖ₑ are eventually dominated by a fixed nonnegative multiple of the enorm of a MemLp function, then f n → g in the Lᵖ seminorm. In particular, this applies when truncating a function by cutoffs that are eventually 1 on every bounded set. The dominating function's codomain only needs a topology and an extended norm.

Main declarations

• TauCeti.tendsto_eLpNorm_sub_of_ae_tendsto: the convergence eLpNorm (f n - g) q m → 0.

theorem TauCeti.tendsto_eLpNorm_sub_of_ae_tendsto {α : Type u_1} {ι : Type u_2} {F : Type u_3} {G : Type u_4} [MeasurableSpace α] {m : MeasureTheory.Measure α} [SeminormedAddGroup F] [IsTopologicalAddGroup F] [TopologicalSpace G] [ENorm G] {l : Filter ι} [l.IsCountablyGenerated] {q : ENNReal} (hq0 : q ≠ 0) (hq : q ≠ ⊤) {f : ι → α → F} {g : α → F} (hf : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (f n) m) (hg : MeasureTheory.AEStronglyMeasurable g m) {bound : α → G} (hb : MeasureTheory.MemLp bound q m) {C : NNReal} (hbound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : α) ∂m, ‖f n x - g x‖ₑ ≤ ↑C * ‖bound x‖ₑ) (hlim : ∀ᵐ (x : α) ∂m, Filter.Tendsto (fun (n : ι) => f n x) l (nhds (g x))) : Filter.Tendsto (fun (n : ι) => MeasureTheory.eLpNorm (f n - g) q m) l (nhds 0)

Dominated convergence in Lᵖ. For a finite nonzero exponent, if f n converges to g at almost every point and ‖f n - g‖ₑ is eventually dominated by a fixed nonnegative multiple of the enorm of a MemLp function, then f n → g in the Lᵖ seminorm. The dominating function may take values in any topological space with an extended norm. Both the measurability of f n and the domination are only needed eventually along l. The limit needs only to be a.e. strongly measurable; the dominating function supplies the integrability of the errors.