The limit of the cross densities #
As the mollification radius tends to zero and the cutoff radius to infinity,
the space-time integral of a cross density converges to minus the convection
pairing and the gradient pairing. This is the limit passage on the right side
of the cross-testing identity in lem:pv-serrin-uniqueness.
theorem
ESS.serrinCrossDensity_limit
{t T : ℝ}
(ht : t ≤ T)
{w z : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dw Dz : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{pw : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{p1 q1 p4 q4 : ENNReal}
[p1.HolderTriple q1 1]
[p4.HolderTriple q4 1]
(hp1 : 1 ≤ p1)
(hp1t : p1 ≠ ⊤)
(hq1 : 1 ≤ q1)
(hq1t : q1 ≠ ⊤)
(hp4 : 1 ≤ p4)
(hp4t : p4 ≠ ⊤)
(hq4 : 1 ≤ q4)
(hq4t : q4 ≠ ⊤)
(hz1 :
∀ (k : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) p1
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hN :
∀ (k : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w r j * Dw r k j) q1
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hDz :
∀ (k j : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dz r k j) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hDw :
∀ (k j : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dw r k j) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hz2 :
∀ (k : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) 2
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hz4 :
∀ (k : Fin 3),
MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) p4
(MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hpw : MeasureTheory.MemLp pw q4 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
(∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity w Dw pw z Dz 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 w Dw pw z Dz n (serrinCutoff n) q)
Filter.atTop
(nhds
((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, z q k * ∑ j : Fin 3, w q j * Dw q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dz q k j * Dw q k j))
Integrability and the limit of the space-time integral of a cross density.