proposition: Lemma dvg_harmonic (R : numFieldType) : ~ cvgn (series (@harmonic R)).
proof: Proof. have ge_half n : (0 < n)%N -> 2^-1 <= \sum_(n <= i < n.*2) harmonic i. case: n => // n _. rewrite (@le_trans _ _ (\sum_(n.+1 <= i < n.+1.*2) n.+1.*2%:R^-1)) //=. rewrite sumr_const_nat -addnn addnK addnn -mul2n natrM invfM. by rewrite -[_ *+ n.+1]mulr_natr divfK. by apply: ler_sum_nat => i /andP[? ?]; rewrite lef_pV2 ?qualifE/= ?ler_nat. move/cvg_cauchy/cauchy_ballP => /(_ _ [gt0 of 2^-1 : R]); rewrite !near_map2. rewrite -ball_normE => /nearP_dep hcvg; near \oo => n; near \oo => m. have: `|series harmonic n - series harmonic m| < 2^-1 :> R by near: m; near: n. rewrite le_gtF// distrC -[X in X - _](addrNK (series harmonic n.*2)). rewrite sub_series_geq; last by near: m; apply: nbhs_infty_ge. rewrite -addrA sub_series_geq -addnn ?leq_addr// addnn. have sh_ge0 i j : 0 <= \sum_(i <= k < j) harmonic k :> R. by rewrite ?sumr_ge0//; move=> k _; apply: harmonic_ge0. by rewrite ger0_norm// ler_wpDl// ge_half//; near: n. 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