Compactness Gradient Pairing #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.tendsto_integral_of_strong_l2
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(F : ℕ → α → E)
(G : α → E)
(hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ)
(hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 μ) Filter.atTop (nhds 0))
:
Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x ∂μ) Filter.atTop (nhds (∫ (x : α), G x ∂μ))
Strong L² convergence on a finite-measure space passes to Bochner
integrals.
theorem
CKN.Leray.tendsto_integral_mul_test_of_strong_l2
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[NormedSpace ℝ E]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(F : ℕ → α → E)
(G : α → E)
(φ : α → ℝ)
(hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ)
(hφ : MeasureTheory.MemLp φ ⊤ μ)
(hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 μ) Filter.atTop (nhds 0))
:
A bounded scalar multiplier preserves convergence of integrals under
strong L² convergence.
theorem
CKN.Leray.tendsto_setIntegral_mul_test_of_strong_l2
{α : Type u_1}
[MeasurableSpace α]
(μ : MeasureTheory.Measure α)
[MeasureTheory.IsFiniteMeasure μ]
(F : ℕ → α → ℝ)
(G φ : α → ℝ)
(S : Set α)
(hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ)
(hφ : MeasureTheory.MemLp φ ⊤ μ)
(hS : MeasurableSet S)
(hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 μ) Filter.atTop (nhds 0))
:
A bounded test on a measurable subset preserves strong L² convergence
of scalar pairings.