Campanato Holder Corollaries

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

theorem CKN.Foundation.Parabolic.campanato_holder_local {f : ParabolicPoint → ℝ} {z₀ : ParabolicPoint} {R α K p : ℝ} (hα : 0 < α) : α < 1 → ∀ (hR : 0 < R) (hp : 1 ≤ p) (hK : 0 ≤ K) (hf : MeasureTheory.LocallyIntegrable f MeasureTheory.volume) (hdata : ParabolicBallLpDataOn f (Metric.ball z₀ R) (8 * R) p) (hcamp : ParabolicBallCampanatoBoundOn f (Metric.ball z₀ R) (8 * R) α K p), ∃ (g : ParabolicPoint → ℝ), g =ᵐ[MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2))] f ∧ ParabolicHolderSeminormLE (Metric.ball z₀ (R / 2)) g α (parabolicCampanatoHolderConstant α p * K)