proposition: Lemma cvg_to_0_linear (R : realFieldType) (f : R -> R) K (k : R) : 0 < k -> (forall r, 0 < `| r | < k -> `|f r| <= K * `| r |) -> f x @[x --> 0^'] --> 0.
proof: Proof. move=> k0 kfK; have [K0|K0] := lerP K 0. - apply/cvgrPdist_lt => _/posnumP[e]; near=> x. rewrite distrC subr0 (le_lt_trans (kfK _ _)) //; last first. by rewrite (@le_lt_trans _ _ 0)// mulr_le0_ge0. near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt. - apply/(@eqolim0 _ _ R (0^'))/eqoP => _/posnumP[e]; near=> x. rewrite (le_trans (kfK _ _)) //=. + near: x; exists (k / 2); first by rewrite /mkset divr_gt0. move=> t /=; rewrite distrC subr0 => tk2 t0. by rewrite normr_gt0 t0 (lt_trans tk2) // -[in ltLHS](add0r k) midf_lt. + rewrite normr1 mulr1 mulrC -ler_pdivlMr //. near: x; exists (e%:num / K); first by rewrite /mkset divr_gt0. by move=> t /=; rewrite distrC subr0 => /ltW. 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