Morrey Decay #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The remaining assembly uses the standing constants from the iteration convention; the one-step decay display is its only analytic hypothesis.
theorem
CKN.morreyDecay_of_thetaDecay
{Ω : 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₂₈)
(hThetaDecay :
∀ {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βlim :
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))
: