Local quadratic data for Gaussian averages

The pointwise growth assumption supplies the missing local square integrability of the field in lem:bu-gaussian.

@[reducible, inline]

abbrev ESS.buHalfSpace : Set CKN.Foundation.Parabolic.Vec3

The spatial domain in lem:bu-gaussian.

Equations

• ESS.buHalfSpace = {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}

@[reducible, inline]

abbrev ESS.buHalfCylinder : Set CKN.Foundation.Parabolic.ParabolicPoint

The open space-time domain in lem:bu-gaussian.

Equations

• ESS.buHalfCylinder = CKN.spaceTimeSet ESS.buHalfSpace (Set.Ioo 0 1)

theorem ESS.buGaussian_local_quadratic_l2 (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)) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) : S ⊆ buHalfCylinder → Bornology.IsBounded S → ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤

The solution and its weak derivatives have finite local quadratic data under the source hypotheses of lem:bu-gaussian.