The velocity average supplied by the small-data hypothesis #
The original nonnegative sum in the unit-cylinder hypothesis controls the cubic velocity average on the half-cylinder. This supplies the absolute-value part of the reanchored heat representative without any additional assumption on that average.
theorem
CKN.Core.Endgame.halfCylinder_velocity_average_of_small_data
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q ε₀ : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hε₀ : 0 ≤ ε₀)
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hsmall :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀)
:
MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x))
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume ∧ MeasureTheory.IntegrableOn
(fun (x : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3)
(Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2)) MeasureTheory.volume ∧ (⨍ (x : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2), Foundation.Parabolic.vec3EuclideanNorm (u x) ^ 3) ^ (1 / 3) ≤ ((MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))).toReal⁻¹ * ε₀) ^ (1 / 3)
The full small-data hypothesis bounds the half-cylinder velocity average and supplies both integrability conditions used in reanchoring.
theorem
CKN.Core.Endgame.halfCylinder_representative_of_heat_sources_of_small_data
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q ε₀ γ θ₀ θ₁ P : ℝ}
{u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hε₀ : 0 ≤ ε₀)
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hsmall :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε₀)
(hγ : 0 < γ)
(hγ1 : γ < 1)
(hθ₀ : 1 / θ₀ = (2 - γ) / 5)
(hθ₁ : 1 / θ₁ = (1 - γ) / 5)
(hP : 1 ≤ P)
(hPθ₀ : P ≤ θ₀)
(hPθ₁ : P ≤ θ₁)
(hF : ∀ (i : Fin 3), AEMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) MeasureTheory.volume)
(hG : ∀ (j i : Fin 3), AEMeasurable (fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) MeasureTheory.volume)
(hNF :
∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm P θ₀ fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) < ⊤)
(hNG :
∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm P θ₁ fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i) < ⊤)
(hSupportF : ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.ParabolicPoint) => F x i)
(hSupportG : ∀ (j i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.ParabolicPoint) => G j x i)
(hrep :
u =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
fun (x : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential (fun (y : Foundation.Parabolic.ParabolicPoint) => F y i)
(fun (j : Fin 3) (y : Foundation.Parabolic.ParabolicPoint) => G j y i) x)
:
∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))] u ∧ ParabolicHolderVecNormLE (closure (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))) w γ
(2 * vectorHeatHolderCoefficient F G γ θ₀ θ₁ P + ((MeasureTheory.volume (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))).toReal⁻¹ * ε₀) ^ (1 / 3)) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z
The original small-data hypothesis and genuine heat sources give a closed-half-cylinder representative whose explicit norm uses only the source coefficient and the small-data threshold, together with interior regularity.