Interior Weak

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Distributional harmonicity and the mollifier identities used below.

def CKN.Foundation.Heat.WeaklyHarmonicOn (U : Set Parabolic.Vec3) (h : Parabolic.Vec3 → ℝ) : Prop

A locally integrable function is weakly harmonic when its Laplacian pairing with every compactly supported smooth test function vanishes.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Foundation.Heat.weaklyHarmonicOn_mollify_spatialLaplacian_eq_zero {U : Set Parabolic.Vec3} (hU : MeasurableSet U) {h : Parabolic.Vec3 → ℝ} (hmem : MeasureTheory.MemLp h (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict U)) (hweak : WeaklyHarmonicOn U h) {ε : ℝ} (hε : 0 < ε) {x : Parabolic.Vec3} (hx : Metric.closedBall x ε ⊆ U) : spatialLaplacian (mollify (U.indicator h) ε hε) x = 0