Space-time integration by parts

The compactly supported spatial Laplacian pairing identity used in prop:carleman-gauss of the Escauriaza–Seregin–Šverák manuscript and lem:caccioppoli.

theorem CKN.instIsAddHaarMeasureProdVec3RealVolume : MeasureTheory.volume.IsAddHaarMeasure

@[instance_reducible]

def CKN.instTopologicalSpaceParabolicPoint : TopologicalSpace Foundation.Parabolic.ParabolicPoint

The product topology on spatial points and time used for space-time calculus.

Equations

• CKN.instTopologicalSpaceParabolicPoint = instTopologicalSpaceProd

theorem CKN.integral_spatial_laplacian_pairing {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑2) f) (hg : ContDiff ℝ (↑2) g) (hfc : HasCompactSupport f) (hgc : HasCompactSupport g) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), (∑ i : Fin 3, spatialSecondPartial (have this := f; this) i i z) * g z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, spatialPartial (have this := f; this) i z * spatialPartial (have this := g; this) i z ∧ -∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, spatialPartial (have this := f; this) i z * spatialPartial (have this := g; this) i z = ∫ (z : Foundation.Parabolic.Vec3 × ℝ), f z * ∑ i : Fin 3, spatialSecondPartial (have this := g; this) i i z