De Giorgi preiter vanishing

theorem deGiorgi_preiter_vanishing    {Aseq : ℕ → ℝ} {d : ℕ}    (hd : 2 < (d : ℝ))    {K lamStar : ℝ} (hK : 0 < K) (hLamStar : 0 < lamStar)    (hA_nonneg : ∀ n, 0 ≤ Aseq n)    (hpre :      ∀ n,        Aseq (n + 1) ≤          K / ((deGiorgiRadius n - deGiorgiRadius (n + 1)) ^ 2 *            (deGiorgiLevel lamStar (n + 1) - deGiorgiLevel lamStar n) ^ (4 / (d : ℝ))) *          Aseq n ^ (1 + 2 / (d : ℝ)))    (hsmall :      Aseq 0 ≤        (deGiorgiRecurrenceCoeff d K lamStar) ^ (-(1 : ℝ) / (2 / (d : ℝ))) *          (deGiorgiRecurrenceBase d) ^ (-(1 : ℝ) / (2 / (d : ℝ)) ^ 2)) :    Tendsto Aseq atTop (nhds 0) := by  have hα : 0 < 2 / (d : ℝ) := by positivity  have hB : 1 < deGiorgiRecurrenceBase d := by    dsimp [deGiorgiRecurrenceBase]    exact (Real.one_lt_rpow_iff_of_pos (by positivity)).2 (Or.inl ⟨by norm_num, by positivity⟩)  have hC : 0 < deGiorgiRecurrenceCoeff d K lamStar := by    dsimp [deGiorgiRecurrenceCoeff]    positivity  have hrec :      ∀ n,        Aseq (n + 1) ≤          deGiorgiRecurrenceCoeff d K lamStar *            deGiorgiRecurrenceBase d ^ n *            Aseq n ^ (1 + 2 / (d : ℝ)) :=    deGiorgi_preiter_to_recurrence hLamStar hpre  rw [Metric.tendsto_atTop]  intro ε hε  obtain ⟨N, hN⟩ :=    deGiorgi_recurrence_closeout hC hB hα hA_nonneg hrec hsmall ε hε  exact ⟨N, fun n hn => by    rw [Real.dist_eq, sub_zero, abs_of_nonneg (hA_nonneg n)]    exact hN n hn⟩