proposition: Lemma is_linear_comp {K : AbsRing} {U V W : NormedModule K} (l1 : U -> V) (l2 : V -> W) : is_linear l1 -> is_linear l2 -> is_linear (fun x => l2 (l1 x)).
proof: Proof. intros Hl1 Hl2. split. - move => x y. by rewrite !linear_plus. - move => k x. by rewrite !linear_scal. - destruct (linear_norm _ Hl1) as [M1 Hn1]. destruct (linear_norm _ Hl2) as [M2 Hn2]. exists (M2 * M1) ; split. now apply Rmult_lt_0_compat. move => x. eapply Rle_trans. by apply Hn2. rewrite Rmult_assoc. apply Rmult_le_compat_l. now apply Rlt_le. apply Hn1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv