Local regularity from pressure-gradient and localized-source estimates #
The velocity improvement and pressure-gradient construction are used on nested balls before localizing the equation and applying the heat estimate.
Local regularity from actual heat-potential sources #
An almost-everywhere heat representation transfers the quantitative estimate for compactly supported Morrey sources to the represented velocity.
theorem
CKN.Core.Endgame.regular_point_of_heat_sources
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{R γ θ₀ θ₁ P : ℝ}
(hR : 0 < R)
(hball : Metric.ball z R ⊆ spaceTimeSet Ω I)
(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 (Metric.ball z R)] 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 (Metric.ball z R)] u ∧ ParabolicHolderVecNormLE (Metric.ball z R) w γ
(vectorHeatValueBound F G γ θ₀ θ₁ P z R + vectorHeatHolderCoefficient F G γ θ₀ θ₁ P) ∧ IsRegularPoint Ω I u z
Genuine Morrey sources and an almost-everywhere heat representation give a bounded Hölder representative and regularity at the center of the ball.
theorem
CKN.Core.Endgame.regular_point_of_heat_sources_at_step_parameters
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{u F : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{G : Fin 3 → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{z : Foundation.Parabolic.ParabolicPoint}
{R q : ℝ}
(hq : 5 / 2 < q)
(hR : 0 < R)
(hball : Metric.ball z R ⊆ spaceTimeSet Ω I)
(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 (6 / 5) (stepTheta₀ (stepGamma₀ q))
fun (x : Foundation.Parabolic.ParabolicPoint) => F x i) < ⊤)
(hNG :
∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (stepTheta₁ (stepGamma₀ q))
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 (Metric.ball z R)] 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 (Metric.ball z R)] u ∧ ParabolicHolderVecNormLE (Metric.ball z R) w (stepGamma₀ q)
(vectorHeatValueBound F G (stepGamma₀ q) (stepTheta₀ (stepGamma₀ q)) (stepTheta₁ (stepGamma₀ q)) (6 / 5) z R + vectorHeatHolderCoefficient F G (stepGamma₀ q) (stepTheta₀ (stepGamma₀ q)) (stepTheta₁ (stepGamma₀ q))
(6 / 5)) ∧ IsRegularPoint Ω I u z
The standing exponent choices discharge all numerical conditions of the
heat regularity estimate at integrability exponent 6/5.
theorem
CKN.Core.Endgame.holder_representative_of_local_producers
(q : ℝ)
(hq : 5 / 2 < q)
(hG :
∀ (q τ : ℝ),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
∀ {Ω : 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 →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 τ (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆
⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ morreyVecMem (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (Metric.ball z₀ (R / 2)) Dp)
(hB :
∀ (q : ℝ),
5 / 2 < q →
∀ {Ω : 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 →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
morreyVecMem 3 25 (Metric.ball z₀ (R / 4)) u)
(hL :
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ},
φ ∈ spaceTimeTestFunction Ω I →
∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ},
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
(∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) →
(∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Ω' ×ˢ J →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) →
Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j w i)
z)
(hS :
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ},
φ ∈ spaceTimeTestFunction Ω I →
∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ},
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
5 / 2 < q →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
tsupport φ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ R →
morreyVecMem 3 25 (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R)
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) →
∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ R))) →
morreyVecMem (6 / 5) (min q (25 / 9)) (Metric.ball z₀ R) Dp →
(∀ (i : Fin 3),
AEMeasurable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i)
MeasureTheory.volume) ∧ (∀ (j i : Fin 3),
AEMeasurable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i)
MeasureTheory.volume) ∧ (∀ (i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i) ∧ (∀ (j i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i) ∧ (∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i) < ⊤) ∧ ∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3)
fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i) < ⊤)
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(z₀ : Foundation.Parabolic.ParabolicPoint)
(R : ℝ)
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
(hu : morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u)
(hDu :
∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i)
:
∃ (w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
w =ᵐ[MeasureTheory.volume.restrict (Metric.ball z₀ (R / 16 / 8))] u ∧ ParabolicHolderVecOn (Metric.ball z₀ (R / 16 / 8)) w (stepGamma₀ q)
The localized equation and source estimates give a representative on a fixed smaller ball with the standing Hölder exponent.
theorem
CKN.Core.Endgame.regular_point_of_local_producers
(q : ℝ)
(hq : 5 / 2 < q)
(hG :
∀ (q τ : ℝ),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
∀ {Ω : 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 →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 τ (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ (R / 2)))) ∧ (∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆
⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ (R / 2) →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ morreyVecMem (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q) (Metric.ball z₀ (R / 2)) Dp)
(hB :
∀ (q : ℝ),
5 / 2 < q →
∀ {Ω : 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 →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) →
morreyVecMem 3 25 (Metric.ball z₀ (R / 4)) u)
(hL :
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ},
φ ∈ spaceTimeTestFunction Ω I →
∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ},
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
(∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet Ω' J))) →
(∀ (i : Fin 3),
∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ,
tsupport ψ ⊆ Ω' ×ˢ J →
∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) →
Step3.localizedVelocity φ u =ᵐ[MeasureTheory.volume]
fun (z : Foundation.Parabolic.ParabolicPoint) (i : Fin 3) =>
HeatPotential.heatPotential
(fun (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp w i)
(fun (j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j w i)
z)
(hS :
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
∀ {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ},
φ ∈ spaceTimeTestFunction Ω I →
∀ {Ω' : Set Foundation.Parabolic.Vec3} {J : Set ℝ},
localBox Ω I Ω' J →
tsupport φ ⊆ Ω' ×ˢ J →
∀ (z₀ : Foundation.Parabolic.ParabolicPoint) (R : ℝ),
0 < R →
5 / 2 < q →
Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I →
tsupport φ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ R →
morreyVecMem 3 25 (Metric.ball z₀ R) u →
(∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ R)
fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i) →
∀ {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3},
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ R))) →
morreyVecMem (6 / 5) (min q (25 / 9)) (Metric.ball z₀ R) Dp →
(∀ (i : Fin 3),
AEMeasurable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i)
MeasureTheory.volume) ∧ (∀ (j i : Fin 3),
AEMeasurable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i)
MeasureTheory.volume) ∧ (∀ (i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i) ∧ (∀ (j i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i) ∧ (∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceG φ u Du f Dp z i) < ⊤) ∧ ∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3)
fun (z : Foundation.Parabolic.ParabolicPoint) =>
Step4.localizedGradientSourceH φ u j z i) < ⊤)
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(z₀ : Foundation.Parabolic.ParabolicPoint)
(R : ℝ)
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
(hu : morreyVecMem 3 (25 / 3) (Metric.ball z₀ R) u)
(hDu :
∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i)
:
IsRegularPoint Ω I u z₀
The explicit local analytic estimates imply regularity at the center.