The strong form of the equation against a scalar test

A strong solution satisfies its equation, with the specified weak time derivative and Laplacian, against every scalar space-time test field placed in one velocity component (prop:lps-local-strong).

def ESS.LPS.lpsSingleTest (i : Fin 3) (s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3

The scalar test placed in the i-th velocity component.

Equations

• ESS.LPS.lpsSingleTest i s z = Pi.single i (s z)

theorem ESS.LPS.lpsSingleTest_mem {a b : ℝ} (i : Fin 3) {s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hs : s ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)) : lpsSingleTest i s ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)

theorem ESS.LPS.lpsSingleTest_spatialPartial (i k j : Fin 3) (s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => lpsSingleTest i s y k) j z = if k = i then CKN.spatialPartial s j z else 0

theorem ESS.LPS.lpsSingleTest_timePartial (i k : Fin 3) (s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => lpsSingleTest i s y k) z = if k = i then CKN.timePartial s z else 0

theorem ESS.LPS.lps_test_memLp_slab {a b : ℝ} {s : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hs : s ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)) (j : Fin 3) : MeasureTheory.MemLp s 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial s j z) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.timePartial s z) 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))

A space-time test field and its first derivatives are square integrable on the slab.

theorem ESS.LPS.lps_strong_scalar_equation {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 → ℝ} (hU : IsLpsStrongSolution t₀ T u Du p) {D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtu : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hDerivs : CKN.HasSpaceTimeWeakDerivs Set.univ (Set.Ioo t₀ T) u Du D2u Dtu) (hu : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i) 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T))) (hDu : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Du z i j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T))) (hD2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => D2u z i j j) 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T))) (hDt : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtu z i) 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T))) (hp : MeasureTheory.MemLp p 2 (MeasureTheory.volume.restrict (CKN.vlSlab t₀ T))) (i : Fin 3) {s : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hs : s ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo t₀ T)) : ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab t₀ T, Dtu z i * s z - ∑ j : Fin 3, u z i * u z j * CKN.spatialPartial s j z - (∑ j : Fin 3, D2u z i j j) * s z - p z * CKN.spatialPartial s i z = 0

A strong solution satisfies its equation, in the strong form with its specified time derivative and Laplacian, against every scalar test placed in one velocity component (prop:lps-local-strong).