proposition: Lemma is_linear_prod {K : AbsRing} {T U V : NormedModule K} (l1 : T -> U) (l2 : T -> V) : is_linear l1 -> is_linear l2 -> is_linear (fun t : T => (l1 t, l2 t)).
proof: Proof. intros H1 H2. split. - intros x y. apply injective_projections ; simpl. by apply H1. by apply H2. - intros k x. apply injective_projections ; simpl. by apply H1. by apply H2. - destruct (linear_norm l1 H1) as [M1 [HM1 Hn1]]. destruct (linear_norm l2 H2) as [M2 [HM2 Hn2]]. exists (sqrt 2 * Rmax M1 M2)%R ; split. apply Rmult_lt_0_compat. apply sqrt_lt_R0, Rlt_0_2. by apply Rmax_case. intros x. eapply Rle_trans. apply norm_prod. rewrite Rmult_assoc. apply Rmult_le_compat_l. by apply sqrt_pos. rewrite Rmult_max_distr_r. apply Rmax_case. by eapply Rle_trans, Rmax_l. by eapply Rle_trans, Rmax_r. by apply norm_ge_0. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv