Library Coquelicot.Derive

This file is part of the Coquelicot formalization of real analysis in Coq: http://coquelicot.saclay.inria.fr/

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 Psatz.
Require Import mathcomp.ssreflect.ssreflect.
Require Import Rcomplements Rbar Lim_seq Iter.
Require Import Hierarchy Continuity Equiv.
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 : U → V) := {
  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 : U → V) : is_linear l →
  l zero = zero.

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

Lemma linear_cont (l : U → V) (x : U) :
  is_linear l → continuous l x.

Lemma is_linear_ext (l1 l2 : U → V) :
  (∀ x, l1 x = l2 x ) → is_linear l1 → is_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 : U → V) (l2 : V → W) :
is_linear l1 → is_linear l2 → is_linear (fun x ⇒ l2 (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

Lemma is_linear_opp : is_linear (@opp V).

plus is a linear function

Lemma is_linear_plus : is_linear (fun x : V × V ⇒ plus (fst x) (snd x)).

fun k ⇒ scal k x is a linear function

Lemma is_linear_scal_l (x : V) :
is_linear (fun k : K ⇒ scal 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 : V ⇒ scal k x).

End Op_LinearFct.

Lemma is_linear_prod {K : AbsRing} {T U V : NormedModule K}
  (l1 : T → U) (l2 : T → V) :
  is_linear l1 → is_linear l2 → is_linear (fun t : T ⇒ (l1 t , l2 t )).

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

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

Section Linear_domin.

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

Lemma is_domin_linear {F : (T → Prop) → Prop} {FF : Filter F} (f : T → W) (g : T → U) (l : U → V) :
  is_linear l → is_domin F f g → is_domin F f (fun t ⇒ l (g t)).

End Linear_domin.

Differentiability using filters

Section Diff.

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

Definition filterdiff (f : U → V) F (l : U → V) :=
  is_linear l ∧ ∀ x, is_filter_lim F x →
  is_domin F (fun y : U ⇒ minus y x) (fun y ⇒ minus (minus (f y) (f x)) (l (minus y x))).

Definition ex_filterdiff (f : U → V) F :=
  ∃ (l : U → V ), filterdiff f F l.

Lemma filterdiff_continuous_aux {F} {FF : Filter F} (f : U → V) :
  ex_filterdiff f F → ∀ x, is_filter_lim F x → filterlim f F (locally (f x)).

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

Lemma filterdiff_locally {F} {FF : ProperFilter F} (f : U → V) 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 : U → V) 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 : U → V) (l1 l2 : U → V) :
  filterdiff f F l1 → (∀ y, l1 y = l2 y ) → filterdiff f F l2.

Lemma filterdiff_ext_loc {F} {FF : Filter F} (f g : U → V) (l : U → V) :
  F (fun y ⇒ f y = g y) → (∀ x, is_filter_lim F x → f x = g x )
  → filterdiff f F l → filterdiff g F l.
Lemma ex_filterdiff_ext_loc {F} {FF : Filter F} (f g : U → V) :
  F (fun y ⇒ f y = g y) → (∀ x, is_filter_lim F x → f x = g x )
  → ex_filterdiff f F → ex_filterdiff g F.

Lemma filterdiff_ext_locally (f g : U → V) (x : U) (l : U → V) :
  locally x (fun y ⇒ f y = g y)
  → filterdiff f (locally x) l → filterdiff g (locally x) l.

Lemma ex_filterdiff_ext_locally (f g : U → V) x :
  locally x (fun y ⇒ f y = g y)
  → ex_filterdiff f (locally x) → ex_filterdiff g (locally x).

Lemma filterdiff_ext {F} {FF : Filter F} (f g : U → V) (l : U → V) :
  (∀ y , f y = g y )
  → filterdiff f F l → filterdiff g F l.
Lemma ex_filterdiff_ext {F} {FF : Filter F} (f g : U → V) :
  (∀ y , f y = g y )
  → ex_filterdiff f F → ex_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 : U → V) :
  is_linear l → filterdiff l F l.
Lemma ex_filterdiff_linear {F} (l : U → V) :
  is_linear l → ex_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 : U → V) (lg : V → W) :
  filterdiff f F lf → filterdiff g (filtermap f F) lg
  → filterdiff (fun y ⇒ g (f y)) F (fun y ⇒ lg (lf y)).

Lemma ex_filterdiff_comp
  {F} {FF : Filter F} (f : U → V) (g : V → W) :
  ex_filterdiff f F → ex_filterdiff g (filtermap f F)
  → ex_filterdiff (fun y ⇒ g (f y)) F.

Lemma filterdiff_comp'
  f g x (lf : U → V) (lg : V → W) :
  filterdiff f (locally x) lf → filterdiff g (locally (f x)) lg
  → filterdiff (fun y ⇒ g (f y)) (locally x) (fun y ⇒ lg (lf y)).

Lemma ex_filterdiff_comp'
  (f : U → V) (g : V → W) x :
  ex_filterdiff f (locally x) → ex_filterdiff g (locally (f x))
  → ex_filterdiff (fun y ⇒ g (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 : (T → Prop) → Prop} {FF : Filter F} :
  ∀ (f : T → U) (g : T → V) (h : U → V → W) (lf : T → U) (lg : T → V)
    (lh : U → V → W),
    filterdiff f F lf →
    filterdiff g F lg →
    filterdiff (fun t ⇒ h (fst t) (snd t)) (filtermap (fun t ⇒ (f t ,g t )) F) (fun t ⇒ lh (fst t) (snd t)) →
    filterdiff (fun y : T ⇒ h (f y) (g y)) F (fun y : T ⇒ lh (lf y) (lg y)).

Lemma ex_filterdiff_comp_2
  {F : (T → Prop) → Prop} {FF : Filter F} :
  ∀ (f : T → U) (g : T → V) (h : U → V → W),
    ex_filterdiff f F →
    ex_filterdiff g F →
    ex_filterdiff (fun t ⇒ h (fst t) (snd t)) (filtermap (fun t ⇒ (f t ,g t )) F) →
    ex_filterdiff (fun y : T ⇒ h (f y) (g y)) F.

End Diff_comp2'.

Context {W : NormedModule K}.

Lemma filterdiff_comp'_2 :
  ∀ (f : T → U) (g : T → V) (h : U → V → W) x (lf : T → U) (lg : T → V)
    (lh : U → V → W),
    filterdiff f (locally x) lf →
    filterdiff g (locally x) lg →
    filterdiff (fun t ⇒ h (fst t) (snd t)) (locally (f x ,g x )) (fun t ⇒ lh (fst t) (snd t)) →
    filterdiff (fun y : T ⇒ h (f y) (g y)) (locally x) (fun y : T ⇒ lh (lf y) (lg y)).

Lemma ex_filterdiff_comp'_2 :
  ∀ (f : T → U) (g : T → V) (h : U → V → W) x,
    ex_filterdiff f (locally x) →
    ex_filterdiff g (locally x) →
    ex_filterdiff (fun t ⇒ h (fst t) (snd t)) (locally (f x ,g x )) →
    ex_filterdiff (fun y : T ⇒ h (f y) (g y)) (locally x).

End Diff_comp2.

Section Operations.

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

Lemma filterdiff_id (F : (V → Prop) → Prop) :
  filterdiff (fun y ⇒ y) F (fun y ⇒ y).

Lemma ex_filterdiff_id (F : (V → Prop) → Prop) :
  ex_filterdiff (fun y ⇒ y) F.

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

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

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

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

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

Lemma ex_filterdiff_minus (F : (V × V → Prop) → Prop) :
  ex_filterdiff (fun u ⇒ minus (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 × V → Prop) → 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 × V ⇒ scal (fst t) (snd t)) F
    (fun t ⇒ plus (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 × V ⇒ scal (fst t) (snd t)) F.

Lemma filterdiff_scal_l : ∀ {F} {FF : Filter F} (x : V),
  filterdiff (fun k : K ⇒ scal k x) F (fun k ⇒ scal k x).

Lemma ex_filterdiff_scal_l : ∀ {F} {FF : Filter F} (x : V),
  ex_filterdiff (fun k : K ⇒ scal 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 : V ⇒ scal k x) F (fun x ⇒ scal 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 : V ⇒ scal 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 × K ⇒ mult (fst t) (snd t)) F
    (fun t ⇒ plus (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 × K ⇒ mult (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 : U → V) :
  filterdiff f F lf →
  filterdiff (fun t ⇒ opp (f t)) F (fun t ⇒ opp (lf t)).
Lemma ex_filterdiff_opp_fct {F} {FF : Filter F} (f : U → V) :
  ex_filterdiff f F →
  ex_filterdiff (fun t ⇒ opp (f t)) F.

Lemma filterdiff_plus_fct {F} {FF : Filter F} (f g : U → V) (lf lg : U → V) :
  filterdiff f F lf → filterdiff g F lg →
  filterdiff (fun u ⇒ plus (f u) (g u)) F (fun u ⇒ plus (lf u) (lg u)).
Lemma ex_filterdiff_plus_fct {F} {FF : Filter F} (f g : U → V) :
  ex_filterdiff f F → ex_filterdiff g F →
  ex_filterdiff (fun u ⇒ plus (f u) (g u)) F.
Lemma filterdiff_iter_plus_fct {I} {F} {FF : Filter F}
  (l : list I) (f : I → U → V) df (x : U) :
  (∀ (j : I), List.In j l → filterdiff (f j) F (df j)) →
  filterdiff (fun y ⇒ iter plus zero l (fun j ⇒ f j y)) F
    (fun x ⇒ iter plus zero l (fun j ⇒ df j x)).

Lemma filterdiff_minus_fct {F} {FF : Filter F} (f g : U → V) (lf lg : U → V) :
  filterdiff f F lf → filterdiff g F lg →
  filterdiff (fun u ⇒ minus (f u) (g u)) F (fun u ⇒ minus (lf u) (lg u)).
Lemma ex_filterdiff_minus_fct {F} {FF : Filter F} (f g : U → V) :
  ex_filterdiff f F → ex_filterdiff g F →
  ex_filterdiff (fun u ⇒ minus (f u) (g u)) F.

Lemma filterdiff_scal_fct x (f : U → K) (g : U → V) lf lg :
  (∀ (n m : K), mult n m = mult m n ) →
  filterdiff f (locally x) lf → filterdiff g (locally x) lg →
  filterdiff (fun t ⇒ scal (f t) (g t)) (locally x)
    (fun t ⇒ plus (scal (lf t) (g x)) (scal (f x) (lg t))).
Lemma ex_filterdiff_scal_fct x (f : U → K) (g : U → V) :
  (∀ (n m : K), mult n m = mult m n ) →
  ex_filterdiff f (locally x) → ex_filterdiff g (locally x) →
  ex_filterdiff (fun t ⇒ scal (f t) (g t)) (locally x).

Lemma filterdiff_scal_l_fct : ∀ {F} {FF : Filter F} (x : V) (f : U → K) lf,
  filterdiff f F lf →
  filterdiff (fun u ⇒ scal (f u) x) F (fun u ⇒ scal (lf u) x).
Lemma ex_filterdiff_scal_l_fct : ∀ {F} {FF : Filter F} (x : V) (f : U → K),
  ex_filterdiff f F →
  ex_filterdiff (fun u ⇒ scal (f u) x) F.

Lemma filterdiff_scal_r_fct : ∀ {F} {FF : Filter F} (k : K) (f lf : U → V),
  (∀ (n m : K), mult n m = mult m n ) →
  filterdiff f F lf →
  filterdiff (fun x ⇒ scal k (f x)) F (fun x ⇒ scal k (lf x)).
Lemma ex_filterdiff_scal_r_fct : ∀ {F} {FF : Filter F} (k : K) (f : U → V),
  (∀ (n m : K), mult n m = mult m n ) →
  ex_filterdiff f F →
  ex_filterdiff (fun x ⇒ scal k (f x)) F.

End Operations_fct.

Lemma filterdiff_mult_fct {K : AbsRing} {U : NormedModule K}
  (f g : U → K) x (lf lg : U → K) :
  (∀ (n m : K), mult n m = mult m n ) →
  filterdiff f (locally x) lf → filterdiff g (locally x) lg
  → filterdiff (fun t ⇒ mult (f t) (g t)) (locally x)
    (fun t ⇒ plus (mult (lf t) (g x)) (mult (f x) (lg t))).

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

Differentiability in 1 dimentional space

Section Derive.

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

Definition is_derive (f : K → V) (x : K) (l : V) :=
  filterdiff f (locally x) (fun y : K ⇒ scal y l).

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

Lemma ex_derive_filterdiff :
  ∀ (f : K → V) (x : K),
  ex_derive f x ↔ ex_filterdiff f (locally x).

Lemma ex_derive_continuous (f : K → V) (x : K) :
  ex_derive f x → continuous f x.

End Derive.

Definitions on R

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

Lemma is_derive_Reals (f : R → R) (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 l → Derive f x = l.

Lemma Derive_correct f x :
ex_derive f x → is_derive f x (Derive f x).

Equivalence with standard library Reals

Lemma ex_derive_Reals_0 (f : R → R) (x : R) :
  ex_derive f x → derivable_pt f x.

Lemma ex_derive_Reals_1 (f : R → R) (x : R) :
  derivable_pt f x → ex_derive f x.

Lemma Derive_Reals (f : R → R) (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 : K → V) (x : K) (l : V),
  locally x (fun t : K ⇒ f t = g t) →
  is_derive f x l → is_derive g x l.

Lemma ex_derive_ext_loc :
  ∀ (f g : K → V) (x : K),
  locally x (fun t : K ⇒ f t = g t) →
  ex_derive f x → ex_derive g x.

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

Lemma ex_derive_ext :
  ∀ (f g : K → V) (x : K),
  (∀ t : K, f t = g t ) →
  ex_derive f x → ex_derive g x.

End Extensionality.

Lemma Derive_ext_loc :
  ∀ f g x,
  locally x (fun t ⇒ f 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 _ : K ⇒ a) 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 : K ⇒ t) x one.

Lemma ex_derive_id :
  ∀ x : K, ex_derive (fun t : K ⇒ t) 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 : K → V) (x : K) (l : V),
  is_derive f x l →
  is_derive (fun x ⇒ opp (f x)) x (opp l).

Lemma ex_derive_opp :
  ∀ (f : K → V) (x : K),
  ex_derive f x →
  ex_derive (fun x ⇒ opp (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 : K → V) (x : K) (df dg : V),
  is_derive f x df →
  is_derive g x dg →
  is_derive (fun x ⇒ plus (f x) (g x)) x (plus df dg).

Lemma ex_derive_plus :
  ∀ (f g : K → V) (x : K),
  ex_derive f x → ex_derive g x →
  ex_derive (fun x ⇒ plus (f x) (g x)) x.

Lemma is_derive_sum_n :
  ∀ (f : nat → K → V) (n : nat) (x : K) (d : nat → V),
  (∀ k, (k ≤ n)%nat → is_derive (f k) x (d k)) →
  is_derive (fun y ⇒ sum_n (fun k ⇒ f k y) n) x (sum_n d n).

Lemma ex_derive_sum_n :
  ∀ (f : nat → K → V) (n : nat) (x : K),
  (∀ k, (k ≤ n)%nat → ex_derive (f k) x ) →
  ex_derive (fun y ⇒ sum_n (fun k ⇒ f k y) n) x.

End Plus.

Lemma Derive_plus :
  ∀ f g x, ex_derive f x → ex_derive g x →
  Derive (fun x ⇒ f x + g x) x = Derive f x + Derive g x.

Lemma Derive_sum_n (f : nat → R → R) (n : nat) (x : R) :
  (∀ k, (k ≤ n)%nat → ex_derive (f k) x ) →
  Derive (fun y ⇒ sum_n (fun k ⇒ f k y) n) x = sum_n (fun k ⇒ Derive (f k) x) n.

Difference of functions

Section Minus.

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

Lemma is_derive_minus :
  ∀ (f g : K → V) (x : K) (df dg : V),
  is_derive f x df →
  is_derive g x dg →
  is_derive (fun x ⇒ minus (f x) (g x)) x (minus df dg).

Lemma ex_derive_minus :
  ∀ (f g : K → V) (x : K),
  ex_derive f x → ex_derive g x →
  ex_derive (fun x ⇒ minus (f x) (g x)) x.

End Minus.

Lemma Derive_minus :
  ∀ f g x, ex_derive f x → ex_derive g x →
  Derive (fun x ⇒ f x - g x) x = Derive f x - Derive g x.

Multiplicative operators

Multiplication of functions

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

Lemma ex_derive_inv (f : R → R) (x : R) :
  ex_derive f x → f x ≠ 0
    → ex_derive (fun y : R ⇒ / f y) x.

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

Lemma is_derive_scal :
  ∀ (f : R → R) (x k df : R),
  is_derive f x df →
  is_derive (fun x : R ⇒ k × f x) x (k × df).

Lemma ex_derive_scal :
  ∀ (f : R → R) (k x : R),
  ex_derive f x →
  ex_derive (fun x : R ⇒ k × f x) x.

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

Section Scal_l.

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

Lemma is_derive_scal_l :
  ∀ (f : K → K) (x l : K) (k : V),
  is_derive f x l →
  is_derive (fun x ⇒ scal (f x) k) x (scal l k).

Lemma ex_derive_scal_l :
  ∀ (f : K → K) (x : K) (k : V),
  ex_derive f x →
  ex_derive (fun x ⇒ scal (f x) k) x.

End Scal_l.

Lemma Derive_scal_l (f : R → R) (k x : R) :
  Derive (fun x ⇒ f x × k) x = Derive f x × k.

Lemma is_derive_mult :
  ∀ (f g : R → R) (x : R) (df dg : R),
  is_derive f x df →
  is_derive g x dg →
  is_derive (fun t : R ⇒ f t × g t) x (df × g x + f x × dg) .

Lemma ex_derive_mult (f g : R → R) (x : R) :
  ex_derive f x → ex_derive g x
    → ex_derive (fun x : R ⇒ f x × g x) x.

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

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

Lemma ex_derive_pow (f : R → R) (n : nat) (x : R) :
  ex_derive f x → ex_derive (fun x : R ⇒ (f x )^n) x.

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

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

Lemma ex_derive_div (f g : R → R) (x : R) :
  ex_derive f x → ex_derive g x → g x ≠ 0
    → ex_derive (fun y ⇒ f y / g y) x.

Lemma Derive_div (f g : R → R) (x : R) :
  ex_derive f x → ex_derive g x → g x ≠ 0
    → Derive (fun y ⇒ f 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 : K → V) (g : K → K) (x : K) (df : V) (dg : K),
  is_derive f (g x) df →
  is_derive g x dg →
  is_derive (fun x ⇒ f (g x)) x (scal dg df).

Lemma ex_derive_comp :
  ∀ (f : K → V) (g : K → K) (x : K),
  ex_derive f (g x) →
  ex_derive g x →
  ex_derive (fun x ⇒ f (g x)) x.

End Comp.

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

Mean value theorem

Lemma MVT_gen (f : R → R) (a b : R) (df : R → R) :
  let a0 := Rmin a b in
  let b0 := Rmax a b in
  (∀ x, a0 < x < b0 → is_derive f x (df x))
  → (∀ x, a0 ≤ x ≤ b0 → continuity_pt f x )
  → ∃ c, a0 ≤ c ≤ b0 ∧ f b - f a = df c × (b - a ).

Lemma incr_function (f : R → R) (a b : Rbar) (df : R → R) :
  (∀ (x : R), Rbar_lt a x → Rbar_lt x b → is_derive f x (df x))
  → ((∀ (x : R), Rbar_lt a x → Rbar_lt x b → df x > 0)
    → (∀ (x y : R), Rbar_lt a x → x < y → Rbar_lt y b → f x < f y )).

Lemma incr_function_le (f : R → R) (a b : Rbar) (df : R → R) :
  (∀ (x : R), Rbar_le a x → Rbar_le x b → is_derive f x (df x))
  → ((∀ (x : R), Rbar_le a x → Rbar_le x b → df x > 0)
    → (∀ (x y : R), Rbar_le a x → x < y → Rbar_le y b → f x < f y )).

Lemma MVT_cor4:
  ∀ (f df : R → R) a eps,
  (∀ c, Rabs (c - a) ≤ eps → is_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 : R → R) (D : R) (x y : R) :
  (∀ t : R, 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).

Lemma norm_le_prod_norm_1 {K : AbsRing} {U V : NormedModule K} (x : U × V) :
  norm (fst x) ≤ norm x.
Lemma norm_le_prod_norm_2 {K : AbsRing} {U V : NormedModule K} (x : U × V) :
  norm (snd x) ≤ norm x.

Lemma is_derive_filterdiff (f : R → R → R) (x y : R) (dfx : R → R → R) (dfy : R) :
  locally (x ,y ) (fun u : R × R ⇒ is_derive (fun z ⇒ f z (snd u)) (fst u) (dfx (fst u) (snd u))) →
  is_derive (fun z : R ⇒ f x z) y dfy →
  continuous (fun u : R × R ⇒ dfx (fst u) (snd u)) (x ,y ) →
  filterdiff (fun u : R × R ⇒ f (fst u) (snd u)) (locally (x ,y )) (fun u : R × R ⇒ plus (scal (fst u) (dfx x y)) (scal (snd u) dfy)).

Newton integration

Lemma fn_eq_Derive_eq: ∀ f g a b,
  continuity_pt f a → continuity_pt f b →
  continuity_pt g a → continuity_pt g b →
  (∀ x, a < x < b → ex_derive f x ) →
  (∀ x, a < x < b → ex_derive g x ) →
  (∀ x, a < x < b → Derive f x = Derive g x ) →
  ∃ C, ∀ x, a ≤ x ≤ b → f x = g x + C.

Extension

Section ext_cont.

Context {U : UniformSpace}.

Definition extension_cont (f g : R → U) (a x : R) : U :=
  match Rle_dec x a with
    | left _ ⇒ f x
    | right _ ⇒ g x
  end.

Lemma extension_cont_continuous (f g : R → U) (a : R) :
  continuous f a → continuous 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 : R → V) (a : R) (l : V) :
  is_derive f a l → is_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 : R → V) (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 : R → V) (a b : Rbar) :
  ∀ (x : R), Rbar_le a x → Rbar_le x b → (extension_C0 f a b) x = f x.

Lemma extension_C0_continuous (f : R → V) (a b : Rbar) :
  Rbar_le a b
  → (∀ x : R, Rbar_le a x → Rbar_le x b → continuous 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 : R → V) (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 : R → V) (a b : Rbar) :
  ∀ (x : R), Rbar_le a x → Rbar_le x b → (extension_C1 f df a b) x = f x.

Lemma extension_C1_is_derive (f df : R → V) (a b : Rbar) :
  Rbar_le a b
  → (∀ x : R, Rbar_le a x → Rbar_le x b → is_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 : R → R) (a b : Rbar) :
  Rbar_le a b
  → (∀ x : R, Rbar_le a x → Rbar_le x b → ex_derive f x )
  → ∀ x : R, ex_derive (extension_C1 f (Derive f) a b) x.

Section NullDerivative.

Context {V : NormedModule R_AbsRing}.

Lemma eq_is_derive :
  ∀ (f : R → V) (a b : R),
  (∀ t, a ≤ t ≤ b → is_derive f t zero ) →
  a < b → f a = f b.

End NullDerivative.

Iterated differential

Definition

Fixpoint Derive_n (f : R → R) (n : nat) x :=
  match n with
    | O ⇒ f x
    | S n ⇒ Derive (Derive_n f n) x
  end.

Definition ex_derive_n f n x :=
  match n with
  | O ⇒ True
  | S n ⇒ ex_derive (Derive_n f n) x
  end.

Definition is_derive_n f n x l :=
  match n with
  | O ⇒ f x = l
  | S n ⇒ is_derive (Derive_n f n) x l
  end.

Lemma is_derive_n_unique f n x l :
  is_derive_n f n x l → Derive_n f n x = l.

Lemma Derive_n_correct f n x :
  ex_derive_n f n x → is_derive_n f n x (Derive_n f n x).

Extensionality

Lemma Derive_n_ext_loc :
  ∀ f g n x,
  locally x (fun t ⇒ f 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 t ⇒ f t = g t) →
  ex_derive_n f n x → ex_derive_n g n x.

Lemma is_derive_n_ext_loc :
  ∀ f g n x l,
  locally x (fun t ⇒ f t = g t) →
  is_derive_n f n x l → is_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 x → ex_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 l → is_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 : R → R) (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 : R → R) (n : nat) (x : R) :
  Derive_n (fun x ⇒ - f x) n x = - Derive_n f n x.

Lemma ex_derive_n_opp (f : R → R) (n : nat) (x : R) :
  ex_derive_n f n x → ex_derive_n (fun x ⇒ -f x) n x.

Lemma is_derive_n_opp (f : R → R) (n : nat) (x l : R) :
  is_derive_n f n x l → is_derive_n (fun x ⇒ -f x) n x (- l).

Addition of functions

Lemma Derive_n_plus (f g : R → R) (n : nat) (x : R) :
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k y) →
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n g k y) →
  Derive_n (fun x ⇒ f x + g x) n x = Derive_n f n x + Derive_n g n x.

Lemma ex_derive_n_plus (f g : R → R) (n : nat) (x : R) :
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k y) →
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n g k y) →
  ex_derive_n (fun x ⇒ f x + g x) n x.

Lemma is_derive_n_plus (f g : R → R) (n : nat) (x lf lg : R) :
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k y) →
  locally x (fun y ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n g k y) →
  is_derive_n f n x lf → is_derive_n g n x lg →
  is_derive_n (fun x ⇒ f x + g x) n x (lf + lg).

Lemma is_derive_n_iter_plus {I : Type} (l : list I) (f : I → R → R) (n: nat) (x : R) :
  locally x (fun y ⇒ ∀ (j : I) (k : nat), List.In j l → (k ≤ n)%nat → ex_derive_n (f j) k y) →
  is_derive_n (fun y ⇒ iter Rplus 0 l (fun j ⇒ f j y)) n x
    (iter Rplus 0 l (fun j ⇒ Derive_n (f j) n x)).

Lemma ex_derive_n_iter_plus {I : Type} (l : list I) (f : I → R → R) (n: nat) (x : R) :
  locally x (fun y ⇒ ∀ (j : I) (k : nat), List.In j l → (k ≤ n)%nat → ex_derive_n (f j) k y) →
  ex_derive_n (fun y ⇒ iter Rplus 0 l (fun j ⇒ f j y)) n x.

Lemma Derive_n_iter_plus {I : Type} (l : list I) (f : I → R → R) (n: nat) (x : R) :
  locally x (fun y ⇒ ∀ (j : I) (k : nat), List.In j l → (k ≤ n)%nat → ex_derive_n (f j) k y) →
  Derive_n (fun y ⇒ iter Rplus 0 l (fun j ⇒ f j y)) n x =
    iter Rplus 0 l (fun j ⇒ Derive_n (f j) n x).

Lemma is_derive_n_sum_n_m n m (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (n ≤ l ≤ m)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  is_derive_n (fun y ⇒ sum_n_m (fun j ⇒ f j y) n m) k x
    (sum_n_m (fun j ⇒ Derive_n (f j) k x) n m).
Lemma ex_derive_n_sum_n_m n m (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (n ≤ l ≤ m)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  ex_derive_n (fun y ⇒ sum_n_m (fun j ⇒ f j y) n m) k x.
Lemma Derive_n_sum_n_m n m (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (n ≤ l ≤ m)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  Derive_n (fun y ⇒ sum_n_m (fun j ⇒ f j y) n m) k x
    = sum_n_m (fun j ⇒ Derive_n (f j) k x) n m.

Lemma is_derive_n_sum_n n (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (l ≤ n)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  is_derive_n (fun y ⇒ sum_n (fun j ⇒ f j y) n) k x
    (sum_n (fun j ⇒ Derive_n (f j) k x) n).
Lemma ex_derive_n_sum_n n (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (l ≤ n)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  ex_derive_n (fun y ⇒ sum_n (fun j ⇒ f j y) n) k x.
Lemma Derive_n_sum_n n (f : nat → R → R) (k: nat) (x : R) :
  locally x (fun t ⇒ ∀ l j , (l ≤ n)%nat →(j ≤ k)%nat → ex_derive_n (f l) j t) →
  Derive_n (fun y ⇒ sum_n (fun j ⇒ f j y) n) k x =
    (sum_n (fun j ⇒ Derive_n (f j) k x) n ).

Subtraction of functions

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

Multiplicative operators

Scalar multiplication

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

Lemma ex_derive_n_scal_l (f : R → R) (n : nat) (a x : R) :
  ex_derive_n f n x → ex_derive_n (fun y ⇒ a × f y) n x.

Lemma is_derive_n_scal_l (f : R → R) (n : nat) (a x l : R) :
  is_derive_n f n x l → is_derive_n (fun y ⇒ a × f y) n x (a × l).

Lemma Derive_n_scal_r (f : R → R) (n : nat) (a x : R) :
  Derive_n (fun y ⇒ f y × a) n x = Derive_n f n x × a.
Lemma ex_derive_n_scal_r (f : R → R) (n : nat) (a x : R) :
  ex_derive_n f n x → ex_derive_n (fun y ⇒ f y × a) n x.
Lemma is_derive_n_scal_r (f : R → R) (n : nat) (a x l : R) :
  is_derive_n f n x l → is_derive_n (fun y ⇒ f y × a) n x (l × a).

Composition

Composition with linear functions

Lemma Derive_n_comp_scal (f : R → R) (a : R) (n : nat) (x : R) :
  locally (a × x) (fun x ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k x) →
  Derive_n (fun y ⇒ f (a × y)) n x = (a ^ n × Derive_n f n (a × x)).

Lemma ex_derive_n_comp_scal (f : R → R) (a : R) (n : nat) (x : R) :
  locally (a × x) (fun x ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k x)
  → ex_derive_n (fun y ⇒ f (a × y)) n x.

Lemma is_derive_n_comp_scal (f : R → R) (a : R) (n : nat) (x l : R) :
  locally (a × x) (fun x ⇒ ∀ k, (k ≤ n)%nat → ex_derive_n f k x)
  → is_derive_n f n (a × x) l
  → is_derive_n (fun y ⇒ f (a × y)) n x (a ^ n × l).

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

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

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

Lemma is_derive_n_comp_trans (f : R → R) (n : nat) (x b l : R) :
  is_derive_n f n (x + b) l →
  is_derive_n (fun y ⇒ f (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)%nat → ex_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.