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 α} [NormedAddCommGroup 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 α} [NormedAddCommGroup 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 α} [NormedAddCommGroup 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 α} [NormedAddCommGroup 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 α} [NormedAddCommGroup 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

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

theorem MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {ι : Type u_3} {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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {ι : Type u_3} {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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {ι : Type u_3} {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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {ι : Type u_3} {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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] {ι : Type u_3} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [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} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NormedAddCommGroup E] [CompleteSpace E] [hp : Fact (1 ≤ p)] : CompleteSpace ↥(Lp E p μ)

Lp is complete for 1 ≤ p.