Convolution identities on almost every slice #
Kernel-convolution identities that hold at every point of space for almost
every time also hold for almost every time at almost every point of space,
for fields that are only almost everywhere strongly measurable
(prop:lps-local-strong).
theorem
ESS.LPS.lps_vlConvT_congr_ae_time
{a b : ℝ}
{f f' : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(h : f =ᵐ[MeasureTheory.volume.restrict (CKN.vlSlab a b)] f')
(k : CKN.Foundation.Parabolic.Vec3 → ℝ)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT k f x t = CKN.vlConvT k f' x t
Convolutions of almost everywhere equal slab fields agree at every point for almost every time.
theorem
ESS.LPS.lps_conv_first_deriv_ae_aem
{a b : ℝ}
{w g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(j : Fin 3)
(hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hgrad :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b),
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, g p * φ p)
{κ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : CKN.IsVlKernel κ)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (CKN.vlDeriv κ j) w x s = CKN.vlConvT κ g x s
The first spatial derivative of a slab field as an identity between kernel convolutions, for almost every time and almost every point, for fields that are only almost everywhere strongly measurable.
theorem
ESS.LPS.lps_strong_mollified_equation_slice
{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 κ)
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo t₀ T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), 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 holds for almost every time at almost every
point of space (prop:lps-local-strong).