OAI/Geometry/RCD/Coordinates/NonlinearIteration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.superlinear_geometric_barrier line 16

   Source documentation

   A superlinear recurrence stays below a geometric barrier whenever the two scalar barrier inequalities hold.

   theorem superlinear_geometric_barrier {Y : ℕ → ℝ} {C b ε A q : ℝ}
       (hY : ∀ i, 0 ≤ Y i) (hC : 0 ≤ C) (hb : 0 ≤ b) (hε : 0 < ε)
       (hA : 0 < A) (hq : 0 < q) (hstart : Y 0 ≤ A)
       (hAq : C*A^ε ≤ q) (hbq : b*q^ε ≤ 1)
       (hrec : ∀ i, Y (i+1) ≤ C*b^i*(Y i)^(1+ε)) :
       ∀ i, Y i ≤ A*q^i := by
   …

2. theorem OAI.RegularPointCoordinates.exists_superlinear_decay_threshold line 46

   Source documentation

   For each superlinear recurrence there is a positive starting threshold which forces convergence to zero.

   theorem exists_superlinear_decay_threshold {C b ε : ℝ}
       (hC : 0 < C) (hb : 0 < b) (hε : 0 < ε) :
       ∃ A : ℝ, 0 < A ∧ ∀ Y : ℕ → ℝ,
         (∀ i, 0 ≤ Y i) → Y 0 ≤ A →
         (∀ i, Y (i+1) ≤ C*b^i*(Y i)^(1+ε)) → Tendsto Y atTop (𝓝 0) := by
   …