OAI/Combinatorics/InfiniteMatroid/Cesaro.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.InfiniteMatroidCounterexample.weighted_mean_zero line 12

   Source documentation

   An elementary weighted Cesàro estimate.

   lemma weighted_mean_zero (w d : ℕ → ℝ) (hw : ∀ n, 0 ≤ w n)
       (hc : Tendsto (fun n ↦ ∑ m ∈ range n, w m) atTop atTop)
       (hd : Tendsto d atTop (𝓝 0)) :
       Tendsto (fun n ↦ (∑ m ∈ range n, w m * d m) / (∑ m ∈ range n, w m)) atTop (𝓝 0) := by
   …

2. lemma OAI.InfiniteMatroidCounterexample.tail_absSup_zero line 62

   Source documentation

   A tail supremum of absolute values of a null sequence is again null.

   lemma tail_absSup_zero (d : ℕ → ℝ) (hb : BddAbove (Set.range (fun n ↦ |d n|)))
       (hd : Tendsto d atTop (𝓝 0)) :
       Tendsto (fun n ↦ sSup ((fun m ↦ |d m|) '' Set.Ici n)) atTop (𝓝 0) := by
   …