StampacchiaDecay.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Geometric decay in the torsion superlevel iteration

theorem OAI.RegularPointCoordinates.power_recurrence_decay line 16

Source documentation

The superlinear recurrence contracts once its initial coefficient and geometric amplification satisfy the displayed scalar bounds.

theorem power_recurrence_decay {Y : ℕ → ℝ} {A B V θ q : ℝ}
    (hY : ∀ j, 0 ≤ Y j) (hA : 0 ≤ A) (hB : 0 ≤ B)
    (hV : 0 < V) (hθ : 0 < θ) (hq : 1 < q)
    (hstart : Y 0 ≤ V) (hsmall : A * V ^ (q - 1) ≤ θ)
    (hamp : B * θ ^ (q - 1) ≤ 1)
    (hstep : ∀ j, Y (j + 1) ≤ A * B ^ j * (Y j) ^ q) :
    ∀ j, Y j ≤ V * θ ^ j := by
…

theorem OAI.RegularPointCoordinates.eq_zero_of_le_geometric line 55
Source documentation
A nonnegative number below every term of a decaying geometric majorant is zero.
```
theorem eq_zero_of_le_geometric {a V θ : ℝ} (ha : 0 ≤ a)
    (hθ0 : 0 ≤ θ) (hθ1 : θ < 1) (hle : ∀ j : ℕ, a ≤ V * θ ^ j) : a = 0 := by
…
```