proposition: Lemma filterdiff_differentiable_pt_lim (f : R -> R -> R) (x y lx ly : R) : filterdiff (fun u : R * R => f (fst u) (snd u)) (locally (x,y)) (fun u : R * R => fst u * lx + snd u * ly) <-> differentiable_pt_lim f x y lx ly.
proof: Proof. split => Df. move => eps. case: Df => _ Df. assert (is_filter_lim (locally (x, y)) (x, y)) by now intro. specialize (Df (x,y) H) => {H}. apply locally_2d_locally. assert (0 < eps / sqrt 2). apply Rdiv_lt_0_compat. by apply eps. by apply Rlt_sqrt2_0. move: (Df (mkposreal _ H)). apply filter_imp => [[u v] /= Huv]. rewrite !(Rmult_comm _ (_-_)). eapply Rle_trans. apply Huv. rewrite Rmult_assoc. apply Rmult_le_compat_l. by apply Rlt_le, eps. rewrite Rmult_comm Rle_div_l. rewrite Rmult_comm. eapply Rle_trans. apply norm_prod. apply Rle_refl. by apply Rlt_sqrt2_0. split. apply (is_linear_comp (fun u : R * R => (scal (fst u) lx,scal (snd u) ly)) (fun u : R * R => plus (fst u) (snd u))). apply is_linear_prod. apply (is_linear_comp (@fst _ _) (fun t : R => scal t lx)). by apply is_linear_fst. by apply @is_linear_scal_l. apply (is_linear_comp (@snd _ _) (fun t : R => scal t ly)). 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 /=. move: (proj1 (locally_2d_locally _ _ _) (Df eps)). apply filter_imp => [[u v]] /= Huv. rewrite !(Rmult_comm (_-_)). eapply Rle_trans. apply Huv. apply Rmult_le_compat_l. by apply Rlt_le, eps. apply (norm_prod (u - x) (v - y)). Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive