Adams estimates for almost-everywhere measurable sources

A measurable representative preserves the source Morrey norm and the Riesz potential at every evaluation point. Thus the scalar Adams estimate does not require pointwise measurability of the original source.

theorem CKN.Core.Endgame.riesz_adams_of_aemeasurable {P τ β : ℝ} (hP : 1 < P) (hPτ : P ≤ τ) (hβ : 0 < β) (hβτ : β * τ < 5) {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) : (Foundation.Parabolic.Morrey.morreyNorm (P / (1 - β * τ / 5)) (τ / (1 - β * τ / 5)) fun (z : Foundation.Parabolic.ParabolicPoint) => (Foundation.Parabolic.Morrey.parabolicRieszPotential β f z).toReal) ≤ Foundation.Parabolic.Morrey.parabolicAdamsPotentialConstant β P τ * Foundation.Parabolic.Morrey.morreyNorm P τ f

The quantitative Adams estimate is invariant under almost-everywhere changes of the source.

theorem CKN.Core.Endgame.order_two_adams_lower_three_of_aemeasurable {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) f < ⊤) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => (Foundation.Parabolic.Morrey.parabolicRieszPotential 2 f z).toReal) < ⊤

The order-two estimate at the first bootstrap exponents, lowered to integrability exponent three. All numerical constants are discharged.

theorem CKN.Core.Endgame.order_one_adams_lower_three_of_aemeasurable {f : Foundation.Parabolic.ParabolicPoint → ℝ} (hf : AEMeasurable f MeasureTheory.volume) (hN : Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) f < ⊤) : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => (Foundation.Parabolic.Morrey.parabolicRieszPotential 1 f z).toReal) < ⊤

The order-one estimate at the first bootstrap exponents, lowered to integrability exponent three.