rescaleLength_pos

formal source

  92  1 / Real.sqrt (runningMax a n)
  93
  94/-- The rescaling factor is positive. -/
  95theorem rescaleLength_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  96    0 < rescaleLength a n := by
  97  unfold rescaleLength
  98  apply div_pos one_pos
  99  exact Real.sqrt_pos.mpr (runningMax_pos a n h)
 100
 101/-- The rescaling factor tends to 0 as the running max diverges. -/
 102theorem rescaleLength_tendsto_zero (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
 103    Tendsto (rescaleLength a) atTop (nhds 0) := by
 104  -- Strategy: for any ε > 0, get N so that runningMax a n > (1/ε)², then
 105  -- sqrt(runningMax a n) > 1/ε, hence 1/sqrt(runningMax a n) < ε.
 106  have h_max := runningMax_tendsto_atTop a h
 107  rw [Metric.tendsto_nhds]
 108  intro ε hε
 109  have hie_pos : (0 : ℝ) < 1 / ε := by positivity
 110  rw [Filter.tendsto_atTop_atTop] at h_max
 111  obtain ⟨N, hN⟩ := h_max ((1 / ε) ^ 2 + 1)
 112  rw [Filter.eventually_atTop]
 113  refine ⟨N, fun n hn => ?_⟩
 114  have hrun : (1 / ε) ^ 2 + 1 ≤ runningMax a n := hN n hn
 115  have hrun_pos : (0 : ℝ) < runningMax a n := by linarith [sq_nonneg (1 / ε)]
 116  have hsqrt_pos : (0 : ℝ) < Real.sqrt (runningMax a n) := Real.sqrt_pos.mpr hrun_pos
 117  simp only [rescaleLength, Real.dist_eq, sub_zero,
 118    abs_of_pos (div_pos one_pos hsqrt_pos)]
 119  rw [div_lt_iff₀ hsqrt_pos]
 120  have h_sqrt_bound : 1 / ε < Real.sqrt (runningMax a n) := by
 121    rw [← Real.sqrt_sq hie_pos.le]
 122    exact Real.sqrt_lt_sqrt (sq_nonneg _) (by linarith)
 123  calc (1 : ℝ) = ε * (1 / ε) := by field_simp
 124    _ < ε * Real.sqrt (runningMax a n) := by
 125        exact mul_lt_mul_of_pos_left h_sqrt_bound hε