proposition: Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n : series (fun k => r / (2 ^ (k + n.+1))%:R : R^o) @ \oo --> (r / 2 ^+ n : R^o).
proof: Proof. rewrite (_ : series _ = series (geometric (r / (2 ^ n.+1)%:R) 2^-1%R)); last first. rewrite funeqE => m; rewrite /series /=; apply: eq_bigr => k _. by rewrite expnD natrM (mulrC (2 ^ k)%:R) invfM exprVn (natrX _ 2 k) mulrA. apply: cvg_trans. apply: cvg_geometric_series. by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE. rewrite [X in (X - _)%R](splitr 1) div1r addrK. by rewrite -mulrA -invfM expnSr natrM -mulrA divff// mulr1 natrX. 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