proposition: Lemma Schwarz_aux : forall f x y (eps : posreal), ( forall u v, Rabs (u - x) < eps -> Rabs (v - y) < eps -> ex_derive (fun z : R => f z v) u /\ ex_derive (fun z : R => Derive (fun t => f t z) u) v ) -> forall h k, Rabs h < eps -> Rabs k < eps -> let phi k x := f x (y + k) - f x y in exists u, exists v, Rabs (u - x) <= Rabs h /\ Rabs (v - y) <= Rabs k /\ phi k (x + h) - phi k x = h * k * (Derive (fun z => Derive (fun t => f t z) u) v).
proof: Proof. intros f x y eps HD h k Hh Hk phi. assert (Hx: x + h - x = h) by ring. assert (Hy: y + k - y = k) by ring. destruct (MVT_cor4 (phi k) (Derive (phi k)) x (Rabs h)) with (b := x + h) as (u&Hu1&Hu2). intros c Hc. apply Derive_correct. apply: ex_derive_minus. apply (HD c). now apply Rle_lt_trans with (Rabs h). now rewrite Hy. apply (HD c). now apply Rle_lt_trans with (Rabs h). rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. rewrite Hx. apply Rle_refl. rewrite Hx in Hu1, Hu2. exists u. destruct (MVT_cor4 (fun v => Derive (fun t => f t v) u) (Derive (fun v => Derive (fun t => f t v) u)) y (Rabs k)) with (b := y + k) as (v&Hv1&Hv2). intros c Hc. apply Derive_correct, HD. now apply Rle_lt_trans with (Rabs h). now apply Rle_lt_trans with (1 := Hc). rewrite Hy. apply Rle_refl. rewrite Hy in Hv1, Hv2. exists v. refine (conj Hu2 (conj Hv2 _)). rewrite Hu1 /phi Derive_minus. rewrite Hv1. ring. apply (HD u). now apply Rle_lt_trans with (Rabs h). now rewrite Hy. apply (HD u). now apply Rle_lt_trans with (Rabs h). rewrite /Rminus Rplus_opp_r Rabs_R0. apply cond_pos. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Hierarchy Continuity Derive