Almost-everywhere pointwise bounds for the localized heat potential #
Finite extended-real Riesz potentials give integrable real majorants at almost every evaluation point. All conversions to real numbers are made only after this finiteness has been established.
theorem
CKN.Core.Endgame.aemeasurable_euclidean_norm_of_components
{g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hg : ∀ (i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => g w i) MeasureTheory.volume)
:
Componentwise almost-everywhere measurability supplies measurability of the Euclidean norm used as the nonnegative potential source.
theorem
CKN.Core.Endgame.duhamel_bound_of_finite_riesz
{g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hg : ∀ (i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => g w i) MeasureTheory.volume)
(hh : ∀ (j i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => h j w i) MeasureTheory.volume)
(hgn :
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w))
MeasureTheory.volume)
(hhn :
∀ (j : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w))
MeasureTheory.volume)
{z : Foundation.Parabolic.ParabolicPoint}
(hgfin :
Foundation.Parabolic.Morrey.parabolicRieszPotential 2
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w)) z < ⊤)
(hhfin :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.parabolicRieszPotential 1
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w)) z < ⊤)
:
At every point where the norm-source Riesz potentials are finite, the actual Duhamel integral is bounded by its pointwise potential majorant.
theorem
CKN.Core.Endgame.pointwisePotentialBound_ae
{v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hg : ∀ (i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => g w i) MeasureTheory.volume)
(hh : ∀ (j i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => h j w i) MeasureTheory.volume)
(hgn :
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w))
MeasureTheory.volume)
(hhn :
∀ (j : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w))
MeasureTheory.volume)
(hgfin :
∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.Morrey.parabolicRieszPotential 2
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w)) z < ⊤)
(hhfin :
∀ (j : Fin 3),
∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), Foundation.Parabolic.Morrey.parabolicRieszPotential 1
(fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w)) z < ⊤)
(hrep : v =ᵐ[MeasureTheory.volume] Step3.duhamelPotential g h)
:
Almost-everywhere potential finiteness suffices; there is no all-point integrability premise on the heat or Riesz convolutions.
theorem
CKN.Core.Endgame.pointwisePotentialBound_ae_of_bootstrap_sources
{v g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{h : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{z₀ : Foundation.Parabolic.ParabolicPoint}
{R : ℝ}
(hR : 0 < R)
(hg : ∀ (i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => g w i) MeasureTheory.volume)
(hh : ∀ (j i : Fin 3), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => h j w i) MeasureTheory.volume)
(hgn :
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (g w))
MeasureTheory.volume)
(hhn :
∀ (j : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (h j w))
MeasureTheory.volume)
(hgN :
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 11) fun (w : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (g w)) < ⊤)
(hhN :
∀ (j : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm 3 (25 / 6) fun (w : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (h j w)) < ⊤)
(hgsupp : ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, g w = 0)
(hhsupp : ∀ (j : Fin 3), ∀ w ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, h j w = 0)
(hrep : v =ᵐ[MeasureTheory.volume] Step3.duhamelPotential g h)
:
Boundedly supported sources at the first bootstrap exponents supply the almost-everywhere finiteness required by the pointwise potential estimate.