Small Time Trace #
Trace estimates at small positive times in the backward uniqueness argument.
theorem
ESS.ftc_small_time
{B : Set CKN.Foundation.Parabolic.Vec3}
{τ : ℝ}
(hB : IsOpen B)
(hτ : 0 < τ)
{w Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hwcont : ContinuousOn w (CKN.spaceTimeSet B (Set.Ico 0 τ)))
(hwzero :
∀ x ∈ B,
w
(have this := (x, 0);
this) = 0)
(hDtwL2 :
MeasureTheory.MemLp Dtw 2 ((MeasureTheory.volume.restrict B).prod (MeasureTheory.volume.restrict (Set.Ioo 0 τ))))
(Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hderiv : CKN.HasSpaceTimeWeakDerivs B (Set.Ioo 0 τ) w Dw D2w Dtw)
(t : ℝ)
:
0 < t →
t < τ →
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ENNReal.ofReal
(CKN.Foundation.Parabolic.vec3EuclideanNorm
(w
(have this := (x, t);
this)) ^ 2) ≤ ENNReal.ofReal t * ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in B, ∫⁻ (s : ℝ) in Set.Ioc 0 t, ENNReal.ofReal
(CKN.Foundation.Parabolic.vec3EuclideanNorm
(Dtw
(have this := (x, s);
this)) ^ 2)
The small-time trace estimate from manuscript label lem:ftc-small-time.
The space-time time derivative identity gives the a.e. sectionwise weak
derivative through hasSectionwiseTimeWeakDeriv_of_hasSpaceTimeWeakDerivs.
The spacetime L² hypothesis uses the product volume. The nested right-hand
lintegral places space outside time; Tonelli's theorem identifies it with the
manuscript's time-outside-space order.