The mollified strong equation #
Testing the strong equation of a strong solution against a translated kernel
times a function of time gives, at every point of space and for almost every
time, an identity between kernel convolutions of the specified fields
(prop:lps-local-strong).
theorem
ESS.LPS.lps_slab_integral_sep_L1
{a τ : ℝ}
{g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hg : MeasureTheory.Integrable g (MeasureTheory.volume.restrict (CKN.vlSlab a τ)))
{k : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hk : CKN.IsVlKernel k)
(x : CKN.Foundation.Parabolic.Vec3)
{η : ℝ → ℝ}
(hη : Continuous η)
(hηb : ∃ (C : ℝ), ∀ (s : ℝ), |η s| ≤ C)
:
MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g p * (k (x - p.1) * η p.2))
(MeasureTheory.volume.restrict (CKN.vlSlab a τ)) ∧ ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a τ, g p * (k (x - p.1) * η p.2) = ∫ (s : ℝ) in Set.Ioo a τ, η s * CKN.vlConvT k g x s
Fubini for an integrable slab field against a separated bounded weight.
theorem
ESS.LPS.lps_convT_integrableOn_L1
{a τ : ℝ}
{g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hg : MeasureTheory.Integrable g (MeasureTheory.volume.restrict (CKN.vlSlab a τ)))
{k : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hk : CKN.IsVlKernel k)
(x : CKN.Foundation.Parabolic.Vec3)
:
MeasureTheory.IntegrableOn (fun (s : ℝ) => CKN.vlConvT k g x s) (Set.Ioo a τ) MeasureTheory.volume
theorem
ESS.LPS.lps_strong_mollified_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)
{κ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : CKN.IsVlKernel κ)
(x : CKN.Foundation.Parabolic.Vec3)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), CKN.vlConvT κ (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => Dtu z i) x t + ∑ j : Fin 3,
CKN.vlConvT (CKN.vlDeriv κ j) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z i * u z j) x t - ∑ j : Fin 3, CKN.vlConvT κ (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => D2u z i j j) x t + CKN.vlConvT (CKN.vlDeriv κ i) p x t = 0
The mollified strong equation: at every point of space, for almost every
time, the convolutions of the specified fields satisfy the momentum equation
in the i-th component (prop:lps-local-strong).