Theta Descent

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.theta_descent_uniform {C₂₇ C₂₈ : ℝ} (hC₂₇ : 0 < C₂₇) (hC₂₈ : 0 < C₂₈) {Θ : ℕ → ℝ → ℝ} {S : Set ℝ} {Tbar Lbar : ℝ} (hΘ : ∀ (n : ℕ), ∀ s ∈ S, 0 ≤ Θ n s) (hΘ0 : ∀ s ∈ S, Θ 0 s ≤ Tbar) (hrec : ∀ (n : ℕ), ∀ s ∈ S, Θ (n + 1) s ≤ 3 / 8 * Θ n s + CKN.iterationC₂₉ C₂₇ C₂₈ * Lbar) (hL : 0 ≤ Lbar) (hLsmall : CKN.iterationC₂₉ C₂₇ C₂₈ * Lbar ≤ CKN.iterationEta C₂₇ / 16) : ∃ (N : ℕ), ∀ s ∈ S, Θ N s ≤ CKN.iterationEta C₂₇