proposition: Theorem cesaro (u_ : R ^nat) (l : R) : u_ @ \oo --> l -> arithmetic_mean u_ @ \oo --> l.
proof: Proof. move=> u0_cvg; have ssplit v_ m n : (m <= n)%N -> `|n%:R^-1 * series v_ n| <= n%:R^-1 * `|series v_ m| + n%:R^-1 * `|\sum_(m <= i < n) v_ i|. move=> /subnK<-; rewrite series_addn mulrDr (le_trans (ler_normD _ _))//. by rewrite !normrM ger0_norm. apply/cvgrPdist_lt=> _/posnumP[e]; near \oo => m; near=> n. have {}/ssplit -/(_ _ [sequence l - u_ n]_n) : (m.+1 <= n.+1)%nat. by near: n; exists m. rewrite !seriesEnat /= big_split/=. rewrite sumrN mulrBr sumr_const_nat -(mulr_natl l) mulKf//. move=> /le_lt_trans->//; rewrite [e%:num]splitr ltrD//. have [->|neq0] := eqVneq (\sum_(0 <= k < m.+1) (l - u_ k)) 0. by rewrite normr0 mulr0. rewrite -ltr_pdivlMr ?normr_gt0//. rewrite -ltf_pV2 ?qualifE//= ?mulr_gt0 ?invr_gt0 ?normr_gt0// invrK. rewrite (lt_le_trans (archi_boundP _))// ler_nat leqW//. by near: n; apply: nbhs_infty_ge. rewrite ltr_pdivrMl ?ltr0n // (le_lt_trans (ler_norm_sum _ _ _)) //. rewrite (le_lt_trans (@ler_sum_nat _ _ _ _ (fun i => e%:num / 2) _))//; last first. by rewrite sumr_const_nat mulr_natl ltr_pMn2l// ltn_subrL. move=> i /andP[mi _]; move: i mi; near: m. have : \forall x \near \oo, `|l - u_ x| < e%:num / 2. by move/cvgrPdist_lt : u0_cvg; apply. move=> -[N _ Nu]; exists N => // k Nk i ki. by rewrite ltW// Nu//= (leq_trans Nk)// ltnW. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(set_interval) reals ereal signed topology normedtype landau