proposition: Lemma filterdiff_comp {F} {FF : Filter F} f g (lf : U -> V) (lg : V -> W) : filterdiff f F lf -> filterdiff g (filtermap f F) lg -> filterdiff (fun y => g (f y)) F (fun y => lg (lf y)).
proof: Proof. intros Df Dg. split. apply is_linear_comp. by apply Df. by apply Dg. intros x Hx. assert (Cf : filterlim f F (locally (f x))). apply filterdiff_continuous_aux with (2 := Hx). eexists ; by apply Df. assert (is_domin (filtermap f F) (fun y : V => minus y (f x)) (fun y : V => minus (minus (g y) (g (f x))) (lg (minus y (f x))))). apply Dg. move => P HP. by apply Cf. destruct Dg as [Hg _]. rename H into Dg. destruct Df as [Hf Df]. apply domin_rw_r with (fun y : U => plus (minus (minus (g (f y)) (g (f x))) (lg (minus (f y) (f x)))) (lg (minus (minus (f y) (f x)) (lf (minus y x))))). apply equiv_ext_loc. apply filter_forall => y. rewrite /minus -!plus_assoc. repeat apply f_equal. rewrite plus_assoc. rewrite (linear_plus _ Hg (plus _ _)). rewrite plus_assoc. rewrite plus_opp_l plus_zero_l. by apply linear_opp. apply domin_plus. intros eps. destruct (linear_norm _ Hf) as [mf [Hmf Hnf]]. assert (F (fun y => norm (minus (f y) (f x)) <= (1 + mf) * norm (minus y x))). specialize (Df x Hx (mkposreal _ Rlt_0_1)). move: Df ; apply filter_imp. move => y /= Hy. replace (minus (f y) (f x)) with (plus (minus (minus (f y) (f x)) (lf (minus y x))) (lf (minus y x))). eapply Rle_trans. apply @norm_triangle. rewrite Rmult_plus_distr_r. apply Rplus_le_compat. exact Hy. by apply Hnf. by rewrite {1}/minus -plus_assoc plus_opp_l plus_zero_r. clear Df ; rename H into Df. assert (He : 0 < eps / (1 + mf)). apply Rdiv_lt_0_compat. apply cond_pos. apply Rplus_lt_0_compat. exact Rlt_0_1. exact Hmf. specialize (Dg (mkposreal _ He)). unfold filtermap in Dg. generalize (filter_and _ _ Df Dg). apply filter_imp => /= y {Df Dg} [Df Dg]. apply Rle_trans with (1 := Dg). unfold Rdiv. rewrite Rmult_assoc. apply Rmult_le_compat_l. apply Rlt_le, eps. rewrite Rmult_comm ; apply Rle_div_l. apply Rplus_lt_0_compat. exact Rlt_0_1. exact Hmf. rewrite Rmult_comm ; by apply Df. specialize (Df x Hx). by apply is_domin_linear. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv