The mollified energy identity on one time slice #
On a time slice where the gradient, the force and the force pressure have
their slice properties, the source of the mollified forced regularized
velocity is a sum of convolutions, and the spatial pairing ∑ₖ ∫ wₖ Sₖ ψ
equals, after integration by parts, the mollified transport-minus-viscous,
pressure and force pairings of eq:reg-local-energy-forced.
theorem
CKN.Leray.integrable_mul_of_hasCompactSupport_right
{g h : Foundation.Parabolic.Vec3 → ℝ}
(hg : Continuous g)
(hh : Continuous h)
(hhc : HasCompactSupport h)
:
MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => g x * h x) MeasureTheory.volume
theorem
CKN.Leray.leSF_eq_conv
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
{t : ℝ}
(k : Fin 3)
(hA :
∀ (j : Fin 3),
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) 2
MeasureTheory.volume)
(hF2 : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t)) 2 MeasureTheory.volume)
(hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume)
(hpf :
HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t))
(forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft))
(hpfl :
MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t))
MeasureTheory.volume)
(x : Foundation.Parabolic.Vec3)
:
leSF ρ ε hε ha hf η x t k = ∑ j : Fin 3, leConv (spatialDeriv η j) (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) x + leConv (spatialDeriv η k)
(fun (y : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (y, t)) x + leConv η
(fun (y : Foundation.Parabolic.Vec3) =>
forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft y k)
x - leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t) k) x
The source as a sum of convolutions on a good time slice.
theorem
CKN.Leray.leW_eq_leConv
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
(η : Foundation.Parabolic.Vec3 → ℝ)
(x : Foundation.Parabolic.Vec3)
(t : ℝ)
(k : Fin 3)
:
leW ρ ε hε ha hf η x t k = leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x
theorem
CKN.Leray.fderiv_leConv_mul
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
{g : Foundation.Parabolic.Vec3 → ℝ}
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(x : Foundation.Parabolic.Vec3)
(j : Fin 3)
:
theorem
CKN.Leray.integral_leW_mul_leSF
(ρ : RegMollifierProfile)
(ε : ℝ)
(hε : 0 < ε)
{a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
(ha : IsInJ a)
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hf : IsLocallySquareIntegrableForce f)
{η : Foundation.Parabolic.Vec3 → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
{t : ℝ}
(k : Fin 3)
(hA :
∀ (j : Fin 3),
MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) 2
MeasureTheory.volume)
(hF2 : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t)) 2 MeasureTheory.volume)
(hft : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) 2 MeasureTheory.volume)
(hpf :
HasWeakGradientOn Set.univ (fun (x : Vec 3) => forcePressure f hf (x, t))
(forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft))
(hpfl :
MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => forcePressure f hf (x, t))
MeasureTheory.volume)
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
:
∫ (x : Foundation.Parabolic.Vec3), leW ρ ε hε ha hf η x t k * leSF ρ ε hε ha hf η x t k * ψ x = (((-∑ j : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), leConv η (fun (y : Foundation.Parabolic.Vec3) => leTensor ρ ε hε ha hf j k (y, t)) x * (leConv (spatialDeriv η j) (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k)
x * ψ x + leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x * (fderiv ℝ ψ x) (basisVec j))) - ∫ (x : Foundation.Parabolic.Vec3), leConv η
(fun (y : Foundation.Parabolic.Vec3) => forcedQuadPressure ρ ε hε (forcedRegCurve ρ ε hε ha hf) (y, t))
x * (leConv (spatialDeriv η k) (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x * ψ x + leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x * (fderiv ℝ ψ x) (basisVec k))) + ∫ (x : Foundation.Parabolic.Vec3), leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x * ψ x * leConv η
(fun (y : Foundation.Parabolic.Vec3) =>
forcePressureGradientFunction (fun (x : Foundation.Parabolic.Vec3) => f (x, t)) hft y k)
x) - ∫ (x : Foundation.Parabolic.Vec3), leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedForceMod f hf (y, t) k) x * (leConv η (fun (y : Foundation.Parabolic.Vec3) => forcedRegRep ρ ε hε ha hf (y, t) k) x * ψ x)
The mollified energy pairing in one direction on a good time slice.