Iteration #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The paper proposition is exposed conditionally until the analytic one-step estimate is available.
theorem
CKN.iteration_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)
{z : Foundation.Parabolic.ParabolicPoint}
{r₅ C₂₇ C₂₈ : ℝ}
(hC₂₇ : 0 < C₂₇)
(hC₂₈ : 0 < C₂₈)
(hr₅ : 0 < r₅)
(hz : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 r₅) ⊆ spaceTimeSet Ω I)
(hθ₅ : theta (iterationKappa C₂₇) u Du p z r₅ ≤ iterationEta C₂₇)
(hLam₅ : lambda q f z r₅ ≤ iterationLambda₀ C₂₇ C₂₈)
(hThetaDecay :
∀ {w : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ},
0 < ρ →
closure (Foundation.Parabolic.parabolicCylinder w.1 w.2 ρ) ⊆ spaceTimeSet Ω I →
theta (iterationKappa C₂₇) u Du p w (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₇ * iterationKappa C₂₇ ^ (-5) * (beta u Du w ρ ^ (1 / 2) + beta u Du w ρ) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * lambda q f w ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f w ρ ∧ (theta (iterationKappa C₂₇) u Du p w ρ ≤ 1 →
theta (iterationKappa C₂₇) u Du p w (iterationKappa C₂₇ * ρ) ≤ C₂₇ * iterationKappa C₂₇ ^ (2 / 3) * theta (iterationKappa C₂₇) u Du p w ρ + 2 * C₂₇ * iterationKappa C₂₇ ^ (-5) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ + C₂₈ * iterationKappa C₂₇ ^ (-1 / 2) * theta (iterationKappa C₂₇) u Du p w ρ ^ (1 / 2) * lambda q f w ρ ^ (1 / 2) + C₂₈ * iterationKappa C₂₇ ^ (-3) * lambda q f w ρ))
:
(∀ (n : ℕ),
theta (iterationKappa C₂₇) u Du p z (iterationKappa C₂₇ ^ n * r₅) ≤ iterationEta C₂₇ * iterationKappa C₂₇ ^ (↑n * iterationEpsilon)) ∧ ∀ (r : ℝ),
0 < r →
r ≤ r₅ →
theta (iterationKappa C₂₇) u Du p z r ≤ iterationKappa C₂₇ ^ (-4 / 3 - iterationEpsilon) * iterationEta C₂₇ * r₅ ^ (-iterationEpsilon) * r ^ iterationEpsilon
Conditional form of prop:iteration, consuming the two inequalities of
lem:theta-decay as its only additional analytic input.