Phase-shifted absorbed Carleman estimate #
The fixed normal phase can be removed from both sides of the absorbed half-space estimate without changing its coefficient.
theorem
ESS.bu_short_integral_shift_le
(scale a c : ℝ)
(K : Set CKN.Foundation.Parabolic.ParabolicPoint)
(F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(h :
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * F z ≤ c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortCarlemanWeight a z * G z)
:
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * F z ≤ c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * G z
Multiplying the Carleman density by a fixed positive factor preserves an integrated inequality.
theorem
ESS.bu_short_cutoff_energy_absorbed_shifted :
∃ (a₀ : ℝ) (c : ℝ),
0 < a₀ ∧ 0 < c ∧ ∀ (scale R ε c₁ : ℝ),
0 < scale →
scale ≤ 1 →
∀ (hR : 0 < R),
0 < ε →
0 ≤ c₁ →
c * 36 * (c₁ * scale) ^ 2 ≤ 1 / 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),
ContinuousOn w ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico 0 1) →
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo 0 1) w Dw D2w
Dtw →
(∀ 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 < ⊤) →
(∀ᵐ (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))) →
∀ (a : ℝ),
max a₀ 1 < a →
have κ := buShortFullCutoff scale R hR ε;
have K := buCutSupportSet κ;
have v := buAffineField (-scale ^ 2 / 2) scale w;
have Dv := buAffineDw (-scale ^ 2 / 2) scale Dw;
have W := buCutField κ v;
have DW := buCutDw κ v Dv;
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (W z) ^ 2 + CKN.spatialGradientSq W DW z) ≤ 4 * c * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in K, buShortShiftedWeight scale a z * buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ^ 2
For a sufficiently small parabolic rescaling, the shifted cutoff energy is controlled by the shifted scalar cutoff heat error.