Assembly of mixed-norm cross-testing limits #
The regularized weak identity passes to the limit once both oriented cross-density limits are available. The finite mixed-norm and endpoint providers supply these limits separately.
theorem
ESS.lps_cross_identity_from_density_limits
{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)
(hDensityVU :
∀ t ∈ Set.Ioo 0 T,
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity v Dv pv u Du n (serrinCutoff n))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity v Dv pv u Du n (serrinCutoff n) q)
Filter.atTop
(nhds
((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, u q k * ∑ j : Fin 3, v q j * Dv q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Dv q k j)))
(hDensityUV :
∀ t ∈ Set.Ioo 0 T,
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity u Du pu v Dv n (serrinCutoff n))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto
(fun (n : ℕ) =>
∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity u Du pu v Dv n (serrinCutoff n) q)
Filter.atTop
(nhds
((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, v q k * ∑ j : Fin 3, u q j * Du q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Du q k j)))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, b x k * a x k = ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, u q k * ∑ j : Fin 3, v q j * Dv q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Dv q k j) + ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, v q k * ∑ j : Fin 3, u q j * Du q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Du q k j)
Cross-testing identity from the two oriented mixed-norm density limits.