Translated data for spatial unique continuation #
An affine time change followed by spatial translation places a ball inside the positive half-space at initial time zero.
theorem
ESS.bu_short_uc_translated_data
(M τ δ c₁ R : ℝ)
(c : CKN.Foundation.Parabolic.Vec3)
(hτ : 0 < τ)
(hδ : 0 < δ)
(hδ1 : δ ≤ 1)
(hend : τ + δ ^ 2 * 2 < 1)
(hc₁ : 0 < c₁)
(hR : 0 < R)
(hball : CKN.Foundation.Parabolic.vec3Ball c R ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2})
(w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(hcont : ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1))
(hweak : CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w Dtw)
(hL2 :
∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z)))
(hgrowth :
∀ z ∈ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1),
CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (M * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2))
:
have W := ucScaledField c 1 (buAffineField τ δ w);
have G := ucScaledDw c 1 (buAffineDw τ δ Dw);
have H := ucScaledD2w c 1 (buAffineD2w τ δ D2w);
have T := ucScaledDtw c 1 (buAffineDtw τ δ Dtw);
ContinuousOn W (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ico 0 2) ∧ CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 2) W G H T ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 2), ‖W z‖ₑ ^ 2 + ‖G z‖ₑ ^ 2 + ‖H z‖ₑ ^ 2 + ‖T z‖ₑ ^ 2 < ⊤ ∧ ∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 R) (Set.Ioo 0 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector H T z) ≤ c₁ * δ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) + √(CKN.spatialGradientSq W G z))
The field translated from an interior half-space ball has the
continuity, weak derivatives, quadratic energy, and differential
inequality required by unique continuation (thm:uc).