Compactness Gradient Restriction #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.inner_indicator_eq_restricted_inner
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ : MeasureTheory.Measure α}
(S : Set α)
(hS : MeasurableSet S)
(f : α → E)
(hf : MeasureTheory.MemLp f 2 μ)
(w : ↥(MeasureTheory.Lp E 2 (μ.restrict S)))
:
inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp (S.indicator fun (x : α) => ↑↑w x) ⋯) = inner ℝ (MeasureTheory.MemLp.toLp f ⋯) w
Pairing with a test extended by zero identifies the full-space and restricted L² Hilbert pairings.
theorem
CKN.Leray.weak_l2_restrict_of_weak_l2
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ : MeasureTheory.Measure α}
(S : Set α)
(hS : MeasurableSet S)
(f : ℕ → α → E)
(g : ↥(MeasureTheory.Lp E 2 μ))
(hf : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 μ)
(hweak :
∀ (v : ↥(MeasureTheory.Lp E 2 μ)),
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f k) ⋯) v) Filter.atTop (nhds (inner ℝ g v)))
(w : ↥(MeasureTheory.Lp E 2 (μ.restrict S)))
:
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f k) ⋯) w) Filter.atTop
(nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : α) => ↑↑g x) ⋯) w))
Weak L² convergence passes from a measure to its restriction to a measurable set.
theorem
CKN.Leray.weak_l2_of_measure_eq
{α : Type u_1}
{E : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{μ ν : MeasureTheory.Measure α}
(hμ : μ = ν)
(f : ℕ → α → E)
(g : α → E)
(hfμ : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 μ)
(hgμ : MeasureTheory.MemLp g 2 μ)
(hfν : ∀ (k : ℕ), MeasureTheory.MemLp (f k) 2 ν)
(hgν : MeasureTheory.MemLp g 2 ν)
(hweak :
∀ (w : ↥(MeasureTheory.Lp E 2 μ)),
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f k) ⋯) w) Filter.atTop
(nhds (inner ℝ (MeasureTheory.MemLp.toLp g hgμ) w)))
(w : ↥(MeasureTheory.Lp E 2 ν))
:
Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (f k) ⋯) w) Filter.atTop
(nhds (inner ℝ (MeasureTheory.MemLp.toLp g hgν) w))
Weak L² convergence is unchanged when two measures are equal.