The three short-time densities from one Gaussian average #
The common cell-center Gaussian bound applies to the tangential factor and both fixed Carleman factors.
theorem
ESS.bu_short_three_densities_integrable_of_average
(scale c a β G Cg : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hc : 0 ≤ c)
(ha : 0 ≤ a)
(hβ : 0 < β)
(hGtan : G ≤ 1 / 16)
(hGnorm : G ≤ β / 48)
(hCg : 0 ≤ Cg)
{v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hcont : ContinuousOn v ({x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ×ˢ Set.Ico (1 / 2) (3 / 2)))
(hweak :
CKN.HasSpaceTimeWeakDerivs {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)) v Dv D2v Dtv)
(hlocal :
∀ S ⊆ CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2)),
Bornology.IsBounded S →
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤)
(hineq :
∀ᵐ (z :
CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict
(CKN.spaceTimeSet {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} (Set.Ioo (1 / 2) (3 / 2))), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (√(CKN.spatialGradientSq v Dv z) + CKN.Foundation.Parabolic.vec3EuclideanNorm (v z)))
(hAvg :
∀ (k : ℤ),
1 ≤ k →
∀ (m : Fin 3 → ℤ) (ell : Fin 2048),
(buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale).Nonempty →
have d := CKN.Foundation.buSmallTimeDyadicScale k;
have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1;
have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2;
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 ≤ Cg * d ^ 2 * Real.exp (G * (Y 0 ^ 2 + Y 1 ^ 2 + Y 2 ^ 2)) * Real.exp (-(β * Y 2 ^ 2 / (12 * d))))
:
have E := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z;
have W₀ := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
Real.exp (-(z.1 0 ^ 2 + z.1 1 ^ 2) / (4 * z.2)) * (1 + z.1 2) ^ 4;
have W₁ := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => buShortShiftedWeight scale a z * (1 + z.1 2) ^ 4;
have W₂ := buShortShiftedWeight scale a;
MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W₀ z * E z) (buShortHighStrip scale)
MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W₁ z * E z) (buShortHighStrip scale)
MeasureTheory.volume ∧ MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W₂ z * E z)
(buShortHighStrip scale) MeasureTheory.volume
Gaussian velocity averages imply integrability of all three
weighted quadratic densities on the high normal strip
(lem:bu-small-time).