rescaleLength

formal source

  88
  89/-- The rescaling factor λₙ = 1 / √(runningMax a n).
  90    Used to rescale space: x ↦ x/λₙ, t ↦ t/λₙ². -/
  91noncomputable def rescaleLength (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  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]