Absolute thresholds for the clipped pressure-gradient slots #
The two actual-integral estimates are used above one fixed absolute Calderón–Zygmund threshold. Their spatial and temporal clipping is preserved.
theorem
CKN.Core.Endgame.theoremA_hGA_of_integral_slots_threshold
(Cstar : ℝ)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cstar ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ Step4.originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal
(r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
(hBIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cstar ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∫⁻ (s : ℝ) in Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ ENNReal.ofReal (|C_CZ| + 1) * ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1) * ENNReal.ofReal
(max 1
((2 * R₁ / (1 - R₁)) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))))
(q τ C_CZ R₀ R₁ ε : ℝ)
(KU KD : ENNReal)
:
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cstar ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD < ⊤ ∧ ∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (J : Set ℝ),
localBox Ω I U J →
U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ →
∀ (i : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet U J))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ ∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder 0 0 R₁).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) ≤ Step4.oneSidedPressureGradientKPAffine q τ C_CZ R₀ R₁ ε KU KD
The actual clipped cell and time-mass bounds above a fixed threshold produce the affine pressure-gradient estimate at every admissible constant.
theorem
CKN.Core.Endgame.epsilonRegularityL3_of_threshold_slots
(Cslot : ℝ)
(hCslot : 0 ≤ Cslot)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cslot ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ Step4.originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal
(r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
(hBIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cslot ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∫⁻ (s : ℝ) in Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ ENNReal.ofReal (|C_CZ| + 1) * ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1) * ENNReal.ofReal
(max 1
((2 * R₁ / (1 - R₁)) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))))
(q : ℝ)
(hq : 5 / 2 < q)
:
∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ),
0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(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),
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
∫⁻ (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 ε₀ →
∃ (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 γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z
The small-data conclusion from the two actual-integral slots.
The final absolute constant is the maximum of their common threshold and
9 * max czP1OperatorConstant 0, so the same constant also supplies the
singly centred Calderón–Zygmund estimate. The endgame uses C_CZ = Cstar
and C₁₂_p1 = Cstar * 9 * sobolevPoincareL6Constant.toReal.
theorem
CKN.Core.Endgame.epsilonRegularityL3_of_separate_threshold_slots
(CA CB : ℝ)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
CA ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ Step4.originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal
(r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
(hBIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
CB ≤ C_CZ →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ}
{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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) ≤ KD) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i
(fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) →
∀ (i : Fin 3),
∫⁻ (s : ℝ) in Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ ENNReal.ofReal (|C_CZ| + 1) * ENNReal.ofReal (|R₀| + |R₁| + |ε| + 1) * ENNReal.ofReal
(max 1
((2 * R₁ / (1 - R₁)) ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))))
(q : ℝ)
(hq : 5 / 2 < q)
:
∃ (ε₀ : ℝ) (γ₀ : ℝ) (C₄ : ℝ),
0 < ε₀ ∧ 0 < γ₀ ∧ γ₀ ≤ 2 / 3 ∧ 0 ≤ C₄ ∧ ∀ (Ω : Set Foundation.Parabolic.Vec3) (I : Set ℝ)
(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),
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
∫⁻ (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 ε₀ →
∃ (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 γ₀ C₄ ∧ ∀ z ∈ Foundation.Parabolic.vec3Ball 0 (1 / 2) ×ˢ Set.Ioo (-(1 / 4)) 0, IsRegularPoint Ω I u z
Combine the independent absolute cell and time-mass thresholds with the singly centred Calderón–Zygmund constant. Their maximum is nonnegative without any additional hypothesis. Repeating the maximum with the Calderón–Zygmund constant in the common-threshold theorem leaves it unchanged.