Library Coquelicot.Derive

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 Rbar.
Require Import Ssreflect.ssreflect.
Require Import Lim_seq Iter.
Require Import Hierarchy Continuity Equiv.
Require Import Rcomplements.
Open Scope R_scope.

This file describes results about differentiability on a generic normed module. Specific results are also given on R with a total function Derive. It ends with the Taylor-Lagrange formula.

Section LinearFct.

Linear functions


Context {K : AbsRing} {U V : NormedModule K}.

Record is_linear (l : UV) := {
  linear_plus : (x y : U), l (plus x y) = plus (l x) (l y) ;
  linear_scal : (k : K) (x : U), l (scal k x) = scal k (l x) ;
  linear_norm : M : R, 0 < M ( x : U, norm (l x) M × norm x) }.

Lemma linear_zero (l : UV) : is_linear l
  l zero = zero.

Lemma linear_opp (l : UV) (x : U) : is_linear l
  l (opp x) = opp (l x).

Lemma linear_cont (l : UV) (x : U) :
  is_linear lcontinuous l x.

Lemma is_linear_ext (l1 l2 : UV) :
  ( x, l1 x = l2 x) → is_linear l1is_linear l2.

zero in a linear function
Lemma is_linear_zero : is_linear (fun _zero).

End LinearFct.

Lemma is_linear_comp {K : AbsRing} {U V W : NormedModule K}
  (l1 : UV) (l2 : VW) :
  is_linear l1is_linear l2is_linear (fun xl2 (l1 x)).

Section Op_LinearFct.

Context {K : AbsRing} {V : NormedModule K}.

id is a linear function
Lemma is_linear_id : is_linear (fun (x : V) ⇒ x).

opp is a linear function
plus is a linear function
Lemma is_linear_plus : is_linear (fun x : V × Vplus (fst x) (snd x)).

fun k scal k x is a linear function
Lemma is_linear_scal_l (x : V) :
  is_linear (fun k : Kscal k x).

fun x scal k x is a linear function if mult is commutative
Lemma is_linear_scal_r (k : K) :
  ( n m : K, mult n m = mult m n)
  → is_linear (fun x : Vscal k x).

End Op_LinearFct.

Lemma is_linear_prod {K : AbsRing} {T U V : NormedModule K}
  (l1 : TU) (l2 : TV) :
  is_linear l1is_linear l2is_linear (fun t : T(l1 t, l2 t)).

Lemma is_linear_fst {K : AbsRing} {U V : NormedModule K} :
  is_linear (fun t : U × Vfst t).

Lemma is_linear_snd {K : AbsRing} {U V : NormedModule K} :
  is_linear (fun t : U × Vsnd t).

Section Linear_domin.

Context {T : Type} {Kw K : AbsRing} {W : NormedModule Kw} {U V : NormedModule K}.

Lemma is_domin_linear {F : (TProp) → Prop} {FF : Filter F} (f : TW) (g : TU) (l : UV) :
  is_linear lis_domin F f gis_domin F f (fun tl (g t)).

End Linear_domin.

Differentiability using filters


Section Diff.

Context {K : AbsRing} {U : NormedModule K} {V : NormedModule K}.

Definition filterdiff (f : UV) F (l : UV) :=
  is_linear l x, is_filter_lim F x
  is_domin F (fun y : Uminus y x) (fun yminus (minus (f y) (f x)) (l (minus y x))).

Definition ex_filterdiff (f : UV) F :=
   (l : UV), filterdiff f F l.

Lemma filterdiff_continuous_aux {F} {FF : Filter F} (f : UV) :
  ex_filterdiff f F x, is_filter_lim F xfilterlim f F (locally (f x)).

Lemma filterdiff_continuous (f : UV) x :
  ex_filterdiff f (locally x) → continuous f x.

Lemma filterdiff_locally {F} {FF : ProperFilter F} (f : UV) x l :
  is_filter_lim F x
  filterdiff f (locally x) l
  filterdiff f F l.

Lemma ex_filterdiff_locally {F} {FF : ProperFilter F} (f : UV) x :
  is_filter_lim F x
  ex_filterdiff f (locally x) →
  ex_filterdiff f F.

Operations


Lemma filterdiff_ext_lin {F} {FF : Filter F} (f : UV) (l1 l2 : UV) :
  filterdiff f F l1 → ( y, l1 y = l2 y) → filterdiff f F l2.

Lemma filterdiff_ext_loc {F} {FF : Filter F} (f g : UV) (l : UV) :
  F (fun yf y = g y) → ( x, is_filter_lim F xf x = g x)
  → filterdiff f F lfilterdiff g F l.
Lemma ex_filterdiff_ext_loc {F} {FF : Filter F} (f g : UV) :
  F (fun yf y = g y) → ( x, is_filter_lim F xf x = g x)
  → ex_filterdiff f Fex_filterdiff g F.

Lemma filterdiff_ext_locally (f g : UV) (x : U) (l : UV) :
  locally x (fun yf y = g y)
  → filterdiff f (locally x) lfilterdiff g (locally x) l.

Lemma ex_filterdiff_ext_locally (f g : UV) x :
  locally x (fun yf y = g y)
  → ex_filterdiff f (locally x) → ex_filterdiff g (locally x).

Lemma filterdiff_ext {F} {FF : Filter F} (f g : UV) (l : UV) :
  ( y , f y = g y)
  → filterdiff f F lfilterdiff g F l.
Lemma ex_filterdiff_ext {F} {FF : Filter F} (f g : UV) :
  ( y , f y = g y)
  → ex_filterdiff f Fex_filterdiff g F.

Lemma filterdiff_const {F} {FF : Filter F} (a : V) :
  filterdiff (fun _a) F (fun _zero).
Lemma ex_filterdiff_const {F} {FF : Filter F} (a : V) :
  ex_filterdiff (fun _a) F.

Lemma filterdiff_linear {F} (l : UV) :
  is_linear lfilterdiff l F l.
Lemma ex_filterdiff_linear {F} (l : UV) :
  is_linear lex_filterdiff l F.

End Diff.

Section Diff_comp.

Context {K : AbsRing} {U V W : NormedModule K}.

Lemma filterdiff_comp
  {F} {FF : Filter F} f g (lf : UV) (lg : VW) :
  filterdiff f F lffilterdiff g (filtermap f F) lg
  → filterdiff (fun yg (f y)) F (fun ylg (lf y)).

Lemma ex_filterdiff_comp
  {F} {FF : Filter F} (f : UV) (g : VW) :
  ex_filterdiff f Fex_filterdiff g (filtermap f F)
  → ex_filterdiff (fun yg (f y)) F.

Lemma filterdiff_comp'
  f g x (lf : UV) (lg : VW) :
  filterdiff f (locally x) lffilterdiff g (locally (f x)) lg
  → filterdiff (fun yg (f y)) (locally x) (fun ylg (lf y)).

Lemma ex_filterdiff_comp'
  (f : UV) (g : VW) x :
  ex_filterdiff f (locally x) → ex_filterdiff g (locally (f x))
  → ex_filterdiff (fun yg (f y)) (locally x).

End Diff_comp.

Section Diff_comp2.

Context {K : AbsRing} {T U V : NormedModule K}.

Section Diff_comp2'.

Context {W : NormedModule K}.

Lemma filterdiff_comp_2
  {F : (TProp) → Prop} {FF : Filter F} :
   (f : TU) (g : TV) (h : UVW) (lf : TU) (lg : TV)
    (lh : UVW),
    filterdiff f F lf
    filterdiff g F lg
    filterdiff (fun th (fst t) (snd t)) (filtermap (fun t(f t,g t)) F) (fun tlh (fst t) (snd t)) →
    filterdiff (fun y : Th (f y) (g y)) F (fun y : Tlh (lf y) (lg y)).

Lemma ex_filterdiff_comp_2
  {F : (TProp) → Prop} {FF : Filter F} :
   (f : TU) (g : TV) (h : UVW),
    ex_filterdiff f F
    ex_filterdiff g F
    ex_filterdiff (fun th (fst t) (snd t)) (filtermap (fun t(f t,g t)) F) →
    ex_filterdiff (fun y : Th (f y) (g y)) F.

End Diff_comp2'.

Context {W : NormedModule K}.

Lemma filterdiff_comp'_2 :
   (f : TU) (g : TV) (h : UVW) x (lf : TU) (lg : TV)
    (lh : UVW),
    filterdiff f (locally x) lf
    filterdiff g (locally x) lg
    filterdiff (fun th (fst t) (snd t)) (locally (f x,g x)) (fun tlh (fst t) (snd t)) →
    filterdiff (fun y : Th (f y) (g y)) (locally x) (fun y : Tlh (lf y) (lg y)).

Lemma ex_filterdiff_comp'_2 :
   (f : TU) (g : TV) (h : UVW) x,
    ex_filterdiff f (locally x) →
    ex_filterdiff g (locally x) →
    ex_filterdiff (fun th (fst t) (snd t)) (locally (f x,g x)) →
    ex_filterdiff (fun y : Th (f y) (g y)) (locally x).

End Diff_comp2.

Section Operations.

Context {K : AbsRing} {V : NormedModule K}.

Lemma filterdiff_id (F : (VProp) → Prop) :
  filterdiff (fun yy) F (fun yy).

Lemma ex_filterdiff_id (F : (VProp) → Prop) :
  ex_filterdiff (fun yy) F.

Lemma filterdiff_opp (F : (VProp) → Prop) :
  filterdiff opp F opp.

Lemma ex_filterdiff_opp (F : (VProp) → Prop) :
  ex_filterdiff opp F.

Lemma filterdiff_plus (F : (V × VProp) → Prop) :
  filterdiff (fun uplus (fst u) (snd u)) F (fun uplus (fst u) (snd u)).

Lemma ex_filterdiff_plus (F : (V × VProp) → Prop) :
  ex_filterdiff (fun uplus (fst u) (snd u)) F.

Lemma filterdiff_minus (F : (V × VProp) → Prop) :
  filterdiff (fun uminus (fst u) (snd u)) F (fun uminus (fst u) (snd u)).

Lemma ex_filterdiff_minus (F : (V × VProp) → Prop) :
  ex_filterdiff (fun uminus (fst u) (snd u)) F.

Local Ltac plus_grab e :=
  repeat rewrite (plus_assoc _ e) -(plus_comm e) -(plus_assoc e).

Lemma filterdiff_scal :
   {F : (K × VProp) → Prop} {FF : ProperFilter F} (x : K × V),
  is_filter_lim F x
  ( (n m : K), mult n m = mult m n) →
  filterdiff (fun t : K × Vscal (fst t) (snd t)) F
    (fun tplus (scal (fst t) (snd x)) (scal (fst x) (snd t))).

Lemma ex_filterdiff_scal : {F} {FF : ProperFilter F} (x : K × V),
  is_filter_lim F x
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff (fun t : K × Vscal (fst t) (snd t)) F.

Lemma filterdiff_scal_l : {F} {FF : Filter F} (x : V),
  filterdiff (fun k : Kscal k x) F (fun kscal k x).

Lemma ex_filterdiff_scal_l : {F} {FF : Filter F} (x : V),
  ex_filterdiff (fun k : Kscal k x) F.

Lemma filterdiff_scal_r : {F} {FF : Filter F} (k : K),
  ( (n m : K), mult n m = mult m n) →
  filterdiff (fun x : Vscal k x) F (fun xscal k x).

Lemma ex_filterdiff_scal_r : {F} {FF : Filter F} (k : K),
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff (fun x : Vscal k x) F.

End Operations.

Lemma filterdiff_mult {K : AbsRing} :
  {F} {FF : ProperFilter F} (x : K × K),
  is_filter_lim F x
  ( (n m : K), mult n m = mult m n) →
  filterdiff (fun t : K × Kmult (fst t) (snd t)) F
    (fun tplus (mult (fst t) (snd x)) (mult (fst x) (snd t))).

Lemma ex_filterdiff_mult {K : AbsRing} :
  {F} {FF : ProperFilter F} (x : K × K),
  is_filter_lim F x
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff (fun t : K × Kmult (fst t) (snd t)) F.

Composed operations

Section Operations_fct.

Context {K : AbsRing} {U V : NormedModule K}.

Lemma filterdiff_opp_fct {F} {FF : Filter F} (f lf : UV) :
  filterdiff f F lf
  filterdiff (fun topp (f t)) F (fun topp (lf t)).
Lemma ex_filterdiff_opp_fct {F} {FF : Filter F} (f : UV) :
  ex_filterdiff f F
  ex_filterdiff (fun topp (f t)) F.

Lemma filterdiff_plus_fct {F} {FF : Filter F} (f g : UV) (lf lg : UV) :
  filterdiff f F lffilterdiff g F lg
  filterdiff (fun uplus (f u) (g u)) F (fun uplus (lf u) (lg u)).
Lemma ex_filterdiff_plus_fct {F} {FF : Filter F} (f g : UV) :
  ex_filterdiff f Fex_filterdiff g F
  ex_filterdiff (fun uplus (f u) (g u)) F.
Lemma filterdiff_iter_plus_fct {I} {F} {FF : Filter F}
  (l : list I) (f : IUV) df (x : U) :
  ( (j : I), List.In j lfilterdiff (f j) F (df j)) →
  filterdiff (fun yiter plus zero l (fun jf j y)) F
    (fun xiter plus zero l (fun jdf j x)).

Lemma filterdiff_minus_fct {F} {FF : Filter F} (f g : UV) (lf lg : UV) :
  filterdiff f F lffilterdiff g F lg
  filterdiff (fun uminus (f u) (g u)) F (fun uminus (lf u) (lg u)).
Lemma ex_filterdiff_minus_fct {F} {FF : Filter F} (f g : UV) :
  ex_filterdiff f Fex_filterdiff g F
  ex_filterdiff (fun uminus (f u) (g u)) F.

Lemma filterdiff_scal_fct x (f : UK) (g : UV) lf lg :
  ( (n m : K), mult n m = mult m n) →
  filterdiff f (locally x) lffilterdiff g (locally x) lg
  filterdiff (fun tscal (f t) (g t)) (locally x)
    (fun tplus (scal (lf t) (g x)) (scal (f x) (lg t))).
Lemma ex_filterdiff_scal_fct x (f : UK) (g : UV) :
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff f (locally x) → ex_filterdiff g (locally x) →
  ex_filterdiff (fun tscal (f t) (g t)) (locally x).

Lemma filterdiff_scal_l_fct : {F} {FF : Filter F} (x : V) (f : UK) lf,
  filterdiff f F lf
  filterdiff (fun uscal (f u) x) F (fun uscal (lf u) x).
Lemma ex_filterdiff_scal_l_fct : {F} {FF : Filter F} (x : V) (f : UK),
  ex_filterdiff f F
  ex_filterdiff (fun uscal (f u) x) F.

Lemma filterdiff_scal_r_fct : {F} {FF : Filter F} (k : K) (f lf : UV),
  ( (n m : K), mult n m = mult m n) →
  filterdiff f F lf
  filterdiff (fun xscal k (f x)) F (fun xscal k (lf x)).
Lemma ex_filterdiff_scal_r_fct : {F} {FF : Filter F} (k : K) (f : UV),
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff f F
  ex_filterdiff (fun xscal k (f x)) F.

End Operations_fct.

Lemma filterdiff_mult_fct {K : AbsRing} {U : NormedModule K}
  (f g : UK) x (lf lg : UK) :
  ( (n m : K), mult n m = mult m n) →
  filterdiff f (locally x) lffilterdiff g (locally x) lg
  → filterdiff (fun tmult (f t) (g t)) (locally x)
    (fun tplus (mult (lf t) (g x)) (mult (f x) (lg t))).

Lemma ex_filterdiff_mult_fct {K : AbsRing} {U : NormedModule K}
  (f g : UK) x :
  ( (n m : K), mult n m = mult m n) →
  ex_filterdiff f (locally x) → ex_filterdiff g (locally x)
  → ex_filterdiff (fun tmult (f t) (g t)) (locally x).

Differentiability in 1 dimentional space


Section Derive.

Context {K : AbsRing} {V : NormedModule K}.

Definition is_derive (f : KV) (x : K) (l : V) :=
  filterdiff f (locally x) (fun y : Kscal y l).

Definition ex_derive (f : KV) (x : K) :=
   l : V, is_derive f x l.

Lemma ex_derive_filterdiff :
   (f : KV) (x : K),
  ex_derive f x ex_filterdiff f (locally x).

Lemma ex_derive_continuous (f : KV) (x : K) :
  ex_derive f xcontinuous f x.

End Derive.

Definitions on R


Definition Derive (f : RR) (x : R) := real (Lim (fun h(f (x+h) - f x)/h) 0).

Lemma is_derive_Reals (f : RR) (x l : R) :
  is_derive f x l derivable_pt_lim f x l.

Derive is correct

Lemma is_derive_unique f x l :
  is_derive f x lDerive f x = l.

Lemma Derive_correct f x :
  ex_derive f xis_derive f x (Derive f x).

Equivalence with standard library Reals

Lemma ex_derive_Reals_0 (f : RR) (x : R) :
  ex_derive f xderivable_pt f x.

Lemma ex_derive_Reals_1 (f : RR) (x : R) :
  derivable_pt f xex_derive f x.

Lemma Derive_Reals (f : RR) (x : R) (pr : derivable_pt f x) :
  derive_pt f x pr = Derive f x.

Extensionality

Section Extensionality.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_ext_loc :
   (f g : KV) (x : K) (l : V),
  locally x (fun t : Kf t = g t) →
  is_derive f x lis_derive g x l.

Lemma ex_derive_ext_loc :
   (f g : KV) (x : K),
  locally x (fun t : Kf t = g t) →
  ex_derive f xex_derive g x.

Lemma is_derive_ext :
   (f g : KV) (x : K) (l : V),
  ( t : K, f t = g t) →
  is_derive f x lis_derive g x l.

Lemma ex_derive_ext :
   (f g : KV) (x : K),
  ( t : K, f t = g t) →
  ex_derive f xex_derive g x.

End Extensionality.

Lemma Derive_ext_loc :
   f g x,
  locally x (fun tf t = g t) →
  Derive f x = Derive g x.

Lemma Derive_ext :
   f g x,
  ( t, f t = g t) →
  Derive f x = Derive g x.

Operations

Constant functions

Section Const.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_const :
   (a : V) (x : K), is_derive (fun _ : Ka) x zero.

Lemma ex_derive_const :
   (a : V) (x : K), ex_derive (fun _a) x.

End Const.

Lemma Derive_const :
   (a x : R),
  Derive (fun _a) x = 0.

Identity function

Section Id.

Context {K : AbsRing}.

Lemma is_derive_id :
   x : K, is_derive (fun t : Kt) x one.

Lemma ex_derive_id :
   x : K, ex_derive (fun t : Kt) x.

End Id.

Lemma Derive_id :
   x,
  Derive id x = 1.

Additive operators

Opposite of functions

Section Opp.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_opp :
   (f : KV) (x : K) (l : V),
  is_derive f x l
  is_derive (fun xopp (f x)) x (opp l).

Lemma ex_derive_opp :
   (f : KV) (x : K),
  ex_derive f x
  ex_derive (fun xopp (f x)) x.

End Opp.

Lemma Derive_opp :
   f x,
  Derive (fun x- f x) x = - Derive f x.

Addition of functions

Section Plus.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_plus :
   (f g : KV) (x : K) (df dg : V),
  is_derive f x df
  is_derive g x dg
  is_derive (fun xplus (f x) (g x)) x (plus df dg).

Lemma ex_derive_plus :
   (f g : KV) (x : K),
  ex_derive f xex_derive g x
  ex_derive (fun xplus (f x) (g x)) x.

Lemma is_derive_sum_n :
   (f : natKV) (n : nat) (x : K) (d : natV),
  ( k, (k n)%natis_derive (f k) x (d k)) →
  is_derive (fun ysum_n (fun kf k y) n) x (sum_n d n).

Lemma ex_derive_sum_n :
   (f : natKV) (n : nat) (x : K),
  ( k, (k n)%natex_derive (f k) x) →
  ex_derive (fun ysum_n (fun kf k y) n) x.

End Plus.

Lemma Derive_plus :
   f g x, ex_derive f xex_derive g x
  Derive (fun xf x + g x) x = Derive f x + Derive g x.

Lemma Derive_sum_n (f : natRR) (n : nat) (x : R) :
  ( k, (k n)%natex_derive (f k) x) →
  Derive (fun ysum_n (fun kf k y) n) x = sum_n (fun kDerive (f k) x) n.

Difference of functions

Section Minus.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_minus :
   (f g : KV) (x : K) (df dg : V),
  is_derive f x df
  is_derive g x dg
  is_derive (fun xminus (f x) (g x)) x (minus df dg).

Lemma ex_derive_minus :
   (f g : KV) (x : K),
  ex_derive f xex_derive g x
  ex_derive (fun xminus (f x) (g x)) x.

End Minus.

Lemma Derive_minus :
   f g x, ex_derive f xex_derive g x
  Derive (fun xf x - g x) x = Derive f x - Derive g x.

Multiplicative operators

Multiplication of functions

Lemma is_derive_inv (f : RR) (x l : R) :
  is_derive f x lf x 0
    → is_derive (fun y : R/ f y) x (-l/(f x)^2).

Lemma ex_derive_inv (f : RR) (x : R) :
  ex_derive f xf x 0
    → ex_derive (fun y : R/ f y) x.

Lemma Derive_inv (f : RR) (x : R) :
  ex_derive f xf x 0
    → Derive (fun y/ f y) x = - Derive f x / (f x) ^ 2.

Lemma is_derive_scal :
   (f : RR) (x k df : R),
  is_derive f x df
  is_derive (fun x : Rk × f x) x (k × df).

Lemma ex_derive_scal :
   (f : RR) (k x : R),
  ex_derive f x
  ex_derive (fun x : Rk × f x) x.

Lemma Derive_scal :
   f k x,
  Derive (fun xk × f x) x = k × Derive f x.

Section Scal_l.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_scal_l :
   (f : KK) (x l : K) (k : V),
  is_derive f x l
  is_derive (fun xscal (f x) k) x (scal l k).

Lemma ex_derive_scal_l :
   (f : KK) (x : K) (k : V),
  ex_derive f x
  ex_derive (fun xscal (f x) k) x.

End Scal_l.

Lemma Derive_scal_l (f : RR) (k x : R) :
  Derive (fun xf x × k) x = Derive f x × k.

Lemma is_derive_mult :
   (f g : RR) (x : R) (df dg : R),
  is_derive f x df
  is_derive g x dg
  is_derive (fun t : Rf t × g t) x (df × g x + f x × dg) .

Lemma ex_derive_mult (f g : RR) (x : R) :
  ex_derive f xex_derive g x
    → ex_derive (fun x : Rf x × g x) x.

Lemma Derive_mult (f g : RR) (x : R) :
  ex_derive f xex_derive g x
    → Derive (fun xf x × g x) x = Derive f x × g x + f x × Derive g x.

Lemma is_derive_pow (f : RR) (n : nat) (x : R) (l : R) :
  is_derive f x lis_derive (fun x : R(f x)^n) x (INR n × l × (f x)^(pred n)).

Lemma ex_derive_pow (f : RR) (n : nat) (x : R) :
  ex_derive f xex_derive (fun x : R(f x)^n) x.

Lemma Derive_pow (f : RR) (n : nat) (x : R) :
  ex_derive f xDerive (fun x(f x)^n) x = (INR n × Derive f x × (f x)^(pred n)).

Lemma is_derive_div :
   (f g : RR) (x : R) (df dg : R),
  is_derive f x df
  is_derive g x dg
  g x 0 →
  is_derive (fun t : Rf t / g t) x ((df × g x - f x × dg) / (g x ^ 2)).

Lemma ex_derive_div (f g : RR) (x : R) :
  ex_derive f xex_derive g xg x 0
    → ex_derive (fun yf y / g y) x.

Lemma Derive_div (f g : RR) (x : R) :
  ex_derive f xex_derive g xg x 0
    → Derive (fun yf y / g y) x = (Derive f x × g x - f x × Derive g x) / (g x) ^ 2.

Composition of functions

Section Comp.

Context {K : AbsRing} {V : NormedModule K}.

Lemma is_derive_comp :
   (f : KV) (g : KK) (x : K) (df : V) (dg : K),
  is_derive f (g x) df
  is_derive g x dg
  is_derive (fun xf (g x)) x (scal dg df).

Lemma ex_derive_comp :
   (f : KV) (g : KK) (x : K),
  ex_derive f (g x) →
  ex_derive g x
  ex_derive (fun xf (g x)) x.

End Comp.

Lemma Derive_comp (f g : RR) (x : R) :
  ex_derive f (g x) → ex_derive g x
    → Derive (fun xf (g x)) x = Derive g x × Derive f (g x).

Mean value theorem


Lemma MVT_gen (f : RR) (a b : R) (df : RR) :
  let a0 := Rmin a b in
  let b0 := Rmax a b in
  ( x, a0 < x < b0is_derive f x (df x))
  → ( x, a0 x b0continuity_pt f x)
  → c, a0 c b0 f b - f a = df c × (b - a).

Lemma incr_function (f : RR) (a b : Rbar) (df : RR) :
  ( (x : R), Rbar_lt a xRbar_lt x bis_derive f x (df x))
  → (( (x : R), Rbar_lt a xRbar_lt x bdf x > 0)
    → ( (x y : R), Rbar_lt a xx < yRbar_lt y bf x < f y)).

Lemma incr_function_le (f : RR) (a b : Rbar) (df : RR) :
  ( (x : R), Rbar_le a xRbar_le x bis_derive f x (df x))
  → (( (x : R), Rbar_le a xRbar_le x bdf x > 0)
    → ( (x y : R), Rbar_le a xx < yRbar_le y bf x < f y)).

Lemma MVT_cor4:
   (f df : RR) a eps,
  ( c, Rabs (c - a) epsis_derive f c (df c)) →
   b, (Rabs (b - a) eps) →
   c, f b - f a = df c × (b - a) (Rabs (c - a) Rabs (b - a)).

Lemma bounded_variation :
   h dh D x y,
  ( t, Rabs (t - x) Rabs (y - x) → is_derive h t (dh t) (Rabs (dh t) D)) →
  Rabs (h y - h x) D × Rabs (y - x).

Newton integration


Lemma fn_eq_Derive_eq: f g a b,
  continuity_pt f acontinuity_pt f b
  continuity_pt g acontinuity_pt g b
  ( x, a < x < bex_derive f x) →
  ( x, a < x < bex_derive g x) →
  ( x, a < x < bDerive f x = Derive g x) →
   C, x, a x bf x = g x + C.

Extension


Section ext_cont.

Context {U : UniformSpace}.

Definition extension_cont (f g : RU) (a x : R) : U :=
  match Rle_dec x a with
    | left _f x
    | right _g x
  end.

Lemma extension_cont_continuous (f g : RU) (a : R) :
  continuous f acontinuous g a
  → f a = g a
  → continuous (extension_cont f g a) a.

End ext_cont.

Section ext_cont'.

Context {V : NormedModule R_AbsRing}.

Lemma extension_cont_is_derive (f g : RV) (a : R) (l : V) :
  is_derive f a lis_derive g a l
  → f a = g a
  → is_derive (extension_cont f g a) a l.

End ext_cont'.

Section ext_C0.

Context {V : NormedModule R_AbsRing}.

Definition extension_C0 (f : RV) (a b : Rbar) (x : R) : V :=
  match Rbar_le_dec a x with
    | left _match Rbar_le_dec x b with
        | left _f x
        | right _f (real b)
      end
    | right _f (real a)
  end.

Lemma extension_C0_ext (f : RV) (a b : Rbar) :
   (x : R), Rbar_le a xRbar_le x b → (extension_C0 f a b) x = f x.

Lemma extension_C0_continuous (f : RV) (a b : Rbar) :
  Rbar_le a b
  → ( x : R, Rbar_le a xRbar_le x bcontinuous f x)
  → x, continuous (extension_C0 f a b) x.

End ext_C0.

C1 extension


Section ext_C1.

Context {V : NormedModule R_AbsRing}.

Definition extension_C1 (f df : RV) (a b : Rbar) (x : R) : V :=
  match Rbar_le_dec a x with
    | left _match Rbar_le_dec x b with
        | left _f x
        | right _plus (f (real b)) (scal (x - real b) (df (real b)))
      end
    | right _plus (f (real a)) (scal (x - real a) (df (real a)))
  end.

Lemma extension_C1_ext (f df : RV) (a b : Rbar) :
   (x : R), Rbar_le a xRbar_le x b → (extension_C1 f df a b) x = f x.

Lemma extension_C1_is_derive (f df : RV) (a b : Rbar) :
  Rbar_le a b
  → ( x : R, Rbar_le a xRbar_le x bis_derive f x (df x))
  → x : R, is_derive (extension_C1 f df a b) x (extension_C0 df a b x).

End ext_C1.

Lemma extension_C1_ex_derive (f df : RR) (a b : Rbar) :
  Rbar_le a b
  → ( x : R, Rbar_le a xRbar_le x bex_derive f x)
  → x : R, ex_derive (extension_C1 f (Derive f) a b) x.

Iterated differential

Definition


Fixpoint Derive_n (f : RR) (n : nat) x :=
  match n with
    | Of x
    | S nDerive (Derive_n f n) x
  end.

Definition ex_derive_n f n x :=
  match n with
  | OTrue
  | S nex_derive (Derive_n f n) x
  end.

Definition is_derive_n f n x l :=
  match n with
  | Of x = l
  | S nis_derive (Derive_n f n) x l
  end.

Lemma is_derive_n_unique f n x l :
  is_derive_n f n x lDerive_n f n x = l.

Lemma Derive_n_correct f n x :
  ex_derive_n f n xis_derive_n f n x (Derive_n f n x).

Extensionality

Lemma Derive_n_ext_loc :
   f g n x,
  locally x (fun tf t = g t) →
  Derive_n f n x = Derive_n g n x.

Lemma ex_derive_n_ext_loc :
   f g n x,
  locally x (fun tf t = g t) →
  ex_derive_n f n xex_derive_n g n x.

Lemma is_derive_n_ext_loc :
   f g n x l,
  locally x (fun tf t = g t) →
  is_derive_n f n x lis_derive_n g n x l.

Lemma Derive_n_ext :
   f g n x,
  ( t, f t = g t) →
  Derive_n f n x = Derive_n g n x.

Lemma ex_derive_n_ext :
   f g n x,
  ( t, f t = g t) →
  ex_derive_n f n xex_derive_n g n x.

Lemma is_derive_n_ext :
   f g n x l,
  ( t, f t = g t) →
  is_derive_n f n x lis_derive_n g n x l.

Lemma Derive_n_comp: f n m x,
  Derive_n (Derive_n f m) n x = Derive_n f (n+m) x.

Lemma is_derive_Sn (f : RR) (n : nat) (x l : R) :
  locally x (ex_derive f) →
  (is_derive_n f (S n) x l is_derive_n (Derive f) n x l).

Constant function

Lemma is_derive_n_const n a : x, is_derive_n (fun _a) (S n) x 0.
Lemma ex_derive_n_const a n x: ex_derive_n (fun _a) n x.
Lemma Derive_n_const n a : x, Derive_n (fun _a) (S n) x = 0.

Operations

Additive operators

Opposite

Lemma Derive_n_opp (f : RR) (n : nat) (x : R) :
  Derive_n (fun x- f x) n x = - Derive_n f n x.

Lemma ex_derive_n_opp (f : RR) (n : nat) (x : R) :
  ex_derive_n f n xex_derive_n (fun x-f x) n x.

Lemma is_derive_n_opp (f : RR) (n : nat) (x l : R) :
  is_derive_n f n x lis_derive_n (fun x-f x) n x (- l).

Addition of functions

Lemma Derive_n_plus (f g : RR) (n : nat) (x : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  Derive_n (fun xf x + g x) n x = Derive_n f n x + Derive_n g n x.

Lemma ex_derive_n_plus (f g : RR) (n : nat) (x : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  ex_derive_n (fun xf x + g x) n x.

Lemma is_derive_n_plus (f g : RR) (n : nat) (x lf lg : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  is_derive_n f n x lfis_derive_n g n x lg
  is_derive_n (fun xf x + g x) n x (lf + lg).

Lemma is_derive_n_iter_plus {I : Type} (l : list I) (f : IRR) (n: nat) (x : R) :
  locally x (fun y (j : I) (k : nat), List.In j l → (k n)%natex_derive_n (f j) k y) →
  is_derive_n (fun yiter Rplus 0 l (fun jf j y)) n x
    (iter Rplus 0 l (fun jDerive_n (f j) n x)).

Lemma ex_derive_n_iter_plus {I : Type} (l : list I) (f : IRR) (n: nat) (x : R) :
  locally x (fun y (j : I) (k : nat), List.In j l → (k n)%natex_derive_n (f j) k y) →
  ex_derive_n (fun yiter Rplus 0 l (fun jf j y)) n x.

Lemma Derive_n_iter_plus {I : Type} (l : list I) (f : IRR) (n: nat) (x : R) :
  locally x (fun y (j : I) (k : nat), List.In j l → (k n)%natex_derive_n (f j) k y) →
  Derive_n (fun yiter Rplus 0 l (fun jf j y)) n x =
    iter Rplus 0 l (fun jDerive_n (f j) n x).

Lemma is_derive_n_sum_n_m n m (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (n l m)%nat ->(j k)%natex_derive_n (f l) j t) →
  is_derive_n (fun ysum_n_m (fun jf j y) n m) k x
    (sum_n_m (fun jDerive_n (f j) k x) n m).
Lemma ex_derive_n_sum_n_m n m (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (n l m)%nat ->(j k)%natex_derive_n (f l) j t) →
  ex_derive_n (fun ysum_n_m (fun jf j y) n m) k x.
Lemma Derive_n_sum_n_m n m (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (n l m)%nat ->(j k)%natex_derive_n (f l) j t) →
  Derive_n (fun ysum_n_m (fun jf j y) n m) k x
    = sum_n_m (fun jDerive_n (f j) k x) n m.

Lemma is_derive_n_sum_n n (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (l n)%nat ->(j k)%natex_derive_n (f l) j t) →
  is_derive_n (fun ysum_n (fun jf j y) n) k x
    (sum_n (fun jDerive_n (f j) k x) n).
Lemma ex_derive_n_sum_n n (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (l n)%nat ->(j k)%natex_derive_n (f l) j t) →
  ex_derive_n (fun ysum_n (fun jf j y) n) k x.
Lemma Derive_n_sum_n n (f : natRR) (k: nat) (x : R) :
  locally x (fun t l j , (l n)%nat ->(j k)%natex_derive_n (f l) j t) →
  Derive_n (fun ysum_n (fun jf j y) n) k x =
    (sum_n (fun jDerive_n (f j) k x) n).

Subtraction of functions

Lemma Derive_n_minus (f g : RR) (n : nat) (x : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  Derive_n (fun xf x - g x) n x = Derive_n f n x - Derive_n g n x.
Lemma ex_derive_n_minus (f g : RR) (n : nat) (x : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  ex_derive_n (fun xf x - g x) n x.
Lemma is_derive_n_minus (f g : RR) (n : nat) (x lf lg : R) :
  locally x (fun y k, (k n)%natex_derive_n f k y) →
  locally x (fun y k, (k n)%natex_derive_n g k y) →
  is_derive_n f n x lfis_derive_n g n x lg
  is_derive_n (fun xf x - g x) n x (lf - lg).

Multiplicative operators

Scalar multiplication

Lemma Derive_n_scal_l (f : RR) (n : nat) (a x : R) :
  Derive_n (fun ya × f y) n x = a × Derive_n f n x.

Lemma ex_derive_n_scal_l (f : RR) (n : nat) (a x : R) :
  ex_derive_n f n xex_derive_n (fun ya × f y) n x.

Lemma is_derive_n_scal_l (f : RR) (n : nat) (a x l : R) :
  is_derive_n f n x lis_derive_n (fun ya × f y) n x (a × l).

Lemma Derive_n_scal_r (f : RR) (n : nat) (a x : R) :
  Derive_n (fun yf y × a) n x = Derive_n f n x × a.
Lemma ex_derive_n_scal_r (f : RR) (n : nat) (a x : R) :
  ex_derive_n f n xex_derive_n (fun yf y × a) n x.
Lemma is_derive_n_scal_r (f : RR) (n : nat) (a x l : R) :
  is_derive_n f n x lis_derive_n (fun yf y × a) n x (l × a).

Composition

Composition with linear functions

Lemma Derive_n_comp_scal (f : RR) (a : R) (n : nat) (x : R) :
  locally (a × x) (fun x k, (k n)%natex_derive_n f k x) →
  Derive_n (fun yf (a × y)) n x = (a ^ n × Derive_n f n (a × x)).

Lemma ex_derive_n_comp_scal (f : RR) (a : R) (n : nat) (x : R) :
  locally (a × x) (fun x k, (k n)%natex_derive_n f k x)
  → ex_derive_n (fun yf (a × y)) n x.

Lemma is_derive_n_comp_scal (f : RR) (a : R) (n : nat) (x l : R) :
  locally (a × x) (fun x k, (k n)%natex_derive_n f k x)
  → is_derive_n f n (a × x) l
  → is_derive_n (fun yf (a × y)) n x (a ^ n × l).

Lemma Derive_n_comp_opp (f : RR) (n : nat) (x : R) :
  locally (- x) (fun y ⇒ ( k, (k n)%natex_derive_n f k y)) →
  Derive_n (fun yf (- y)) n x = ((-1) ^ n × Derive_n f n (-x)).
Lemma ex_derive_n_comp_opp (f : RR) (n : nat) (x : R) :
  locally (- x) (fun y ⇒ ( k, (k n)%natex_derive_n f k y)) →
  ex_derive_n (fun yf (- y)) n x.
Lemma is_derive_n_comp_opp (f : RR) (n : nat) (x l : R) :
  locally (- x) (fun y ⇒ ( k, (k n)%natex_derive_n f k y)) →
  is_derive_n f n (-x) l
  is_derive_n (fun yf (- y)) n x ((-1)^n × l).

Lemma Derive_n_comp_trans (f : RR) (n : nat) (x b : R) :
  Derive_n (fun yf (y + b)) n x = Derive_n f n (x + b).

Lemma ex_derive_n_comp_trans (f : RR) (n : nat) (x b : R) :
  ex_derive_n f n (x + b) →
  ex_derive_n (fun yf (y + b)) n x.

Lemma is_derive_n_comp_trans (f : RR) (n : nat) (x b l : R) :
  is_derive_n f n (x + b) l
  is_derive_n (fun yf (y + b)) n x l.

Taylor-Lagrange formula


Theorem Taylor_Lagrange :
   f n x y, x < y
  ( t, x t y k, (k S n)%natex_derive_n f k t ) →
   zeta, x < zeta < y
    f y = sum_f_R0 (fun m(y-x) ^ m / INR (fact m) × Derive_n f m x ) n
        + (y-x) ^ (S n) / INR (fact (S n)) × Derive_n f (S n) zeta.