Geometric bounds and convergence of superlinear recurrences

Let Y : ℕ → ℝ be a nonnegative sequence satisfying the superlinear recurrence

Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)

with b ≥ 0 and α ≥ 0. If q ≥ 0, b * q ^ α ≤ 1, and C * Y 0 ^ α ≤ q, then Y n ≤ q ^ n * Y 0. When q < 1, this bound implies Y n → 0. In its classical form, for C > 0, b > 1, α > 0,

Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹) implies Y n ≤ (b ^ (-α⁻¹)) ^ n * Y 0, so Y n → 0.

This is the numerical lemma behind De Giorgi's method. In the proof of local boundedness of weak subsolutions of a divergence-form elliptic equation, Y n is the L² mass of the truncation (u - kₙ)⁺ on a ball B_{rₙ}, along increasing levels kₙ and shrinking radii rₙ. The Caccioppoli inequality for truncations, the Sobolev inequality and Chebyshev's inequality combine into a recurrence of the above shape, with b accounting for the geometric shrinking of the gaps rₙ - rₙ₊₁ and kₙ₊₁ - kₙ. The vanishing of the limit then says that u is bounded above on the limiting ball by the limiting level.

The general statement TauCeti.le_geom_of_le_mul_pow_mul_rpow only asks for a ratio q with b * q ^ α ≤ 1 and C * Y 0 ^ α ≤ q; the classical threshold is the choice q = b ^ (-α⁻¹).

Main declarations

• TauCeti.le_geom_of_le_mul_pow_mul_rpow: geometric bound Y n ≤ q ^ n * Y 0 for a superlinear recurrence from a small start.
• TauCeti.le_rpow_neg_inv_pow_mul_of_le_mul_pow_mul_rpow: the same bound at the classical threshold Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹), with ratio b ^ (-α⁻¹).
• TauCeti.tendsto_atTop_zero_of_le_mul_pow_mul_rpow_of_ratio_lt_one: for q < 1, the sequence tends to zero.
• TauCeti.tendsto_atTop_zero_of_le_mul_pow_mul_rpow: convergence at the classical threshold when b > 1.

References

• E. DiBenedetto, Degenerate Parabolic Equations, Chapter I, Lemma 4.1 (fast geometric convergence).
• O. A. Ladyzhenskaya, N. N. Ural'tseva, Linear and Quasilinear Elliptic Equations, Chapter 2, Lemma 4.7.
• The same recurrence is closed out in Scott Armstrong and Julia Kempe's Apache-2.0 scottnarmstrong/DeGiorgi/DeGiorgi/DeGiorgiIteration/Recurrence.lean, commit 4c1b3077d3782b24065184df4ba59501b2e56fc7 (DeGiorgi.deGiorgi_recurrence_closeout), by a rescaling argument; the proof here is the direct induction of DiBenedetto.

theorem TauCeti.le_geom_of_le_mul_pow_mul_rpow {Y : ℕ → ℝ} {C b q α : ℝ} (hY : ∀ (n : ℕ), 0 ≤ Y n) (hb : 0 ≤ b) (hq : 0 ≤ q) (hα : 0 ≤ α) (hbq : b * q ^ α ≤ 1) (h0 : C * Y 0 ^ α ≤ q) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)) (n : ℕ) : Y n ≤ q ^ n * Y 0

Geometric bound. Let Y be a nonnegative sequence with

Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)

for some b ≥ 0 and α ≥ 0. If q ≥ 0 satisfies b * q ^ α ≤ 1 and the starting value is small in the sense that C * Y 0 ^ α ≤ q, then Y n ≤ q ^ n * Y 0 for every n.

No sign condition on C is needed.

theorem TauCeti.le_rpow_neg_inv_pow_mul_of_le_mul_pow_mul_rpow {Y : ℕ → ℝ} {C b α : ℝ} (hY : ∀ (n : ℕ), 0 ≤ Y n) (hC : 0 < C) (hb : 0 < b) (hα : 0 < α) (h0 : Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹)) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)) (n : ℕ) : Y n ≤ (b ^ (-α⁻¹)) ^ n * Y 0

Geometric bound, classical threshold. Let Y be a nonnegative sequence with

Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)

for constants C > 0, b > 0 and α > 0. If Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹), then Y n ≤ (b ^ (-α⁻¹)) ^ n * Y 0 for every n.

theorem TauCeti.tendsto_atTop_zero_of_le_mul_pow_mul_rpow_of_ratio_lt_one {Y : ℕ → ℝ} {C b q α : ℝ} (hY : ∀ (n : ℕ), 0 ≤ Y n) (hb : 0 ≤ b) (hq : 0 ≤ q) (hq1 : q < 1) (hα : 0 ≤ α) (hbq : b * q ^ α ≤ 1) (h0 : C * Y 0 ^ α ≤ q) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)) : Filter.Tendsto Y Filter.atTop (nhds 0)

Convergence to zero from a geometric bound. If the ratio q in le_geom_of_le_mul_pow_mul_rpow is less than one, then Y n → 0.

theorem TauCeti.tendsto_atTop_zero_of_le_mul_pow_mul_rpow {Y : ℕ → ℝ} {C b α : ℝ} (hY : ∀ (n : ℕ), 0 ≤ Y n) (hC : 0 < C) (hb : 1 < b) (hα : 0 < α) (h0 : Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹)) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)) : Filter.Tendsto Y Filter.atTop (nhds 0)

Fast geometric convergence to zero, classical threshold. Let Y be a nonnegative sequence with

Y (n + 1) ≤ C * b ^ n * Y n ^ (1 + α)

for constants C > 0, b > 1 and α > 0. If Y 0 ≤ C ^ (-α⁻¹) * b ^ (-(α ^ 2)⁻¹), then Y n → 0. This is the form in which De Giorgi's iteration concludes.