Potential Measurability

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

theorem CKN.Core.Endgame.measurable_riesz_potential (β : ℝ) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : Measurable f) : Measurable (Foundation.Parabolic.Morrey.parabolicRieszPotential β f)

A measurable source has a measurable extended-real Riesz potential.

theorem CKN.Core.Endgame.measurable_riesz_potential_of_aemeasurable (β : ℝ) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) : Measurable (Foundation.Parabolic.Morrey.parabolicRieszPotential β f)

Almost-everywhere measurable sources also have measurable potentials: their measurable representatives give the same potential at every point.