Almost everywhere convergence along a subsequence

If the Lebesgue integrals of nonnegative functions F n : α → ℝ≥0∞ tend to 0, then along a subsequence the functions themselves tend to 0 almost everywhere. Choose the subsequence with integrals below 2⁻ʲ: the sum ∑ⱼ F (φ j) then has finite integral, so it is finite almost everywhere, and its terms tend to 0 there.

Applied to the p-th powers of the errors of fields converging in Lᵖ, the same sum, plus the p-th power of the limit, dominates the p-th powers of the fields along the subsequence, since ‖x‖ᵖ ≤ 2ᵖ⁻¹ (‖a‖ᵖ + ‖x - a‖ᵖ).

Main statements

• TauCeti.exists_strictMono_lintegral_tsum_ne_top_of_tendsto_lintegral: a subsequence of functions whose integrals tend to 0 has a sum with finite integral.
• TauCeti.exists_strictMono_ae_tendsto_zero_of_tendsto_lintegral: a subsequence of functions whose integrals tend to 0 tends to 0 almost everywhere.
• TauCeti.exists_strictMono_enorm_pow_le_and_ae_tendsto_of_tendsto_lintegral: fields converging in Lᵖ converge almost everywhere along a subsequence, along which their p-th powers have a common integrable majorant.

theorem TauCeti.exists_strictMono_lintegral_tsum_ne_top_of_tendsto_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} (hF : ∀ (n : ℕ), AEMeasurable (F n) μ) (h : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∫⁻ (a : α), ∑' (j : ℕ), F (φ j) a ∂μ ≠ ⊤

A subsequence with summable integrals. If F n : α → ℝ≥0∞ are almost everywhere measurable and ∫⁻ F n ∂μ → 0, then along a subsequence the sum ∑ⱼ F (φ j) has finite integral. It dominates every F (φ j), which makes it a common integrable bound for a dominated convergence argument along the subsequence.

theorem TauCeti.exists_strictMono_ae_tendsto_zero_of_tendsto_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ℕ → α → ENNReal} (hF : ∀ (n : ℕ), AEMeasurable (F n) μ) (h : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (a : α), F n a ∂μ) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun (j : ℕ) => F (φ j) a) Filter.atTop (nhds 0)

A subsequence converging almost everywhere. If F n : α → ℝ≥0∞ are almost everywhere measurable and ∫⁻ F n ∂μ → 0, then along a subsequence F (φ j) a → 0 for almost every a.

theorem TauCeti.exists_strictMono_enorm_pow_le_and_ae_tendsto_of_tendsto_lintegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {E : Type u_2} [SeminormedAddCommGroup E] {p : ℕ} (hp : p ≠ 0) {Ω : Set α} (hΩ : MeasurableSet Ω) {U : ℕ → Set α} (hU : ∀ (k : ℕ), MeasurableSet (U k)) (hUΩ : ∀ (k : ℕ), U k ⊆ Ω) (hΩU : ∀ y ∈ Ω, ∀ᶠ (k : ℕ) in Filter.atTop, y ∈ U k) {F : ℕ → α → E} (hF : ∀ (k : ℕ), MeasureTheory.AEStronglyMeasurable (F k) (μ.restrict (U k))) {H : α → E} (hHm : MeasureTheory.AEStronglyMeasurable H (μ.restrict Ω)) (hH : ∫⁻ (y : α) in Ω, ‖H y‖ₑ ^ p ∂μ ≠ ⊤) (hFH : Filter.Tendsto (fun (k : ℕ) => ∫⁻ (y : α) in U k, ‖F k y - H y‖ₑ ^ p ∂μ) Filter.atTop (nhds 0)) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∃ (G : α → ENNReal), ∫⁻ (y : α), G y ∂μ ≠ ⊤ ∧ ∀ (j : ℕ), ∀ y ∈ U (φ j), ‖F (φ j) y‖ₑ ^ p ≤ G y) ∧ ∀ᵐ (y : α) ∂μ, y ∈ Ω → Filter.Tendsto (fun (j : ℕ) => F (φ j) y) Filter.atTop (nhds (H y))

A common majorant along a subsequence. Let F k be fields converging to H in Lᵖ on measurable sets U k ⊆ Ω, p ≠ 0 a natural number, with ‖H‖ ∈ Lᵖ(Ω), and let every point of Ω lie in U k for all large k. Then along a subsequence the powers ‖F (φ j)‖ᵖ on U (φ j) have a common integrable majorant, and F (φ j) → H almost everywhere on Ω.