runningMax_pos

formal source

  59  exact ⟨N, fun n hn => le_trans (hN N le_rfl) (le_trans (runningMax_ge a N) (runningMax_mono a hn))⟩
  60
  61/-- The running maximum is positive if any element is positive. -/
  62theorem runningMax_pos (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  63    0 < runningMax a n :=
  64  lt_of_lt_of_le h (runningMax_ge a n)
  65
  66/-! ## Normalization -/
  67
  68/-- The normalized sequence: ã(n) = a(n) / runningMax(a)(n).
  69    By construction, |ã(n)| ≤ 1 for all n. -/
  70noncomputable def normalized (a : ℕ → ℝ) (n : ℕ) : ℝ :=
  71  a n / runningMax a n
  72
  73/-- The normalized sequence is bounded by 1 in absolute value. -/
  74theorem normalized_le_one (a : ℕ → ℝ) (n : ℕ) (h : 0 < a n) :
  75    normalized a n ≤ 1 := by
  76  unfold normalized
  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)