Closed-cylinder control using only past-time source bounds #
The smooth localization may depend on the future boundary of the domain. Only its sources at times at most zero contribute on the target cylinder. Consequently the numerical bounds below concern the truncated sources only.
theorem
CKN.Core.Endgame.uniform_halfCylinder_representative_of_past_source_bounds
(q ε₀ : ℝ)
(KF KG : ENNReal)
(hq : 5 / 2 < q)
(hε₀ : 0 ≤ ε₀)
(hKF : KF < ⊤)
(hKG : KG < ⊤)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{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}
(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 ε₀)
(hF :
∀ (i : Fin 3),
AEMeasurable
({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
F z i)
MeasureTheory.volume)
(hG :
∀ (j i : Fin 3),
AEMeasurable
({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
G j z i)
MeasureTheory.volume)
(hNF :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
F z i) ≤ KF)
(hNG :
∀ (j i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3)
({z : Foundation.Parabolic.ParabolicPoint | z.2 ≤ 0}.indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
G j z i) ≤ KG)
(hFsupp :
∀ (z : Foundation.Parabolic.ParabolicPoint), z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → F z = 0)
(hGsupp :
∀ (j : Fin 3) (z : Foundation.Parabolic.ParabolicPoint),
z.2 ≤ 0 → z ∉ Foundation.Parabolic.parabolicCylinder 0 0 1 → G j z = 0)
(hrep :
u =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder 0 0 (1 / 2))]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential (fun (w : Foundation.Parabolic.ParabolicPoint) => F w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) => G j w i) z)
:
∃ (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 (stepGamma₀ q)
(uniformHalfCylinderHolderBound q ε₀ KF KG) ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z
The uniform half-cylinder estimate needs no bound on future-time sources. The source representation is retained before truncation, and causality proves the required representation after truncation.