proposition: Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|.
proof: Proof. move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. have [|xn0] := real_le0P (normr_real x). by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0. set k := 2 / e%:num * (PosNum xn0)%:num. have kn0 : k != 0 by rewrite /k. have abskgt0 : `|k| > 0 by rewrite normr_gt0. rewrite -[x in leLHS](scalerKV kn0) linearZZ normrZ -ler_pdivlMl //. suff /he : ball 0 e%:num (k^-1 *: x). rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply. by rewrite ger0_norm /k // mulVf. rewrite -ball_normE /= distrC subr0 normrZ. rewrite normfV ger0_norm /k // invrM ?unitfE // mulrAC mulVf //. by rewrite invf_div mul1r [ltRHS]splitr; apply: ltr_pwDr. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum matrix interval) mathcomp(mathcomp_extra boolp classical_sets functions) reals signed topology prodnormedzmodule normedtype landau forms