Library Coquelicot.Derive_2d

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2015 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Import Reals Omega.
Require Import Ssreflect.ssreflect.
Require Import Rcomplements Hierarchy Continuity Derive.

This file describes results about differentiability in R x R. This includes the Schwarz theorem and the 2D Taylor-Lagrange inequality.

Differentiability


Definition differentiable_pt_lim (f : RRR) (x y : R) (lx ly : R) :=
   eps : posreal, locally_2d (fun u v
    Rabs (f u v - f x y - (lx × (u - x) + ly × (v - y))) eps × Rmax (Rabs (u - x)) (Rabs (v - y))) x y.

Lemma differentiable_pt_lim_ext : f1 f2 x y lx ly,
  locally_2d (fun u vf1 u v = f2 u v) x y
  differentiable_pt_lim f1 x y lx lydifferentiable_pt_lim f2 x y lx ly.

Definition differentiable_pt (f : RRR) (x y : R) :=
   lx, ly, differentiable_pt_lim f x y lx ly.

Lemma differentiable_continuity_pt : f x y,
  differentiable_pt f x ycontinuity_2d_pt f x y.

Lemma derivable_differentiable_pt_lim : f x y l2,
  locally_2d (fun u vex_derive (fun zf z v) u) x y
  is_derive (fun zf x z) y l2
  continuity_2d_pt (fun u vDerive (fun zf z v) u) x y
  differentiable_pt_lim f x y (Derive (fun uf u y) x) l2.

Lemma differentiable_pt_lim_proj1_0 (f : RR) (x y l : R) :
  derivable_pt_lim f x ldifferentiable_pt_lim (fun u vf u) x y l 0.

Lemma differentiable_pt_lim_proj1_1 (f : RR) (x y l : R) :
  differentiable_pt_lim (fun u vf u) x y l 0 → derivable_pt_lim f x l.

Lemma differentiable_pt_lim_unique (f : RRR) (x y : R) (lx ly : R) :
  differentiable_pt_lim f x y lx ly
    → Derive (fun xf x y) x = lx Derive (fun yf x y) y = ly.

Operations


Lemma differentiable_pt_lim_comp : f1 f2 f3 x y l1x l1y l2x l2y l3x l3y,
  differentiable_pt_lim f1 (f2 x y) (f3 x y) l1x l1y
  differentiable_pt_lim f2 x y l2x l2ydifferentiable_pt_lim f3 x y l3x l3y
  differentiable_pt_lim (fun u vf1 (f2 u v) (f3 u v)) x y
    (l1x × l2x + l1y × l3x) (l1x × l2y + l1y × l3y).

Lemma derivable_pt_lim_comp_2d : f1 f2 f3 x l1x l1y l2 l3,
  differentiable_pt_lim f1 (f2 x) (f3 x) l1x l1y
  derivable_pt_lim f2 x l2derivable_pt_lim f3 x l3
  derivable_pt_lim (fun tf1 (f2 t) (f3 t)) x (l1x × l2 + l1y × l3).

Partial derivatives


Definition partial_derive (m k : nat) (f : RRR) : RRR :=
  fun x yDerive_n (fun tDerive_n (fun zf t z) k y) m x.

Definition differential (p : nat) (f : RRR) (x y dx dy : R) : R :=
  sum_f_R0
    (fun m
      C p m ×
      partial_derive m (p - m)%nat f x y ×
      dx ^ m × dy ^ (p - m)%nat)
    p.

Definition DL_pol (n : nat) (f : RRR) (x y dx dy : R) : R :=
  sum_f_R0
    (fun p
      differential p f x y dx dy / INR (fact p))
    n.

Lemma partial_derive_ext_loc :
   f g p q x y,
  locally_2d (fun u vf u v = g u v) x y
  partial_derive p q f x y = partial_derive p q g x y.

Schwarz theorem


Lemma Schwarz_aux :
   f x y (eps : posreal),
  ( u v, Rabs (u - x) < epsRabs (v - y) < eps
    ex_derive (fun zf z v) u
    ex_derive (fun zDerive (fun tf t z) u) v ) →
   h k, Rabs h < epsRabs k < eps
  let phi k x := f x (y + k) - f x y in
   u, v,
  Rabs (u - x) Rabs h Rabs (v - y) Rabs k
  phi k (x + h) - phi k x = h × k × (Derive (fun zDerive (fun tf t z) u) v).

Lemma Schwarz :
   f x y,
  locally_2d (fun u v
    ex_derive (fun zf z v) u
    ex_derive (fun zf u z) v
    ex_derive (fun zDerive (fun tf z t) v) u
    ex_derive (fun zDerive (fun tf t z) u) v) x y
  continuity_2d_pt (fun u vDerive (fun zDerive (fun tf z t) v) u) x y
  continuity_2d_pt (fun u vDerive (fun zDerive (fun tf t z) u) v) x y
  Derive (fun zDerive (fun tf z t) y) x = Derive (fun zDerive (fun tf t z) x) y.

Lemma partial_derive_add_zero: f p q r s x y,
  (q=0)%nat (r=0)%nat
  partial_derive p q (partial_derive r s f) x y
   = partial_derive (p+r) (q+s) f x y.

Iterated differential


Fixpoint ex_diff_n f n x y :=
  continuity_2d_pt f x y
  match n with
  | OTrue
  | S n
    ex_derive (fun zf z y) x
    ex_derive (fun zf x z) y
    ex_diff_n (fun u vDerive (fun zf z v) u) n x y
    ex_diff_n (fun u vDerive (fun zf u z) v) n x y
  end.

Lemma ex_diff_n_ext_loc: f g n x y,
    locally_2d (fun u vf u v = g u v) x y
      → ex_diff_n f n x yex_diff_n g n x y.

Lemma ex_diff_n_m :
   n m, (m n)%nat f x y, ex_diff_n f n x yex_diff_n f m x y.

Lemma ex_diff_n_deriv_aux1: f n x y,
  ex_diff_n f (S n) x yex_diff_n (fun u vDerive (fun zf z v) u) n x y.

Lemma ex_diff_n_deriv_aux2: f n x y,
  ex_diff_n f (S n) x yex_diff_n (fun u vDerive (fun zf u z) v) n x y.

Lemma ex_diff_n_deriv: n p q, (p+q n)%nat f x y,
    ex_diff_n f n x yex_diff_n (partial_derive p q f) (n -(p+q)) x y.

Lemma ex_diff_n_ex_deriv_inf_1 : n p k, (p+k < n)%nat f x y,
    ex_diff_n f n x y
    ex_derive (fun z : Rpartial_derive p k f z y) x.

Lemma ex_diff_n_ex_deriv_inf_2 : n p k, (p+k < n)%nat f x y,
  ex_diff_n f n x y
  ex_derive (fun zpartial_derive p k f x z) y.

Lemma ex_diff_n_continuity_inf_1 : n p k, (p+k < n)%nat f x y,
  ex_diff_n f n x y
  continuity_2d_pt (fun u vDerive (fun z : Rpartial_derive p k f z v) u) x y.

Lemma Derive_partial_derive_aux1: p f x y,
  locally_2d (ex_diff_n f (S p)) x y
   partial_derive 1 p f x y = partial_derive 0 p (partial_derive 1 0 f) x y.

Lemma Derive_partial_derive_aux2: p k f x y,
  locally_2d (ex_diff_n f (p+S k)) x y
  partial_derive 0 1 (partial_derive p k f) x y =
     partial_derive p (S k) f x y.

Lemma Derive_partial_derive: p k f x y,
  locally_2d (ex_diff_n f (p+S k)) x y
  Derive (fun v : Rpartial_derive p k f x v) y =
     partial_derive p (S k) f x y.

Lemma ex_diff_n_continuity_inf_2 : n p k, (p+k < n)%nat f x y,
  ex_diff_n f n x y
  continuity_2d_pt (fun u vDerive (fun z : Rpartial_derive p k f u z) v) x y.

2D Taylor-Lagrange inequality


Definition DL_regular_n f m x y :=
   D, locally_2d (fun u v
    Rabs (f u v - DL_pol m f x y (u-x) (v-y)) D × (Rmax (Rabs (u-x)) (Rabs (v-y))) ^ (S m)) x y.

Theorem Taylor_Lagrange_2d : f n x y,
  locally_2d (fun u vex_diff_n f (S n) u v) x yDL_regular_n f n x y.