proposition: Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e (P : pred nat) : (forall n, 0 <= A n) -> (0 <= e)%R -> \sum_(i <oo | P i) (A i + (e / (2 ^ i.+1)%:R)%:E) <= \sum_(i <oo | P i) A i + e%:E.
proof: Proof. move=> A0 /nonnegP[{}e]. rewrite (@le_trans _ _ (lim ((fun n => (\sum_(0 <= i < n | P i) A i) + \sum_(0 <= i < n) (e%:num / (2 ^ i.+1)%:R)%:E) @ \oo))) //. rewrite nneseriesD // limeD //. - rewrite leeD2l //; apply: lee_lim => //. + exact: is_cvg_nneseries. + exact: is_cvg_nneseries. + by near=> n; exact: lee_sum_nneg_subset. - exact: is_cvg_nneseries. - exact: is_cvg_nneseries. - exact: adde_def_nneseries. suff cvggeo : (fun n => \sum_(0 <= i < n) (e%:num / (2 ^ i.+1)%:R)%:E) @ \oo --> e%:num%:E. rewrite limeD //. - by rewrite leeD2l // (cvg_lim _ cvggeo). - exact: is_cvg_nneseries. - by apply: is_cvg_nneseries => ?; rewrite lee_fin divr_ge0. - by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_defl. rewrite (_ : (fun n => _) = EFin \o (fun n => \sum_(0 <= i < n) (e%:num / (2 ^ (i + 1))%:R))%R); last first. rewrite funeqE => n /=; rewrite (@big_morph _ _ EFin 0 adde)//. by under [in RHS]eq_bigr do rewrite addn1. apply: cvg_comp; last by apply cvg_refl. have := cvg_geometric_series_half e%:num O. by rewrite expr0 divr1; apply: cvg_trans. Unshelve. all: by end_near. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)