Decay

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Discrete form of the scale iteration used for a rate strictly below three.

theorem CKN.Core.Step4.geometric_decay_iteration {θ σ A B : ℝ} (hθ : 0 ≤ θ) (hσ : 0 ≤ σ) (hθσ : θ < σ) (hA : 0 ≤ A) (hB : 0 ≤ B) {a : ℕ → ℝ} : 0 ≤ a 0 → ∀ (haA : a 0 ≤ A) (hrec : ∀ (n : ℕ), a (n + 1) ≤ θ * a n + B * σ ^ n) (n : ℕ), a n ≤ (A + B / (σ - θ)) * σ ^ n

theorem CKN.Core.Step4.morrey_exponent_from_decay {κ β : ℝ} (hκ : 0 < κ) : 0 ≤ β → ∀ (hβ5 : β < 5) (hβκ : β = 5 - 5 * (6 / 5) / κ), κ = 6 / (5 - β)

theorem CKN.Core.Step4.gradientMorreyExponent {τ τ₃ q : ℝ} : 0 < τ → 0 < τ₃ → ∀ (hq : 0 < q) (hτcond : 1 / τ + 1 / τ₃ > 0), 0 < min (1 / τ + 1 / τ₃)⁻¹ q

theorem CKN.Core.Step4.morreyNorm_le_of_cell_bound {p q : ℝ} {g : Foundation.Parabolic.ParabolicPoint → ℝ} {C : ENNReal} (hcell : ∀ (z : Foundation.Parabolic.ParabolicPoint) (r : { r : ℝ // 0 < r }), Foundation.Parabolic.Morrey.morreyCell p q g z ↑r ≤ C) : Foundation.Parabolic.Morrey.morreyNorm p q g ≤ C

A scale recurrence is the discrete form of the two-scale estimate used for the pressure gradient. The parameters are deliberately exposed: the conversion from a continuous scale to the geometric sequence belongs to the caller, while this lemma contains the complete iteration.

theorem CKN.Core.Step4.decay_iteration {θ σ A B : ℝ} {a : ℕ → ℝ} (hθ : 0 ≤ θ) (hσ : 0 ≤ σ) (hθσ : θ < σ) (hA : 0 ≤ A) (hB : 0 ≤ B) (ha : 0 ≤ a 0) (haA : a 0 ≤ A) (hrec : ∀ (n : ℕ), a (n + 1) ≤ θ * a n + B * σ ^ n) (n : ℕ) : a n ≤ (A + B / (σ - θ)) * σ ^ n