normalized_eq_one_at_max

formal source

  77  exact (div_le_one (runningMax_pos a n h)).mpr (runningMax_ge a n)
  78
  79/-- The normalized sequence achieves 1 at the running-max index. -/
  80theorem normalized_eq_one_at_max (a : ℕ → ℝ) (n : ℕ)
  81    (hmax : a n = runningMax a n) (hpos : 0 < a n) :
  82    normalized a n = 1 := by
  83  unfold normalized
  84  rw [hmax]
  85  exact div_self (ne_of_gt (runningMax_pos a n hpos))
  86
  87/-! ## Rescaled Coordinates -/
  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