Indicator #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Foundation.Parabolic.Morrey.cylinderPowerIntegral_indicator
{p : ℝ}
(hp : 0 < p)
{S : Set ParabolicPoint}
(hS : MeasurableSet S)
(g : ParabolicPoint → ℝ)
(z : ParabolicPoint)
(r : ℝ)
:
cylinderPowerIntegral p (S.indicator g) z r = ∫⁻ (w : ParabolicPoint) in parabolicCylinder z.1 z.2 r ∩ S, ENNReal.ofReal |g w| ^ p
The Morrey cylinder integral of a set indicator equals the integral restricted to the intersection of the cylinder with the set.