Normalized data for the Gaussian estimate #
The output-point geometry in lem:uc-gaussian produces a normalized weak
solution on the fixed time interval (0,2).
theorem
ESS.uc_gaussian_normalize_and_scale
(R T γ c₁ : ℝ)
(hR : 0 < R)
(hT : 0 < T)
(hγ' : γ < 3 / 16)
(hTsmall : T ≤ 1)
(hc₁ : 0 < c₁)
(x₀ x : CKN.Foundation.Parabolic.Vec3)
(t : ℝ)
(ht : 0 < t)
(ht' : t ≤ γ * T)
(hx : CKN.Foundation.Parabolic.vec3EuclideanNorm (x - x₀) ≤ 3 / 8 * √(2 / 100) * R)
(hd : 16 / 100 * t ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm (x - 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 (CKN.Foundation.Parabolic.vec3Ball x₀ R ×ˢ Set.Ico 0 T))
(hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T) w Dw D2w Dtw)
(hL2 :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x₀ R) (Set.Ioo 0 T)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2w Dtw z) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z)))
(hflat : UCIntegralFlatness x₀ R T w)
:
have scale := √(2 * t);
have X := (√(2 / 100))⁻¹ • (x - x₀);
have ρ := 2 * CKN.Foundation.Parabolic.vec3EuclideanNorm X / scale;
have v := ucScaledField x₀ scale w;
have Dv := ucScaledDw x₀ scale Dw;
have D2v := ucScaledD2w x₀ scale D2w;
have Dtv := ucScaledDtw x₀ scale Dtw;
4 ≤ ρ ∧ scale * ρ ≤ 3 * R / 4 ∧ 2 * scale ^ 2 ≤ 3 * T / 4 ∧ CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dv D2v Dtv ∧ ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤ ∧ UCIntegralFlatness 0 ρ 2 v ∧ ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (ucCylinder ρ), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c₁ * scale * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))
Translation and parabolic dilation provide all normalized hypotheses
used in the Gaussian estimate (lem:uc-gaussian).