Data and divergence clauses for the forced limit

The data clauses and the divergence identity of def:sws for the forced limit in the proof of thm:leray-forced. They use only the energy class, the weak-gradient and divergence clauses shared by def:forced-leray-hopf and def:leray-hopf, the local pressure integrability, and the assumed local integrability of the force.

theorem CKN.Leray.forcedAssembly_pairing_tendsto_of_strong_two {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (F : ℕ → α → ℝ) (G w : α → ℝ) (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ) (hw : MeasureTheory.MemLp w 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (F n - G) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * w x ∂μ) Filter.atTop (nhds (∫ (x : α), G x * w x ∂μ))

Strong L² convergence passes to the pairing with a fixed L² field.

theorem CKN.Leray.forcedAssembly_divergence_pairing_zero {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {f u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsForcedLerayHopfSolution T a f u Du) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * spatialPartialProd g i z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The weak-divergence clause of a forced Leray--Hopf solution pairs to zero with any compact smooth scalar test on the finite-time product slab.

theorem CKN.Leray.forcedAssembly_hopfDivergence {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {f u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hglobal : ∀ (T : ℝ), 0 < T → IsForcedLerayHopfSolution T a f u Du) (ψ : Foundation.Parabolic.ParabolicPoint → ℝ) (hψ : ψ ∈ spaceTimeTestFunction Set.univ (Set.Ioi 0)) : ∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioi 0), ∑ i : Fin 3, u z i * spatialPartial ψ i z = 0

The divergence identity of def:sws on positive time follows from the every-slab forced Leray--Hopf weak-divergence clause.

theorem CKN.Leray.forcedAssembly_hopfData {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {f u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} (hglobal : ∀ (T : ℝ), 0 < T → IsForcedLerayHopfSolution T a f u Du) (hp : ∀ (Ω' : Set Foundation.Parabolic.Vec3) (J : Set ℝ), localBox Set.univ (Set.Ioi 0) Ω' J → MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) {q : ℝ} (hq : 5 / 2 < q) (hfq : IsLocallyQIntegrableForce q f) : IsSuitableWeakSolutionData Set.univ (Set.Ioi 0) q u Du p f

A global forced Leray--Hopf pair, local L^{3/2} pressure integrability and local L^q integrability of the force give the data clauses of def:sws on the positive-time half space.