Vanishing initial-time mass on a bounded ball #
The zero trace and the weak time derivative bound imply that the normalized quadratic mass vanishes in shrinking initial-time strips.
theorem
ESS.buGaussian_initial_trace_strip_tendsto_zero
{B : Set CKN.Foundation.Parabolic.Vec3}
{τ : ℝ}
(hBopen : IsOpen B)
(hBfinite : MeasureTheory.volume B < ⊤)
(hτ : 0 < τ)
{v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hcont : ContinuousOn v (CKN.spaceTimeSet B (Set.Ico 0 τ)))
(hzero :
∀ x ∈ B,
v
(have this := (x, 0);
this) = 0)
(hweak : CKN.HasSpaceTimeWeakDerivs B (Set.Ioo 0 τ) v Dv D2v Dtv)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet B (Set.Ioo 0 τ), ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
:
Filter.Tendsto
(fun (ε : ℝ) =>
(∫ (q : CKN.Foundation.Parabolic.Vec3 × ℝ) in B ×ˢ Set.Ioc ε (2 * ε), CKN.Foundation.Parabolic.vec3EuclideanNorm (v (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) ^ 2) / ε ^ 2)
(nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
The normalized quadratic mass of a zero-trace field vanishes on shrinking
initial-time strips (lem:ftc-small-time).