Almost-everywhere finiteness of subcritical potentials

Bounded support turns a finite Morrey norm into a finite global power integral. The maximal estimate and the unoptimized Hedberg estimate then give finiteness of the extended-real potential almost everywhere, before any use of its real-valued conversion.

theorem CKN.Core.Endgame.source_power_integral_lt_top {P τ R : ℝ} (hP : 0 < P) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ f < ⊤) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, f z = 0) : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint), ENNReal.ofReal |f z| ^ P < ⊤

A bounded-support Morrey source has finite global power integral.

theorem CKN.Core.Endgame.riesz_potential_ae_lt_top_of_morrey {β P τ R : ℝ} (hβ : 0 < β) (hP : 1 < P) (hPτ : P ≤ τ) (hβτ : β * τ < 5) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : Measurable f) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ f < ⊤) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, f z = 0) : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.Morrey.parabolicRieszPotential β f z < ⊤

In the strict subcritical range, a bounded-support Morrey source has a finite extended-real Riesz potential almost everywhere.

theorem CKN.Core.Endgame.morrey_norm_congr_ae {P τ : ℝ} {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hfg : f =ᵐ[MeasureTheory.volume] g) : Foundation.Parabolic.Morrey.morreyNorm P τ f = Foundation.Parabolic.Morrey.morreyNorm P τ g

Almost-everywhere changes of a scalar source preserve its Morrey norm.

theorem CKN.Core.Endgame.riesz_potential_congr_ae {β : ℝ} {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hfg : f =ᵐ[MeasureTheory.volume] g) (z : Foundation.Parabolic.ParabolicPoint) : Foundation.Parabolic.Morrey.parabolicRieszPotential β f z = Foundation.Parabolic.Morrey.parabolicRieszPotential β g z

Almost-everywhere changes of a source preserve the extended-real potential at every evaluation point.

theorem CKN.Core.Endgame.riesz_potential_ae_lt_top_of_aemeasurable_morrey {β P τ R : ℝ} (hβ : 0 < β) (hP : 1 < P) (hPτ : P ≤ τ) (hβτ : β * τ < 5) (hR : 0 < R) {z₀ : Foundation.Parabolic.ParabolicPoint} {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ f < ⊤) (hsupp : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, f z = 0) : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.Morrey.parabolicRieszPotential β f z < ⊤

The subcritical finiteness theorem needs only almost-everywhere measurability; a measurable representative is truncated to the same support.