Lp is a complete space

In this file we show that Lp is a complete space for 1 ≤ p, in MeasureTheory.Lp.instCompleteSpace.

theorem MeasureTheory.Lp.eLpNorm'_lim_eq_lintegral_liminf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {p : ℝ} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : eLpNorm' f_lim p μ = (∫⁻ (a : α), Filter.liminf (fun (x : ι) => ‖f x a‖ₑ ^ p) Filter.atTop ∂μ) ^ (1 / p)

theorem MeasureTheory.Lp.eLpNorm'_lim_le_liminf_eLpNorm' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [SeminormedAddGroup E] {f : ℕ → α → E} {p : ℝ} (hp_pos : 0 < p) (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : eLpNorm' f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => eLpNorm' (f n) p μ) Filter.atTop

theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [LinearOrder ι] {f : ι → α → E} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : eLpNorm f_lim ⊤ μ = essSup (fun (x : α) => Filter.liminf (fun (m : ι) => ‖f m x‖ₑ) Filter.atTop) μ

theorem MeasureTheory.Lp.eLpNorm_exponent_top_lim_le_liminf_eLpNorm_exponent_top {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [SeminormedAddGroup E] {ι : Type u_3} [Nonempty ι] [Countable ι] [LinearOrder ι] {f : ι → α → E} {f_lim : α → E} (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ι) => f n x) Filter.atTop (nhds (f_lim x))) : eLpNorm f_lim ⊤ μ ≤ Filter.liminf (fun (n : ι) => eLpNorm (f n) ⊤ μ) Filter.atTop

theorem MeasureTheory.Lp.eLpNorm_lim_le_liminf_eLpNorm {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [SeminormedAddGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (f_lim : α → E) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : eLpNorm f_lim p μ ≤ Filter.liminf (fun (n : ℕ) => eLpNorm (f n) p μ) Filter.atTop

theorem MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [SeminormedAddGroup E] {ι : Type u_3} {u : Filter ι} [u.NeBot] [u.IsCountablyGenerated] {f : ι → α → E} {g : α → E} {C : ENNReal} (bound : ∀ᶠ (n : ι) in u, eLpNorm (f n) p μ ≤ C) (hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ) (h_tendsto : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (x_1 : ι) => f x_1 x) u (nhds (g x))) : eLpNorm g p μ ≤ C

If the eLpNorm of a collection of AEStronglyMeasurable functions that converges almost everywhere is bounded by some constant C, then the eLpNorm of its limit is also bounded by C.

Lp is complete iff Cauchy sequences of ℒp have limits in ℒp

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → ↥(Lp E p μ)) (f_lim : ↥(Lp E p μ)) : Filter.Tendsto f fi (nhds f_lim) ↔ Filter.Tendsto (fun (n : ι) => eLpNorm (↑↑(f n) - ↑↑f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → ↥(Lp E p μ)) (f_lim : α → E) (f_lim_ℒp : MemLp f_lim p μ) : Filter.Tendsto f fi (nhds (MemLp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm'' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [Fact (1 ≤ p)] (f : ι → α → E) (f_ℒp : ∀ (n : ι), MemLp (f n) p μ) (f_lim : α → E) (f_lim_ℒp : MemLp f_lim p μ) : Filter.Tendsto (fun (n : ι) => MemLp.toLp (f n) ⋯) fi (nhds (MemLp.toLp f_lim f_lim_ℒp)) ↔ Filter.Tendsto (fun (n : ι) => eLpNorm (f n - f_lim) p μ) fi (nhds 0)

theorem MeasureTheory.Lp.tendsto_Lp_of_tendsto_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {ι : Type u_4} {fi : Filter ι} [Fact (1 ≤ p)] {f : ι → ↥(Lp E p μ)} (f_lim : α → E) (f_lim_ℒp : MemLp f_lim p μ) (h_tendsto : Filter.Tendsto (fun (n : ι) => eLpNorm (↑↑(f n) - f_lim) p μ) fi (nhds 0)) : Filter.Tendsto f fi (nhds (MemLp.toLp f_lim f_lim_ℒp))

theorem MeasureTheory.Lp.cauchySeq_Lp_iff_cauchySeq_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {ι : Type u_4} [Nonempty ι] [SemilatticeSup ι] [hp : Fact (1 ≤ p)] (f : ι → ↥(Lp E p μ)) : CauchySeq f ↔ Filter.Tendsto (fun (n : ι × ι) => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) Filter.atTop (nhds 0)

theorem MeasureTheory.Lp.completeSpace_lp_of_cauchy_complete_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] [hp : Fact (1 ≤ p)] (H : ∀ (f : ℕ → α → E), (∀ (n : ℕ), MemLp (f n) p μ) → ∀ (B : ℕ → ENNReal), ∑' (i : ℕ), B i < ⊤ → (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) → ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) : CompleteSpace ↥(Lp E p μ)

Prove that controlled Cauchy sequences of ℒp have limits in ℒp

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm' {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} {p : ℝ} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (hp1 : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm' (f n - f m_1) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

theorem MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (hp : 1 ≤ p) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) : ∀ᵐ (x : α) ∂μ, ∃ (l : E), Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds l)

theorem MeasureTheory.Lp.cauchy_tendsto_of_tendsto {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] {f : ℕ → α → E} (hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ) (f_lim : α → E) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) (h_lim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (f_lim x))) : Filter.Tendsto (fun (n : ℕ) => eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)

theorem MeasureTheory.Lp.memLp_of_cauchy_tendsto {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ (n : ℕ), MemLp (f n) p μ) (f_lim : α → E) (h_lim_meas : AEStronglyMeasurable f_lim μ) (h_tendsto : Filter.Tendsto (fun (n : ℕ) => eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)) : MemLp f_lim p μ

theorem MeasureTheory.Lp.cauchy_complete_eLpNorm {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] (hp : 1 ≤ p) {f : ℕ → α → E} (hf : ∀ (n : ℕ), MemLp (f n) p μ) {B : ℕ → ENNReal} (hB : ∑' (i : ℕ), B i ≠ ⊤) (h_cau : ∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → eLpNorm (f n - f m_1) p μ < B N) : ∃ (f_lim : α → E), MemLp f_lim p μ ∧ Filter.Tendsto (fun (n : ℕ) => eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0)

instance MeasureTheory.Lp.instCompleteSpace {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {E : Type u_3} [NormedAddCommGroup E] [CompleteSpace E] [hp : Fact (1 ≤ p)] : CompleteSpace ↥(Lp E p μ)

Lp is complete for 1 ≤ p.