Pressure-gradient estimates at the two exponent-radius triples #
The proof of thm:A uses lem:pressure-gradient-morrey exactly twice: once
inside the bootstrap round prop:bootstrap at velocity exponent τ = 25/3,
and once inside thm:endgame at τ = 25. Each use fixes the two radii as
well, so only the triples (25/3, 11/16, 43/64) and (25, 5/8, 19/32) are
needed. The estimates in this module carry that restriction, together with a
lower bound on the Calderón-Zygmund constant so that a single constant
dominates every coefficient the two estimates require; enlarging that
constant weakens nothing.
epsilonRegularityL3_of_instance_slots_q is the proof of thm:A itself.
Its steps are, in order: the start lemma lem:thmA-start and Steps 1 and 2
(theoremA_initial_uniform_of_displays), the single bootstrap round of
prop:bootstrap and cor:one-round
(exists_uniform_bootstrap_of_initial_pressure), and thm:endgame on the
one-sided cylinder (exists_uniform_halfCylinder_of_final_pressure), with
all sources split at t = 0 as Step 3 requires. The same composition is
written, with an unrestricted pressure-gradient hypothesis, in
CKN.Core.Endgame.epsilonRegularityL3_closer_of_pending_inputs.
theorem
CKN.Core.Endgame.theoremA_hGA_of_integral_slots_instances_q
(Cstar : ℝ → ℝ)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cstar q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 two actual-integral slots at the prescribed exponent/radius triples produce the affine pressure-gradient estimate at those same triples.
theorem
CKN.Core.Endgame.epsilonRegularityL3_of_instance_slots_q
(Cslot : ℝ → ℝ)
(hCslot : ∀ (q : ℝ), 0 ≤ Cslot q)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cslot q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 actual-integral slots at the two triples used by the bootstrap and final pressure steps. The coefficient depending only on the force exponent also absorbs the singly centred Calderón–Zygmund constant.
theorem
CKN.Core.Endgame.epsilonRegularityL3_of_separate_instance_slots_q
(CA CB : ℝ → ℝ)
(hAIntegral :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
CA q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
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 cell and time-mass threshold functions 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.