Weak continuity of the Leray–Hopf limit

This is the weak-continuity clause (LH2) of def:leray-hopf in the proof of prop:leray-hopf-limit. Every slice of the limit lies in the L² closure of smooth, compactly supported, divergence-free fields. Pairings with such fields are Lipschitz in time by the uniform modulus of lem:reg-equicontinuity, and the uniform energy bound extends continuity to every L² field: the component orthogonal to the solenoidal fields pairs to zero.

theorem CKN.Leray.lerayHopfLimit_continuousOn_inner_of_mem_closure_span {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] (S : Set E) (T M : ℝ) (hM : 0 ≤ M) (v : ℝ → E) (hbound : ∀ t ∈ Set.Icc 0 T, ‖v t‖ ≤ M) (hmem : ∀ t ∈ Set.Icc 0 T, v t ∈ (Submodule.span ℝ S).topologicalClosure) (hcont : ∀ s ∈ S, ContinuousOn (fun (t : ℝ) => inner ℝ (v t) s) (Set.Icc 0 T)) (W : E) : ContinuousOn (fun (t : ℝ) => inner ℝ (v t) W) (Set.Icc 0 T)

Continuity of the pairings on a spanning family extends to all tests when the curve stays bounded in the closed span of the family.

def CKN.Leray.lerayHopfLimitSolenoidalTests : Set ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)

The Euclidean L² elements of smooth, compactly supported, divergence-free coordinate fields.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Leray.lerayHopfLimit_mem_closure_solenoidalTests {f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (hf : IsWeakDivFreeL2 f) : MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) ⋯ ∈ closure lerayHopfLimitSolenoidalTests

Every weakly divergence-free L² field lies in the closure of the smooth compactly supported solenoidal tests.

theorem CKN.Leray.lerayHopfLimit_limitPairing_lipschitz (P : ℕ → ℝ → ℝ) (Q : ℝ → ℝ) (K : ℝ) (hmod : ∀ (n : ℕ) (s t : ℝ), 0 ≤ s → 0 ≤ t → |P n t - P n s| ≤ K * |t - s|) (hconv : ∀ (t : ℝ), 0 ≤ t → Filter.Tendsto (fun (n : ℕ) => P n t) Filter.atTop (nhds (Q t))) (s t : ℝ) : 0 ≤ s → 0 ≤ t → |Q t - Q s| ≤ K * |t - s|

A Lipschitz bound for approximating pairings passes to their pointwise limits.

theorem CKN.Leray.lerayHopfLimit_weakContinuity (T : ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (M : ℝ) (hM : 0 ≤ M) (hdiv : ∀ (t : ℝ), 0 ≤ t → IsWeakDivFreeL2 fun (x : Foundation.Parabolic.Vec3) => u (x, t)) (hnorm : ∀ (t : ℝ) (ht : 0 ≤ t), ‖MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (x, t))) ⋯‖ ≤ M) (hmod : ∀ (wc : Fin 3 → Foundation.Parabolic.Vec3 → ℝ), (∀ (i : Fin 3), ContDiff ℝ (↑⊤) (wc i)) → (∀ (i : Fin 3), HasCompactSupport (wc i)) → (∀ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, spatialDeriv (wc i) i x = 0) → ∃ (K : ℝ), ∀ (s t : ℝ), 0 ≤ s → 0 ≤ t → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * wc i x) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, s) i * wc i x| ≤ K * |t - s|) (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : MeasureTheory.MemLp w 2 MeasureTheory.volume → ContinuousOn (fun (t : ℝ) => ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i) (Set.Icc 0 T)

The weak-continuity clause (LH2): if every slice is a weakly divergence-free L² field with a uniform bound, and the pairings with smooth compactly supported solenoidal fields are Lipschitz in time, then the pairing with every L² field is continuous on [0,T].