proposition: Lemma littleo_linear0 (V W : normedModType R) (f : {linear V -> W}) : (f : V -> W) =o_ (0 : V) id -> f = cst 0 :> (V -> W).
proof: Proof. move/eqoP => oid. rewrite funeqE => x; apply/eqP; have [|xn0] := real_le0P (normr_real x). by rewrite normr_le0 => /eqP ->; rewrite linear0. rewrite -normr_le0 -(mul0r `|x|) -ler_pdivrMr //. apply/ler_gtP => _ /posnumP[e]; rewrite ler_pdivrMr //. have /oid /nbhs_ballP [_ /posnumP[d] dfe] := !! gt0 e. set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1. rewrite -{1}(@scalerKV _ _ k _ x) /k // linearZZ normrZ. rewrite -ler_pdivlMl; last by rewrite gtr0_norm. rewrite mulrCA (@le_trans _ _ (e%:num * `|k^-1 *: x|)) //; last first. by rewrite ler_pM // normrZ normfV. apply: dfe; rewrite -ball_normE /= sub0r normrN normrZ. rewrite invrK -ltr_pdivlMr // ger0_norm // ltr_pdivrMr //. by rewrite -mulrA mulVf ?lt0r_neq0 // mulr1 [ltRHS]splitr ltrDl. 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