# `Lp` is a complete space #

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

source
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)
source
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
source
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) μ
source
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
source
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` #

source
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)
source
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)
source
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)
source
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))
source
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)
source
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` #

source
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)
source
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)
source
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)
source
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 μ
source
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)
source
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`.