The mollified cross identity #
For two Leray–Hopf solutions with pressures, the cutoff-weighted pairing of
their mollifications changes in time by the integrated tested fluxes. This is
the regularized cross-testing identity of lem:pv-serrin-uniqueness; the
mollification and cutoff are removed afterwards.
theorem
ESS.serrinMol_cross_identity
{T : ℝ}
{a b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du pu)
(hV : IsSerrinWeakSolution T b v Dv pv)
{ρ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hρ : ContDiff ℝ (↑⊤) ρ)
(hρc : HasCompactSupport ρ)
{η : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hη : Continuous η)
(hηc : HasCompactSupport η)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
:
∫ (y : CKN.Foundation.Parabolic.Vec3), η y * (∑ k : Fin 3, serrinMol v ρ k y t * serrinMol u ρ k y t - ∑ k : Fin 3, serrinMol v ρ k y 0 * serrinMol u ρ k y 0) = ∫ (τ : ℝ) in 0..t, ∫ (y : CKN.Foundation.Parabolic.Vec3), η y * ∑ k : Fin 3,
(serrinMolFlux v Dv pv ρ k y τ * serrinMol u ρ k y τ + serrinMol v ρ k y τ * serrinMolFlux u Du pu ρ k y τ)
The cutoff-weighted pairing of two mollified solutions changes in time by the integrated tested fluxes.