The strong equation at almost every time

Testing against countably many separated solenoidal fields shows that at almost every time the strong form ∂ₜu - Δu + (u·∇)u of the equation is orthogonal to every solenoidal test field, hence to J (lem:lps-H1-estimate).

theorem ESS.lps_strong_form_orthogonal_test_ae {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU : IsLpsStrongSolution t₀ t₁ u Du p) (hD : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu) (hMu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMD2 : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ψ ∈ LpsSolenoidalTest) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ t₁), ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (Dtu (x, t) i - ∑ j : Fin 3, D2u (x, t) i j j + ∑ j : Fin 3, u (x, t) j * Du (x, t) i j) * ψ x i = 0

At almost every time, the strong form of the equation is orthogonal to a fixed smooth compactly supported solenoidal field (lem:lps-H1-estimate).

theorem ESS.lps_abs_pairing_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), ∑ i : Fin 3, F x i * g x i| ≤ 3 * (MeasureTheory.eLpNorm F 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

The L² pairing of two vector fields is bounded by the product of their L² norms.

theorem ESS.lps_strong_form_orthogonal_J_ae {t₀ t₁ : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU : IsLpsStrongSolution t₀ t₁ u Du p) (hD : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ t₁) u Du D2u Dtu) (hMu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMDu : MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMD2 : MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) (hMDt : MeasureTheory.MemLp Dtu 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo t₀ t₁)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ t₁), ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), CKN.IsInJ w → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, (Dtu (x, t) i - ∑ j : Fin 3, D2u (x, t) i j j + ∑ j : Fin 3, u (x, t) j * Du (x, t) i j) * w x i = 0

At almost every time, the strong form ∂ₜu - Δu + (u·∇)u of the equation is orthogonal to every element of J (lem:lps-H1-estimate).