proposition: Lemma Schwarz : forall (f : R -> R -> R) x y, locally_2d (fun u v => ex_derive (fun z : R => f z v) u /\ ex_derive (fun z : R => f u z) v /\ ex_derive (fun z : R => Derive (fun t => f z t) v) u /\ ex_derive (fun z : R => Derive (fun t => f t z) u) v) x y -> continuity_2d_pt (fun u v => Derive (fun z => Derive (fun t => f z t) v) u) x y -> continuity_2d_pt (fun u v => Derive (fun z => Derive (fun t => f t z) u) v) x y -> Derive (fun z => Derive (fun t => f z t) y) x = Derive (fun z => Derive (fun t => f t z) x) y.
proof: Proof. intros f x y (eps, HD) HC2 HC1. refine ((fun H1 => _) (Schwarz_aux f x y eps _)). 2: intros u v Hu Hv ; split ; now apply (HD u v). refine ((fun H2 => _ )(Schwarz_aux (fun x y => f y x) y x eps _)). 2: intros u v Hu Hv ; split ; now apply (HD v u). simpl in H1, H2. apply Req_lt_aux. intros e. destruct (HC1 (pos_div_2 e)) as (d1,Hc1). destruct (HC2 (pos_div_2 e)) as (d2,Hc2). set (d := Rmin (Rmin (pos_div_2 d1) (pos_div_2 d2)) (pos_div_2 eps)). assert (Hd: d > 0). apply Rmin_glb_lt. apply Rmin_stable_in_posreal. apply cond_pos. assert (K: Rabs d < eps). rewrite Rabs_right. apply Rle_lt_trans with (1 := Rmin_r _ _). apply (Rlt_eps2_eps eps). apply cond_pos. now apply Rgt_ge. specialize (H1 d d K K). specialize (H2 d d K K). destruct H1 as (u1&v1&Hu1&Hv1&H1). destruct H2 as (v2&u2&Hv2&Hu2&H2). clear K. rewrite (Rabs_right d (Rgt_ge _ _ Hd)) in Hu1 Hv1 Hu2 Hv2. assert (K: forall a b, Rabs (a - b) <= d -> Rabs (a - b) < d1). intros a b H. apply Rle_lt_trans with (1 := H). apply Rle_lt_trans with (1 := Rmin_l _ _). apply Rle_lt_trans with (1 := Rmin_l _ _). apply (Rlt_eps2_eps d1). apply cond_pos. specialize (Hc1 u1 v1 (K _ _ Hu1) (K _ _ Hv1)). clear K. assert (K: forall a b, Rabs (a - b) <= d -> Rabs (a - b) < d2). intros a b H. apply Rle_lt_trans with (1 := H). apply Rle_lt_trans with (1 := Rmin_l _ _). apply Rle_lt_trans with (1 := Rmin_r _ _). apply (Rlt_eps2_eps d2). apply cond_pos. specialize (Hc2 u2 v2 (K _ _ Hu2) (K _ _ Hv2)). clear -Hd H1 H2 Hc1 Hc2. assert (H: forall a b c, b - c = -(a - b) + (a - c)) by (intros ; ring). rewrite (H (Derive (fun z : R => Derive (fun t : R => f z t) v2) u2)). clear H. apply Rle_lt_trans with (1 := Rabs_triang _ _). rewrite Rabs_Ropp (double_var e). apply Rplus_lt_compat. exact Hc2. replace (Derive (fun z : R => Derive (fun t : R => f z t) v2) u2) with (Derive (fun z : R => Derive (fun t : R => f t z) u1) v1). exact Hc1. apply Rmult_eq_reg_l with (d * d). rewrite -H1 -H2. ring. apply Rgt_not_eq. now apply Rmult_gt_0_compat. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive