High-strip integrability from Gaussian averages

A Gaussian velocity average on every high-strip dyadic cell implies integrability of each fixed weighted quadratic density on the entire short-time high strip.

theorem ESS.bu_short_high_strip_integrable_of_average (scale c b β G Cw Cg : ℝ) (hscale : 0 < scale) (hscale1 : scale ≤ 1) (hc : 0 ≤ c) (hβ : 0 < β) (hGtan : G ≤ 1 / 16) (hGnorm : G ≤ β / 48) (hbβ : b ≤ β / 48) (hCw : 0 ≤ Cw) (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)))) (W : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hWcont : ContinuousOn W {z : CKN.Foundation.Parabolic.ParabolicPoint | 0 < z.1 2 ∧ 0 < z.2}) (hW : ∀ (k : ℤ), 1 ≤ k → ∀ (m : Fin 3 → ℤ) (ell : Fin 2048), ∀ z ∈ buShortShiftedDyadicCell k m ell ∩ buShortHighStrip scale, 0 ≤ W z ∧ W z ≤ Cw * Real.exp (-((CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 0 ^ 2 + (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 1 ^ 2) / 8) * Real.exp (b * (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1 2 ^ 2)) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => W z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z)) (buShortHighStrip scale) MeasureTheory.volume

Gaussian velocity averages give global integrability of any fixed nonnegative short-time weight with the cell-center Gaussian bound (lem:bu-small-time).