The regularized cross identity in integrated-by-parts form #
Combining the mollified cross identity with the fixed-time flux computation
gives, for every mollification radius and cutoff, an identity whose right side
involves only mollified velocities, gradients, convection terms and pressures.
The mollification and the cutoff are removed afterwards in
lem:pv-serrin-uniqueness.
noncomputable def
ESS.serrinCrossDensity
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(pw : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(z : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dz : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(n : ℕ)
(η : CKN.Foundation.Parabolic.Vec3 → ℝ)
(q : CKN.Foundation.Parabolic.ParabolicPoint)
:
The cross density: the tested flux of w against the mollified field z,
in integrated-by-parts form, at a space-time point (y, τ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ESS.serrin_cross_regularized
{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)
(n : ℕ)
{η : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hη : ContDiff ℝ (↑⊤) η)
(hηc : HasCompactSupport η)
{t : ℝ}
(ht : t ∈ Set.Icc 0 T)
:
∫ (y : CKN.Foundation.Parabolic.Vec3), η y * (∑ k : Fin 3, serrinMol v (serrinKernel n) k y t * serrinMol u (serrinKernel n) k y t - ∑ k : Fin 3, serrinMol v (serrinKernel n) k y 0 * serrinMol u (serrinKernel n) k y 0) = ∫ (τ : ℝ) in 0..t, (∫ (y : CKN.Foundation.Parabolic.Vec3), serrinCrossDensity v Dv pv u Du n η (y, τ)) + ∫ (y : CKN.Foundation.Parabolic.Vec3), serrinCrossDensity u Du pu v Dv n η (y, τ)
The regularized cross identity: for every mollification radius and cutoff, the change of the cutoff-weighted mollified pairing equals the time integral of the two cross densities.