Neighborhood Morrey data from the gradient criterion #
The smallness premise stays in the extended nonnegative reals. The only
additional estimate is the pair of one-step inequalities in lem:theta-decay.
theorem
CKN.Core.Endgame.morrey_sources_of_gradient_limsup
{Ω : 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}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hq : 5 / 2 < q)
{z₀ : Foundation.Parabolic.ParabolicPoint}
(hz₀ : z₀ ∈ spaceTimeSet Ω I)
{C₂₇ C₂₈ : ℝ}
(hC₂₇ : 0 < C₂₇)
(hC₂₈ : 0 < C₂₈)
(h_theta_decay :
∀ {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ},
0 < ρ →
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I →
theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₇ * iterationKappa C₂₇ ^ (-5) * (beta u Du z ρ ^ (1 / 2) + beta u Du z ρ) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f z ρ ∧ (theta (iterationKappa C₂₇) u Du p z ρ ≤ 1 →
theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p z ρ + 2 * C₂₇ * iterationKappa C₂₇ ^ (-5) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p z ρ ^ (1 / 2) * lambda q f z ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f z ρ))
(h_beta_decay :
Filter.limsup
(fun (r : ℝ) =>
(ENNReal.ofReal r)⁻¹ * ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 r, ENNReal.ofReal (spatialGradientSq u Du w))
(nhdsWithin 0 (Set.Ioi 0)) < ENNReal.ofReal (iterationEpsilonStar C₂₇ ^ 2))
:
∃ (r₂ : ℝ) (M : ℝ),
0 < r₂ ∧ 1 ≤ M ∧ Metric.ball z₀ (2 * r₂) ⊆ spaceTimeSet Ω I ∧ (∀ z ∈ Metric.ball z₀ r₂,
∀ (r : ℝ), 0 < r → r < r₂ → max (max (alpha u z r) (beta u Du z r)) (delta p z r ^ 2) ≤ M * r ^ (2 / 5)) ∧ morreyVecMem 3 (25 / 3) (Metric.ball z₀ (r₂ / 4)) u ∧ (∀ (i : Fin 3),
morreyVecMem 2 (25 / 8) (Metric.ball z₀ (r₂ / 4)) fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i) ∧ Foundation.Parabolic.Morrey.morreyBallNorm (3 / 2) (25 / 8) ((Metric.ball z₀ (r₂ / 4)).indicator p) < ⊤
Neighborhood decay and the three initial Morrey memberships, obtained from the gradient limsup and the one-step theta inequalities.