Leray–Hopf clauses from strong L² continuity

The last step of prop:pv-local-solution: a finite-energy weak solution with pressure in space-time L⁵ on ℝ³ × (0, T) whose time slices are square integrable and continuous into L² on [0, T], with the datum as its slice at t = 0, is a Leray–Hopf solution. The energy equality, which holds at almost every time in the L⁵ class, extends to every time by continuity of both sides; it gives the energy inequality of def:leray-hopf, and the strong L² continuity gives the weak continuity and the strong initial trace.

theorem ESS.pvLH_component_eLpNorm_le {f : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (k : Fin 3) : MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f x k) 2 MeasureTheory.volume ≤ MeasureTheory.eLpNorm f 2 MeasureTheory.volume

A component of a square-integrable vector field has at most its norm.

theorem ESS.pvLH_pair_le {f g : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, f x k * g x k| ≤ 3 * ((MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal)

The L² pairing of vector fields is bounded by three times the product of their (sup-norm) L² norms.

theorem ESS.pvLH_pairing_continuousOn {T : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hmem : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc 0 T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, s) - U (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc 0 T)) (nhds 0)) {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hw : MeasureTheory.MemLp w 2 MeasureTheory.volume) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * w x i) (Set.Icc 0 T)

Strong L² continuity gives continuity of the pairing with every square integrable field.

theorem ESS.pvLH_sq_continuousOn {T : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hmem : ∀ t ∈ Set.Icc 0 T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, t)) 2 MeasureTheory.volume) (hcont : ∀ t ∈ Set.Icc 0 T, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, s) - U (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc 0 T)) (nhds 0)) : ContinuousOn (fun (t : ℝ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, U (x, t) k * U (x, t) k) (Set.Icc 0 T)

Strong L² continuity gives continuity of the squared L² norm.

theorem ESS.pvLH_dissipation_continuousOn {T : ℝ} {DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hT : 0 ≤ T) (hDU : MeasureTheory.MemLp DU 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ContinuousOn (fun (t : ℝ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, DU q k j * DU q k j) (Set.Icc 0 T)

The dissipation integral over ℝ³ × (0, t) is continuous in t ∈ [0, T].