proposition: Lemma cesaro_converse (u_ : R ^nat) (l : R) : telescope u_ =o_\oo @harmonic R -> arithmetic_mean u_ @ \oo --> l -> u_ @ \oo --> l.
proof: Proof. pose a_ := telescope u_ => a_o u_l. suff abel : forall n, u_ n - arithmetic_mean u_ n = \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1. suff K : u_ - arithmetic_mean u_ @ \oo --> (0 : R). rewrite -(add0r l). rewrite (_ : u_ = u_ - arithmetic_mean u_ + arithmetic_mean u_); last first. by rewrite funeqE => n; rewrite subrK. exact: cvgD. rewrite (_ : _ - arithmetic_mean u_ = (fun n => \sum_(1 <= k < n.+1) k%:R / n.+1%:R * a_ k.-1)); last first. by rewrite funeqE. rewrite {abel} /= (_ : (fun _ => _) = fun n => n.+1%:R^-1 * \sum_(0 <= k < n) k.+1%:R * a_ k); last first. rewrite funeqE => n; rewrite big_add1 /= /= big_distrr /=. by apply eq_bigr => i _; rewrite mulrCA mulrA. have {}a_o : [sequence n.+1%:R * telescope u_ n]_n @ \oo --> (0 : R). apply: (@eqolim0 _ _ _ eventually_filterType). rewrite a_o. set h := 'o_\oo (@harmonic R). apply/eqoP => _/posnumP[e] /=. near=> n; rewrite normr1 mulr1 normrM -ler_pdivlMl// ?normr_gt0//. rewrite mulrC -normrV ?unitfE //. near: n. by case: (eqoP eventually_filterType (@harmonic R) h) => Hh _; apply Hh. move: (cesaro a_o); rewrite /arithmetic_mean /series /= -/a_. exact: (@cesaro_converse_off_by_one (fun k => k.+1%:R * a_ k)). case => [|n]. rewrite /arithmetic_mean/= invr1 mul1r !seriesEnat/=. by rewrite big_nat1 subrr big_geq. rewrite /arithmetic_mean /= seriesEnat /= big_nat_recl //=. under eq_bigr do rewrite eq_sum_telescope. rewrite big_split /= big_const_nat iter_addr addr0 addrA -mulrS mulrDr. rewrite -(mulr_natl (u_ O)) mulrA mulVr ?unitfE ?pnatr_eq0 // mul1r opprD addrA. rewrite eq_sum_telescope (addrC (u_ O)) addrK. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) \sum_(0 <= k < n.+1 | (k < i.+1)%N) a_ k); last first. rewrite !big_mkord; apply: eq_bigr => i _. by rewrite seriesEord/= big_mkord -big_ord_widen. rewrite (exchange_big_dep_nat xpredT) //=. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) \sum_(i <= j < n.+1) a_ i ); last first. apply: congr_big_nat => //= i ni. rewrite big_const_nat iter_addr addr0 -big_filter. rewrite big_const_seq iter_addr addr0; congr (_ *+ _). rewrite /index_iota subn0 -[in LHS](subnKC (ltnW ni)) iotaD filter_cat. rewrite count_cat (_ : [seq _ <- _ | _] = [::]); last first. rewrite -(filter_pred0 (iota 0 i)); apply: eq_in_filter => j. by rewrite mem_iota leq0n andTb add0n => ji; rewrite ltnNge ji. rewrite 2!add0n (_ : [seq _ <- _ | _] = iota i (n.+1 - i)); last first. rewrite -[RHS]filter_predT; apply: eq_in_filter => j. rewrite mem_iota => /andP[ij]; rewrite subnKC; last exact/ltnW. by move=> jn; rewrite ltnS ij. by rewrite count_predT size_iota. rewrite [X in _ - _ * X](_ : _ = \sum_(0 <= i < n.+1) a_ i * (n.+1 - i)%:R); last first. by apply: eq_bigr => i _; rewrite big_const_nat iter_addr addr0 mulr_natr. rewrite big_distrr /= big_mkord (big_morph _ (@opprD _) (@oppr0 _)). rewrite seriesEord -big_split /= big_add1 /= big_mkord; apply: eq_bigr => i _. rewrite mulrCA -[X in X - _]mulr1 -mulrBr [RHS]mulrC; congr (_ * _). rewrite -[X in X - _](@divrr _ (n.+2)%:R) ?unitfE ?pnatr_eq0 //. rewrite [in X in _ - X]mulrC -mulrBl; congr (_ / _). rewrite -natrB; last by rewrite (@leq_trans n.+1) // leq_subr. rewrite subnBA; by [rewrite addSnnS addnC addnK | rewrite 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