runningMax

formal source

  30/-! ## Running Maximum of a Sequence -/
  31
  32/-- The running maximum of a sequence: M̃(n) = max_{k ≤ n} a(k). -/
  33noncomputable def runningMax (a : ℕ → ℝ) : ℕ → ℝ :=
  34  fun n => Finset.sup' (Finset.range (n + 1))
  35    (Finset.nonempty_range_add_one) a
  36
  37/-- The running maximum is always ≥ the current value. -/
  38theorem runningMax_ge (a : ℕ → ℝ) (n : ℕ) :
  39    a n ≤ runningMax a n := by
  40  unfold runningMax
  41  apply Finset.le_sup'
  42  simp
  43
  44/-- The running maximum is monotone non-decreasing. -/
  45theorem runningMax_mono (a : ℕ → ℝ) : Monotone (runningMax a) := by
  46  intro m n hmn
  47  unfold runningMax
  48  apply Finset.sup'_le
  49  intro k hk
  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 :=