Potential Local Lp Measure

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

theorem CKN.Foundation.Euclidean.aestronglyMeasurable_pressureNewtonianPotential {G : Parabolic.Vec3 → ℝ} (hG : Measurable G) : MeasureTheory.AEStronglyMeasurable (pressureNewtonianPotential G) MeasureTheory.volume

The Newtonian potential of measurable data is almost everywhere strongly measurable.

theorem CKN.Foundation.Euclidean.aestronglyMeasurable_pressureNewtonianDerivativePotential (i : Fin 3) {G : Parabolic.Vec3 → ℝ} (hG : Measurable G) : MeasureTheory.AEStronglyMeasurable (pressureNewtonianDerivativePotential i G) MeasureTheory.volume

The first-derivative Newtonian potential of measurable data is almost everywhere strongly measurable.

theorem CKN.Foundation.Euclidean.pressureNewtonianPotential_congr_of_ae_eq {G G' : Parabolic.Vec3 → ℝ} (h : G =ᵐ[MeasureTheory.volume] G') : pressureNewtonianPotential G = pressureNewtonianPotential G'

The Newtonian potential only sees the data up to a null set, so it is unchanged when the data is replaced by an almost-everywhere equal function.

theorem CKN.Foundation.Euclidean.pressureNewtonianDerivativePotential_congr_of_ae_eq (i : Fin 3) {G G' : Parabolic.Vec3 → ℝ} (h : G =ᵐ[MeasureTheory.volume] G') : pressureNewtonianDerivativePotential i G = pressureNewtonianDerivativePotential i G'

The same statement for the first-derivative Newtonian potential.