Unique continuation at a translated top time #
The unique continuation theorem thm:uc is stated at the spatial origin and
initial time zero of a forward cylinder. Reversing time about a top time
t₀ and translating the spatial center to x₀ transports it to past
cylinders B_R(x₀) × (t₀ - T, t₀]. Vanishing on a small past cylinder at the
top point gives the infinite-order hypothesis by lem:flat-from-vanishing.
theorem
ESS.essLocal_uniqueContinuation_past
(R T C M r₀ : ℝ)
(hR : 0 < R)
(hT : 0 < T)
(hC : 0 ≤ C)
(hM : 0 ≤ M)
(hr₀ : 0 < r₀)
(hr₀R : r₀ ≤ R)
(hr₀T : r₀ ^ 2 ≤ T)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ : ℝ)
(ω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2ω : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(Dtω : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hcont : ContinuousOn ω (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioc (t₀ - T) t₀)))
(hderiv : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo (t₀ - T) t₀) ω Dω D2ω Dtω)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo (t₀ - T) t₀), ‖ω z‖ₑ ^ 2 + ‖Dω z‖ₑ ^ 2 + ‖D2ω z‖ₑ ^ 2 + ‖Dtω z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo (t₀ - T) t₀)), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtω z i - ∑ j : Fin 3, D2ω z i j j) ≤ C * (CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) + √(CKN.spatialGradientSq ω Dω z)))
(hbound :
∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioc (t₀ - T) t₀),
CKN.Foundation.Parabolic.vec3EuclideanNorm (ω z) ≤ M)
(hzero :
∀ (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ),
x ∈ CKN.Foundation.Parabolic.vec3Ball x₀ r₀ → s ∈ Set.Ioo (t₀ - r₀ ^ 2) t₀ → ω (x, s) = 0)
(x : CKN.Foundation.Parabolic.Vec3)
:
Unique continuation for the backward heat inequality on a past cylinder:
a bounded continuous field of class W^{2,1}_2 satisfying
|∂ₜω - Δω| ≤ C (|ω| + |∇ω|) which vanishes on a small past cylinder at the top
point (x₀, t₀) vanishes on the whole top ball (thm:uc,
lem:flat-from-vanishing).