The strong form of the equation against separated test fields

Testing the pressure-free weak equation of a strong solution against the separated solenoidal field χ(t) ψ(x), and using the weak time and spatial derivatives, gives the integrated strong form ∫ χ(t) ⟨∂ₜu - Δu + (u·∇)u, ψ⟩ dt = 0 (lem:lps-H1-estimate).

theorem ESS.lps_integral_neg_sub_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g h : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hh : MeasureTheory.Integrable h μ) : ∫ (q : α), -f q - g q + h q ∂μ = -∫ (q : α), f q ∂μ - ∫ (q : α), g q ∂μ + ∫ (q : α), h q ∂μ

Integral of -f - g + h.

theorem ESS.lps_integral_sub_add {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g h : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hh : MeasureTheory.Integrable h μ) : ∫ (q : α), f q - g q + h q ∂μ = ∫ (q : α), f q ∂μ - ∫ (q : α), g q ∂μ + ∫ (q : α), h q ∂μ

Integral of f - g + h.

theorem ESS.lps_integral_sub_sub {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g h : α → ℝ} (hf : MeasureTheory.Integrable f μ) (hg : MeasureTheory.Integrable g μ) (hh : MeasureTheory.Integrable h μ) : ∫ (q : α), f q - g q - h q ∂μ = ∫ (q : α), f q ∂μ - ∫ (q : α), g q ∂μ - ∫ (q : α), h q ∂μ

Integral of f - g - h.

theorem ESS.lps_strong_separated_identity {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χ : ContDiff ℝ (↑⊤) χ) (hχc : HasCompactSupport χ) (hχs : tsupport χ ⊆ Set.Ioo t₀ t₁) (hψ : ∀ (i : Fin 3), ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => ψ x i) (hψc : HasCompactSupport ψ) (hdiv : ∀ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) i x = 0) : ∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, Dtu (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) i * (χ q.2 * ψ q.1 i) - ∑ i : Fin 3, ∑ j : Fin 3, u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) i * u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) j * (χ q.2 * CKN.spatialDeriv (fun (y : CKN.Foundation.Parabolic.Vec3) => ψ y i) j q.1) - ∑ i : Fin 3, (∑ j : Fin 3, D2u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q) i j j) * (χ q.2 * ψ q.1 i) ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo t₀ t₁)) = 0

Testing the strong equation with a separated solenoidal field: the weak time and spatial derivatives convert the weak form into the integrated strong form, up to the transported product u ⊗ u (lem:lps-H1-estimate).