Compactness Lp

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.tendsto_eLpNorm_of_tendstoInMeasure_of_uniform_high {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p r : ENNReal} {f : ℕ → α → E} (hp : 1 ≤ p) (hpr : p < r) (hr : r ≠ ⊤) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) r μ) (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) r μ ≤ B) (hmeasure : MeasureTheory.TendstoInMeasure μ f Filter.atTop fun (x : α) => 0) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n) p μ) Filter.atTop (nhds 0)

On a finite measure space, convergence in measure and a uniform bound in a strictly higher finite exponent imply convergence in every intermediate Lᵖ seminorm. This is the interpolation step in cor:compactness-Lq.

theorem CKN.Leray.tendsto_eLpNorm_sub_of_tendsto_eLpNorm_two_of_uniform_high {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p r : ENNReal} {f : ℕ → α → E} {g : α → E} (hp : 1 ≤ p) (hpr : p < r) (hr : r ≠ ⊤) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) r μ) (hg : MeasureTheory.MemLp g r μ) (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) r μ ≤ B) (h2 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)

Strong local L² convergence and a uniform bound in a higher finite exponent imply convergence in every intermediate exponent. This is the upgrade used in cor:compactness-Lq.

theorem CKN.Leray.tendsto_eLpNorm_sub_of_tendsto_two_of_uniform_high {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {p r : ENNReal} {f : ℕ → α → E} {g : α → E} (hp : 1 ≤ p) (hpr : p < r) (hr : r ≠ ⊤) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) r μ) (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) r μ ≤ B) (h2 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)) : MeasureTheory.MemLp g r μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)

Strong L² convergence and a uniform higher-exponent bound pass that bound to the limit and yield strong convergence at every intermediate exponent. This is the Fatou and interpolation step in cor:compactness-Lq.

theorem CKN.Leray.tendsto_eLpNorm_sub_of_tendsto_two_of_uniform_ten_thirds {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → α → E} {g : α → E} (hbound : ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) (10 / 3) μ ≤ B) (h2 : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)) (p : ENNReal) : 1 ≤ p → p < 10 / 3 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)

Strong local L² convergence and a uniform local L^(10/3) bound imply strong local Lᵖ convergence for every 1 ≤ p < 10/3. This is the upgrade in cor:compactness-Lq.

theorem CKN.Leray.cor_compactness_Lq {α : Type u_1} {E : Type u_2} {ι : Type u_3} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : ℕ → α → E} {g : α → E} (Q : ι → Set α) [∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ.restrict (Q i))] (hbound : ∀ (i : ι), ∃ B < ⊤, ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) (10 / 3) (μ.restrict (Q i)) ≤ B) (h2 : ∀ (i : ι), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 (μ.restrict (Q i))) Filter.atTop (nhds 0)) (i : ι) (p : ENNReal) : 1 ≤ p → p < 10 / 3 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) p (μ.restrict (Q i))) Filter.atTop (nhds 0)

On each member of a family of finite-measure local regions, strong L² convergence and a uniform L^(10/3) bound imply strong Lᵖ convergence for every 1 ≤ p < 10/3. Applied to compact subsets, this is cor:compactness-Lq.