proposition: Lemma is_derive_filterdiff (f : R -> R -> R) (x y : R) (dfx : R -> R -> R) (dfy : R) : locally (x,y) (fun u : R * R => is_derive (fun z => f z (snd u)) (fst u) (dfx (fst u) (snd u))) -> is_derive (fun z : R => f x z) y dfy -> continuous (fun u : R * R => dfx (fst u) (snd u)) (x,y) -> filterdiff (fun u : R * R => f (fst u) (snd u)) (locally (x,y)) (fun u : R * R => plus (scal (fst u) (dfx x y)) (scal (snd u) dfy)).
proof: Proof. intros Dx Dy Cx. split. apply (is_linear_comp (fun u : R * R => (scal (fst u) (dfx x y),scal (snd u) dfy)) (fun u : R * R => plus (fst u) (snd u))). apply is_linear_prod. apply (is_linear_comp (@fst _ _) (fun t : R => scal t (dfx x y))). by apply is_linear_fst. by apply @is_linear_scal_l. apply (is_linear_comp (@snd _ _) (fun t : R => scal t dfy)). by apply is_linear_snd. by apply @is_linear_scal_l. by apply @is_linear_plus. simpl => u Hu. replace u with (x,y) by now apply is_filter_lim_locally_unique. move => {u Hu} eps /=. set (eps' := pos_div_2 eps). generalize (proj1 (filterlim_locally _ _) Cx eps') => {Cx} /= Cx. generalize (filter_and _ _ Dx Cx) => {Dx Cx}. intros (d1,Hd1). destruct (proj2 Dy y (fun P H => H) eps') as (d2,Hd2). set (l1 := dfx x y). exists (mkposreal _ (Rmin_stable_in_posreal d1 d2)). intros (u,v) (Hu,Hv) ; simpl in *. set (g1 t := minus (f t v) (scal t l1)). set (g2 t := minus (f x t) (scal t dfy)). apply Rle_trans with (norm (minus (g1 u) (g1 x)) + norm (minus (g2 v) (g2 y))). eapply Rle_trans, norm_triangle. apply Req_le, f_equal, sym_eq. rewrite /g1 /g2 /minus !opp_plus !opp_opp -!plus_assoc ; apply f_equal. do 5 rewrite plus_comm -!plus_assoc ; apply f_equal. rewrite !scal_distr_r !opp_plus -!plus_assoc !scal_opp_l !opp_opp. rewrite plus_comm -!plus_assoc ; apply f_equal. rewrite plus_comm -!plus_assoc ; apply f_equal. by rewrite plus_comm -!plus_assoc plus_opp_l plus_zero_r. replace (pos eps) with (eps' + eps') by (apply sym_eq ; apply double_var). rewrite Rmult_plus_distr_r. apply Rplus_le_compat. apply Rle_trans with (eps' * norm (minus u x)). apply bounded_variation with (fun t => minus (dfx t v) l1) => t Ht. split. apply: is_derive_minus. apply (Hd1 (t,v)) ; split ; simpl. apply Rle_lt_trans with (1 := Ht). apply Rlt_le_trans with (1:=Hu). apply Rmin_l. apply Rlt_le_trans with (1:=Hv). apply Rmin_l. rewrite -{2}(Rmult_1_r l1). evar_last. apply filterdiff_linear, is_linear_scal_l. by rewrite Rmult_1_r. apply Rlt_le. apply (Hd1 (t,v)) ; split ; simpl. apply Rle_lt_trans with (1 := Ht). apply Rlt_le_trans with (1:=Hu). apply Rmin_l. apply Rlt_le_trans with (1:=Hv). apply Rmin_l. apply Rmult_le_compat_l. apply Rlt_le. apply cond_pos. apply (norm_le_prod_norm_1 (minus (u, v) (x, y))). apply Rle_trans with (eps' * norm (minus v y)). apply Rle_trans with (norm (minus (minus (f x v) (f x y)) (scal (minus v y) dfy))). right; apply f_equal. rewrite /g2 scal_minus_distr_r /minus !opp_plus opp_opp -!plus_assoc ; apply f_equal. rewrite plus_comm -!plus_assoc ; apply f_equal. apply plus_comm. apply Hd2. apply Rlt_le_trans with (1:=Hv). apply Rmin_r. apply Rmult_le_compat_l. apply Rlt_le. apply cond_pos. apply (norm_le_prod_norm_2 (minus (u, v) (x, y))). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lim_seq Iter Hierarchy Continuity Equiv