runningMax_tendsto_atTop

formal source

  50  exact Finset.le_sup' a (Finset.range_mono (by omega) hk)
  51
  52/-- The running maximum of a divergent sequence is divergent. -/
  53theorem runningMax_tendsto_atTop (a : ℕ → ℝ) (h : Tendsto a atTop atTop) :
  54    Tendsto (runningMax a) atTop atTop := by
  55  rw [Filter.tendsto_atTop_atTop]
  56  intro b
  57  rw [Filter.tendsto_atTop_atTop] at h
  58  obtain ⟨N, hN⟩ := h b
  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