Data on the shifted Gaussian cylinder #
The time shift in lem:bu-gaussian moves the rescaled solution away from the
singular initial face of the Gaussian Carleman weight.
noncomputable def
ESS.buGaussianShiftedField
(σ : ℝ)
(v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
The rescaled field after the positive-time translation in
lem:bu-gaussian.
Equations
- ESS.buGaussianShiftedField σ v z = v ((ESS.buGaussianTimeShiftPoint σ).symm z)
Instances For
noncomputable def
ESS.buGaussianShiftedDw
(σ : ℝ)
(Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
:
The first derivative after time translation.
Equations
- ESS.buGaussianShiftedDw σ Dv z i j = Dv ((ESS.buGaussianTimeShiftPoint σ).symm z) i j
Instances For
noncomputable def
ESS.buGaussianShiftedD2w
(σ : ℝ)
(D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3)
:
The second derivative after time translation.
Equations
- ESS.buGaussianShiftedD2w σ D2v z i j k = D2v ((ESS.buGaussianTimeShiftPoint σ).symm z) i j k
Instances For
noncomputable def
ESS.buGaussianShiftedDtw
(σ : ℝ)
(Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
:
The time derivative after time translation.
Equations
- ESS.buGaussianShiftedDtw σ Dtv z i = Dtv ((ESS.buGaussianTimeShiftPoint σ).symm z) i
Instances For
theorem
ESS.buGaussian_shifted_rescaled_data
(c₁ A : ℝ)
(hc₁ : 0 < c₁)
(hA : 0 ≤ A)
(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 (buHalfSpace ×ˢ Set.Ico 0 1))
(hzero : ∀ (x : CKN.Foundation.Parabolic.Vec3), 0 < x 2 → w (x, 0) = 0)
(hderiv : CKN.HasSpaceTimeWeakDerivs buHalfSpace (Set.Ioo 0 1) w Dw D2w Dtw)
(hL2 :
∀ S ⊆ buHalfCylinder,
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 buHalfCylinder, (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ≤ c₁ * (√(CKN.spatialGradientSq w Dw z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (w z)))
(hgrowth :
∀ z ∈ buHalfCylinder,
CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ≤ Real.exp (A * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2))
(x : CKN.Foundation.Parabolic.Vec3)
(t γ : ℝ)
(hx₃ : 2 < x 2)
(ht : 0 < t)
(hγ : γ ≤ 1 / 12)
(htγ : t < γ)
:
have scale := √(3 * t);
have ρ := (x 2 - 1) / scale;
have σ := 1 / 6;
CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2)
(buGaussianShiftedField σ (ucScaledField x scale w)) (buGaussianShiftedDw σ (ucScaledDw x scale Dw))
(buGaussianShiftedD2w σ (ucScaledD2w x scale D2w)) (buGaussianShiftedDtw σ (ucScaledDtw x scale Dtw)) ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2), ‖buGaussianShiftedField σ (ucScaledField x scale w) z‖ₑ ^ 2 + ‖buGaussianShiftedDw σ (ucScaledDw x scale Dw) z‖ₑ ^ 2 + ‖buGaussianShiftedD2w σ (ucScaledD2w x scale D2w) z‖ₑ ^ 2 + ‖buGaussianShiftedDtw σ (ucScaledDtw x scale Dtw) z‖ₑ ^ 2 < ⊤ ∧ (∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm
(ucWeakHeatVector (buGaussianShiftedD2w σ (ucScaledD2w x scale D2w))
(buGaussianShiftedDtw σ (ucScaledDtw x scale Dtw)) z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField σ (ucScaledField x scale w) z) + √(CKN.spatialGradientSq (buGaussianShiftedField σ (ucScaledField x scale w))
(buGaussianShiftedDw σ (ucScaledDw x scale Dw)) z))) ∧ ContinuousOn (buGaussianShiftedField σ (ucScaledField x scale w))
(CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ico σ 2) ∧ (∀ y ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ, buGaussianShiftedField σ (ucScaledField x scale w) (y, σ) = 0) ∧ ∀ z ∈ CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2),
CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField σ (ucScaledField x scale w) z) ≤ Real.exp
(2 * A * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2 + 2 * A * √(3 * t) ^ 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm z.1 ^ 2)
The local source hypotheses give weak derivatives, finite quadratic data, and the differential inequality on the shifted Gaussian cylinder.