One Gaussian estimate on a short-time cell #
The physical Gaussian average at a high-strip cell center yields the normalized dyadic bound used in the cell summation.
theorem
ESS.bu_short_gaussian_cell_average_bound
(M scale γ C β : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hscaleγ : scale ^ 2 ≤ γ)
(hγ : γ < 1 / 12)
(hC : 0 ≤ C)
(hβ : 0 < β)
(hMbar : 1 / 10 ^ 12 / 2 ≤ M)
(k : ℤ)
(hk : 1 ≤ k)
(m : Fin 3 → ℤ)
(ell : Fin 2048)
(z₀ : CKN.Foundation.Parabolic.ParabolicPoint)
(hz₀ : z₀ ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale)
(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)
(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 < ⊤)
(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))
(hGaussian :
have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1;
have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2;
have X := scale • Y;
have t := scale ^ 2 * δ / 2;
t.rpow (-(5 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball X √(3 * t)) (Set.Ioo t (5 * t / 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2 ≤ C * Real.exp (8 * max M (1 / 10 ^ 12 / 2) * CKN.Foundation.Parabolic.vec3EuclideanNorm X ^ 2) * Real.exp (-(β * X 2 ^ 2 / (12 * t))))
:
have d := CKN.Foundation.buSmallTimeDyadicScale k;
have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1;
have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2;
have v := buAffineField (-scale ^ 2 / 2) scale w;
have Avg :=
CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2)) (Set.Ioo (1 / 2 + δ / 2) (1 / 2 + 5 * δ / 4));
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in Avg, CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 ≤ C * d ^ 2 * Real.exp (8 * M * scale ^ 2 * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d)))
The physical Gaussian estimate transfers to a normalized average
at every high-strip cell center (lem:bu-small-time).