proposition: Lemma filterdiff_scal : forall {F : (K * V -> Prop) -> Prop} {FF : ProperFilter F} (x : K * V), is_filter_lim F x -> (forall (n m : K), mult n m = mult m n) -> filterdiff (fun t : K * V => scal (fst t) (snd t)) F (fun t => plus (scal (fst t) (snd x)) (scal (fst x) (snd t))).
proof: Proof. move => F FF [x1 x2] Hx Hcomm ; split. - apply (is_linear_comp (fun t : K * V => (scal (fst t) x2,scal x1 (snd t))) (fun t : V * V => plus (fst t) (snd t))). apply is_linear_prod. apply (is_linear_comp (fun t : K * V => fst t) (fun k : K => scal k x2)). by apply is_linear_fst. by apply is_linear_scal_l. apply is_linear_comp. by apply is_linear_snd. by apply is_linear_scal_r. apply is_linear_plus. - move => y Hy eps. replace y with (x1,x2). 2: now apply is_filter_lim_unique with (1 := Hx). clear y Hy. apply Hx ; clear Hx. apply: locally_le_locally_norm. exists eps. intros [y1 y2] H. simpl. set v := minus (minus _ _) _. replace v with (scal (minus y1 x1) (minus y2 x2)). apply Rle_trans with (1 := norm_scal _ _). generalize (proj1 (sqrt_plus_sqr (abs (minus y1 x1)) (norm (minus y2 x2)))). rewrite -> Rabs_pos_eq by apply abs_ge_0. rewrite -> Rabs_pos_eq by apply norm_ge_0. intros H'. apply Rmult_le_compat. apply abs_ge_0. apply norm_ge_0. apply Rlt_le, Rle_lt_trans with (2 := H). apply Rle_trans with (2 := H'). apply Rmax_l. apply Rle_trans with (2 := H'). apply Rmax_r. rewrite /v /minus !scal_distr_l !scal_distr_r !opp_plus !scal_opp_r !scal_opp_l !opp_opp -!plus_assoc. apply f_equal. plus_grab (opp (scal x1 y2)). apply f_equal. plus_grab (opp (scal y1 x2)). apply f_equal. by rewrite plus_assoc plus_opp_l plus_zero_l. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv