proposition: Lemma contraction_dist n m : `|y n - y (n + m)| <= C * q%:num ^+ n.
proof: Proof. have f1 k : `|y k.+1 - y k| <= q%:num ^+ k * `|f base - base|. elim: k => [|k /(ler_wpM2l (ge0 q))]; first by rewrite expr0 mul1r. rewrite mulrA -exprS; apply: le_trans. by rewrite (@ctrfq (y k.+1, y k)); split; exact: funS. have /le_trans -> // : `| y n - y (n + m)| <= series (geometric (`|f base - base| * q%:num ^+ n) q%:num) m. elim: m => [|m ih]. by rewrite geometric_seriesE ?lt_eqF//= addn0 subrr normr0 subrr mulr0 mul0r. rewrite (le_trans (ler_distD (y (n + m)%N) _ _))//. apply: (le_trans (lerD ih _)); first by rewrite distrC addnS; exact: f1. rewrite [_ * `|_|]mulrC exprD mulrA geometric_seriesE ?lt_eqF//=. rewrite -!/(`1-_) (onem_PosNum ctrf.1) (onemX_NngNum (ltW ctrf.1)). rewrite -!mulrA -mulrDr ler_pM// -mulrDr exprSr onemM -addrA. rewrite -[in leRHS](mulrC _ `1-(_ ^+ m)) -onemMr onemK. by rewrite [in leRHS]mulrDl mulrAC mulrV ?mul1r// unitf_gt0// onem_gt0. rewrite geometric_seriesE ?lt_eqF//= -[leRHS]mulr1 (ACl (1*4*2*3))/= -/C. by rewrite ler_wpM2l// 1?mulr_ge0// lerBlDr lerDl. 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