Campanato Holder Final #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Foundation.Parabolic.campanato_holder
{f : ParabolicPoint → ℝ}
{α K p : ℝ}
(hα : 0 < α)
:
α < 1 →
∀ (hp : 1 ≤ p) (hK : 0 ≤ K) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume)
(hdata : GlobalParabolicBallLpData f p) (hcamp : GlobalParabolicBallCampanatoBound f α K p),
∃ (g : ParabolicPoint → ℝ),
g =ᵐ[MeasureTheory.volume] f ∧ ParabolicHolderSeminormLE Set.univ g α (parabolicCampanatoHolderConstant α p * K)