Physical Gaussian average

The rescaled integral and the radial Gaussian decay give the physical space-time average in lem:bu-gaussian.

theorem ESS.buGaussian_metric_average_integrable_at_small_time (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) (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 < ⊤) (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) (htsmall : t ≤ 1 / 24) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball x √(3 * t)) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume

The physical averaging box is integrable at the chosen short time.

theorem ESS.buGaussian_shifted_scaled_eq_average (x : CKN.Foundation.Parabolic.Vec3) (scale σ : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) : buGaussianShiftedField σ (ucScaledField x scale w) = buGaussianAverageScaledField x scale σ w

Translation of a scaled field agrees with the field in Gaussian averaging coordinates.

theorem ESS.buGaussian_metric_average_normalized (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) (ht : 0 < t) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball x √(3 * t)) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume) : 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 = Real.rpow 3 (5 / 2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball 0 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) (ucScaledField x (√(3 * t)) w) z) ^ 2

The metric-ball change of variables with the source averaging normalization.

theorem ESS.buGaussian_physical_average_of_core (β H c P Ctail Ccore k₀ k₁ Cacc : ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t ρ a barA I : ℝ) (w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hβ : 0 < β) (hH : 0 < H) (ht : 0 < t) (hx : 2 < x 2) (hρlarge : 4 < ρ) (hρ : ρ = (x 2 - 1) / √(3 * t)) (ha : a = β * ρ ^ 2 / H) (hCtail : Ctail = 64 * (1 + β / (2 * H)) / (β / 2) ^ 2 / √β) (hCcore : Ccore = 2 * Real.exp (3 / 2) * c * P * Ctail) (hc : 0 ≤ c) (hPform : P = 192 * (k₀ ^ 2 + k₁ ^ 2 * Cacc) + 49153) (hCacc : 0 ≤ Cacc) (hInt : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2) (CKN.spaceTimeSet (Metric.ball x √(3 * t)) (Set.Ioo t (5 * t / 2))) MeasureTheory.volume) (hMass : Real.exp (-(3 / 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (Metric.ball 0 1) (Set.Ioo (1 / 2) 1), CKN.Foundation.Parabolic.vec3EuclideanNorm (buGaussianShiftedField (1 / 6) (ucScaledField x (√(3 * t)) w) z) ^ 2 ≤ I) (hI : I ≤ 2 * c * P * ((1 + a) * (1 + ρ) ^ 3 * (Real.exp (8 * barA * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (-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 ≤ Real.rpow 3 (5 / 2) * Ccore * Real.exp (8 * barA * CKN.Foundation.Parabolic.vec3EuclideanNorm x ^ 2) * Real.exp (-(β * x 2 ^ 2) / (12 * t))

The Carleman-box estimate gives the physical Gaussian average decay.