Library Coq.Reals.Ranalysis1


Require Import Rbase.
Require Import Rfunctions.
Require Export Rlimit.
Require Export Rderiv.
Local Open Scope R_scope.
Implicit Type f : R -> R.

Basic operations on functions

Definition plus_fct f1 f2 (x:R) : R := f1 x + f2 x.
Definition opp_fct f (x:R) : R := - f x.
Definition mult_fct f1 f2 (x:R) : R := f1 x * f2 x.
Definition mult_real_fct (a:R) f (x:R) : R := a * f x.
Definition minus_fct f1 f2 (x:R) : R := f1 x - f2 x.
Definition div_fct f1 f2 (x:R) : R := f1 x / f2 x.
Definition div_real_fct (a:R) f (x:R) : R := a / f x.
Definition comp f1 f2 (x:R) : R := f1 (f2 x).
Definition inv_fct f (x:R) : R := / f x.
Definition mirr_fct f (x:R) : R := f (- x).

Declare Scope Rfun_scope.
Delimit Scope Rfun_scope with F.

Arguments plus_fct (f1 f2)%F x%R.
Arguments mult_fct (f1 f2)%F x%R.
Arguments minus_fct (f1 f2)%F x%R.
Arguments div_fct (f1 f2)%F x%R.
Arguments inv_fct f%F x%R.
Arguments opp_fct f%F x%R.
Arguments mult_real_fct a%R f%F x%R.
Arguments div_real_fct a%R f%F x%R.
Arguments comp (f1 f2)%F x%R.
Arguments mirr_fct f%F x%R.

Infix "+" := plus_fct : Rfun_scope.
Notation "- x" := (opp_fct x) : Rfun_scope.
Infix "*" := mult_fct : Rfun_scope.
Infix "-" := minus_fct : Rfun_scope.
Infix "/" := div_fct : Rfun_scope.
Notation "/ x" := (inv_fct x) : Rfun_scope.

Definition fct_cte (a x:R) : R := a.
Definition id (x:R) := x.

Variations of functions

Definition increasing f : Prop := forall x y:R, x <= y -> f x <= f y.
Definition decreasing f : Prop := forall x y:R, x <= y -> f y <= f x.
Definition strict_increasing f : Prop := forall x y:R, x < y -> f x < f y.
Definition strict_decreasing f : Prop := forall x y:R, x < y -> f y < f x.
Definition constant f : Prop := forall x y:R, f x = f y.

Definition no_cond (x:R) : Prop := True.

Definition constant_D_eq f (D:R -> Prop) (c:R) : Prop :=
  forall x:R, D x -> f x = c.

Definition of continuity as a limit

Definition continuity_pt f (x0:R) : Prop := continue_in f no_cond x0.
Definition continuity f : Prop := forall x:R, continuity_pt f x.

Arguments continuity_pt f%F x0%R.
Arguments continuity f%F.

Lemma continuity_pt_locally_ext :
  forall f g a x, 0 < a -> (forall y, Rdist y x < a -> f y = g y) ->
  continuity_pt f x -> continuity_pt g x.

Lemma continuity_pt_plus :
  forall f1 f2 (x0:R),
    continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 + f2) x0.

Lemma continuity_pt_opp :
  forall f (x0:R), continuity_pt f x0 -> continuity_pt (- f) x0.

Lemma continuity_pt_minus :
  forall f1 f2 (x0:R),
    continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 - f2) x0.

Lemma continuity_pt_mult :
  forall f1 f2 (x0:R),
    continuity_pt f1 x0 -> continuity_pt f2 x0 -> continuity_pt (f1 * f2) x0.

Lemma continuity_pt_const : forall f (x0:R), constant f -> continuity_pt f x0.

Lemma continuity_pt_scal :
  forall f (a x0:R),
    continuity_pt f x0 -> continuity_pt (mult_real_fct a f) x0.

Lemma continuity_pt_inv :
  forall f (x0:R), continuity_pt f x0 -> f x0 <> 0 -> continuity_pt (/ f) x0.

Lemma div_eq_inv : forall f1 f2, (f1 / f2)%F = (f1 * / f2)%F.

Lemma continuity_pt_div :
  forall f1 f2 (x0:R),
    continuity_pt f1 x0 ->
    continuity_pt f2 x0 -> f2 x0 <> 0 -> continuity_pt (f1 / f2) x0.

Lemma continuity_pt_comp :
  forall f1 f2 (x:R),
    continuity_pt f1 x -> continuity_pt f2 (f1 x) -> continuity_pt (f2 o f1) x.

Lemma continuity_plus :
  forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 + f2).

Lemma continuity_opp : forall f, continuity f -> continuity (- f).

Lemma continuity_minus :
  forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 - f2).

Lemma continuity_mult :
  forall f1 f2, continuity f1 -> continuity f2 -> continuity (f1 * f2).

Lemma continuity_const : forall f, constant f -> continuity f.

Lemma continuity_scal :
  forall f (a:R), continuity f -> continuity (mult_real_fct a f).

Lemma continuity_inv :
  forall f, continuity f -> (forall x:R, f x <> 0) -> continuity (/ f).

Lemma continuity_div :
  forall f1 f2,
    continuity f1 ->
    continuity f2 -> (forall x:R, f2 x <> 0) -> continuity (f1 / f2).

Lemma continuity_comp :
  forall f1 f2, continuity f1 -> continuity f2 -> continuity (f2 o f1).

Derivative's definition using Landau's kernel


Definition derivable_pt_lim f (x l:R) : Prop :=
  forall eps:R,
    0 < eps ->
    exists delta : posreal,
      (forall h:R,
        h <> 0 -> Rabs h < delta -> Rabs ((f (x + h) - f x) / h - l) < eps).

Definition derivable_pt_abs f (x l:R) : Prop := derivable_pt_lim f x l.

Definition derivable_pt f (x:R) := { l:R | derivable_pt_abs f x l }.
Definition derivable f := forall x:R, derivable_pt f x.

Definition derive_pt f (x:R) (pr:derivable_pt f x) := proj1_sig pr.
Definition derive f (pr:derivable f) (x:R) := derive_pt f x (pr x).

Arguments derivable_pt_lim f%F x%R l.
Arguments derivable_pt_abs f%F (x l)%R.
Arguments derivable_pt f%F x%R.
Arguments derivable f%F.
Arguments derive_pt f%F x%R pr.
Arguments derive f%F pr x.

Definition antiderivative f (g:R -> R) (a b:R) : Prop :=
  (forall x:R,
    a <= x <= b -> exists pr : derivable_pt g x, f x = derive_pt g x pr) /\
  a <= b.

Class of differential functions

Record Differential : Type := mkDifferential
  {d1 :> R -> R; cond_diff : derivable d1}.

Record Differential_D2 : Type := mkDifferential_D2
  {d2 :> R -> R;
    cond_D1 : derivable d2;
    cond_D2 : derivable (derive d2 cond_D1)}.

Lemma uniqueness_step1 :
  forall f (x l1 l2:R),
    limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l1 0 ->
    limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l2 0 ->
    l1 = l2.

Lemma uniqueness_step2 :
  forall f (x l:R),
    derivable_pt_lim f x l ->
    limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0.

Lemma uniqueness_step3 :
  forall f (x l:R),
    limit1_in (fun h:R => (f (x + h) - f x) / h) (fun h:R => h <> 0) l 0 ->
    derivable_pt_lim f x l.

Lemma uniqueness_limite :
  forall f (x l1 l2:R),
    derivable_pt_lim f x l1 -> derivable_pt_lim f x l2 -> l1 = l2.

Lemma derive_pt_eq :
  forall f (x l:R) (pr:derivable_pt f x),
    derive_pt f x pr = l <-> derivable_pt_lim f x l.

Lemma derive_pt_eq_0 :
  forall f (x l:R) (pr:derivable_pt f x),
    derivable_pt_lim f x l -> derive_pt f x pr = l.

Lemma derive_pt_eq_1 :
  forall f (x l:R) (pr:derivable_pt f x),
    derive_pt f x pr = l -> derivable_pt_lim f x l.

Equivalence of this definition with the one using limit concept

Lemma derive_pt_D_in :
  forall f (df:R -> R) (x:R) (pr:derivable_pt f x),
    D_in f df no_cond x <-> derive_pt f x pr = df x.

Lemma derivable_pt_lim_D_in :
  forall f (df:R -> R) (x:R),
    D_in f df no_cond x <-> derivable_pt_lim f x (df x).


Lemma derivable_pt_lim_ext : forall f g x l, (forall z, f z = g z) ->
  derivable_pt_lim f x l -> derivable_pt_lim g x l.


Lemma derivable_pt_lim_locally_ext : forall f g x a b l,
  a < x < b ->
  (forall z, a < z < b -> f z = g z) ->
  derivable_pt_lim f x l -> derivable_pt_lim g x l.

derivability -> continuity

Lemma derivable_derive :
  forall f (x:R) (pr:derivable_pt f x), exists l : R, derive_pt f x pr = l.

Theorem derivable_continuous_pt :
  forall f (x:R), derivable_pt f x -> continuity_pt f x.

Theorem derivable_continuous : forall f, derivable f -> continuity f.

Main rules

Rules for derivable_pt_lim (value of the derivative at a point)


Lemma derivable_pt_lim_id : forall x:R, derivable_pt_lim id x 1.

Lemma derivable_pt_lim_comp :
  forall f1 f2 (x l1 l2:R),
    derivable_pt_lim f1 x l1 ->
    derivable_pt_lim f2 (f1 x) l2 -> derivable_pt_lim (f2 o f1) x (l2 * l1).

Lemma derivable_pt_lim_opp :
  forall f (x l:R), derivable_pt_lim f x l -> derivable_pt_lim (- f) x (- l).

Lemma derivable_pt_lim_opp_fwd :
  forall f (x l:R), derivable_pt_lim f x (- l) -> derivable_pt_lim (- f) x l.

Lemma derivable_pt_lim_opp_rev :
  forall f (x l:R), derivable_pt_lim (- f) x (- l) -> derivable_pt_lim f x l.

Lemma derivable_pt_lim_mirr_fwd :
  forall f (x l:R), derivable_pt_lim f (- x) (- l) -> derivable_pt_lim (mirr_fct f) x l.

Lemma derivable_pt_lim_mirr_rev :
  forall f (x l:R), derivable_pt_lim (mirr_fct f) (- x) (- l) -> derivable_pt_lim f x l.

Lemma derivable_pt_lim_plus :
  forall f1 f2 (x l1 l2:R),
    derivable_pt_lim f1 x l1 ->
    derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 + f2) x (l1 + l2).

Lemma derivable_pt_lim_minus :
  forall f1 f2 (x l1 l2:R),
    derivable_pt_lim f1 x l1 ->
    derivable_pt_lim f2 x l2 -> derivable_pt_lim (f1 - f2) x (l1 - l2).

Lemma derivable_pt_lim_mult :
  forall f1 f2 (x l1 l2:R),
    derivable_pt_lim f1 x l1 ->
    derivable_pt_lim f2 x l2 ->
    derivable_pt_lim (f1 * f2) x (l1 * f2 x + f1 x * l2).

Lemma derivable_pt_lim_const : forall a x:R, derivable_pt_lim (fct_cte a) x 0.

Lemma derivable_pt_lim_scal :
  forall f (a x l:R),
    derivable_pt_lim f x l -> derivable_pt_lim (mult_real_fct a f) x (a * l).

Lemma derivable_pt_lim_div_scal :
  forall f x l a, derivable_pt_lim f x l ->
     derivable_pt_lim (fun y => f y / a) x (l / a).

Lemma derivable_pt_lim_scal_right :
  forall f x l a, derivable_pt_lim f x l ->
     derivable_pt_lim (fun y => f y * a) x (l * a).

Lemma derivable_pt_lim_Rsqr : forall x:R, derivable_pt_lim Rsqr x (2 * x).

Rules for derivable_pt (derivability at a point)


Lemma derivable_pt_id : forall x:R, derivable_pt id x.

Lemma derivable_pt_comp :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 (f1 x) -> derivable_pt (f2 o f1) x.

Lemma derivable_pt_xeq:
  forall (f : R -> R) (x1 x2 : R), x1=x2 -> derivable_pt f x1 -> derivable_pt f x2.

Lemma derivable_pt_opp :
  forall (f : R -> R) (x:R), derivable_pt f x -> derivable_pt (- f) x.

Lemma derivable_pt_opp_rev:
  forall (f : R -> R) (x : R), derivable_pt (- f) x -> derivable_pt f x.

Lemma derivable_pt_mirr:
  forall (f : R -> R) (x : R), derivable_pt f (-x) -> derivable_pt (mirr_fct f) x.

Lemma derivable_pt_mirr_rev:
  forall (f : R -> R) (x : R), derivable_pt (mirr_fct f) (- x) -> derivable_pt f x.

Lemma derivable_pt_mirr_prem:
  forall (f : R -> R) (x : R), derivable_pt (mirr_fct f) x -> derivable_pt f (-x).

Lemma derivable_pt_plus :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 + f2) x.

Lemma derivable_pt_minus :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 - f2) x.

Lemma derivable_pt_mult :
  forall f1 f2 (x:R),
    derivable_pt f1 x -> derivable_pt f2 x -> derivable_pt (f1 * f2) x.

Lemma derivable_pt_const : forall a x:R, derivable_pt (fct_cte a) x.

Lemma derivable_pt_scal :
  forall f (a x:R), derivable_pt f x -> derivable_pt (mult_real_fct a f) x.

Lemma derivable_pt_Rsqr : forall x:R, derivable_pt Rsqr x.

Rules for derivable (derivability on whole domain)


Lemma derivable_id : derivable id.

Lemma derivable_comp :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f2 o f1).

Lemma derivable_opp : forall f, derivable f -> derivable (- f).

Lemma derivable_mirr : forall f, derivable f -> derivable (mirr_fct f).

Lemma derivable_plus :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 + f2).

Lemma derivable_minus :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 - f2).

Lemma derivable_mult :
  forall f1 f2, derivable f1 -> derivable f2 -> derivable (f1 * f2).

Lemma derivable_const : forall a:R, derivable (fct_cte a).

Lemma derivable_scal :
  forall f (a:R), derivable f -> derivable (mult_real_fct a f).

Lemma derivable_Rsqr : derivable Rsqr.

Rules for derive_pt (derivative function on whole domain)


Lemma derive_pt_id : forall x:R, derive_pt id x (derivable_pt_id _) = 1.

Lemma derive_pt_comp :
  forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 (f1 x)),
    derive_pt (f2 o f1) x (derivable_pt_comp _ _ _ pr1 pr2) =
    derive_pt f2 (f1 x) pr2 * derive_pt f1 x pr1.

Lemma derive_pt_opp :
  forall f (x:R) (pr1:derivable_pt f x),
    derive_pt (- f) x (derivable_pt_opp _ _ pr1) = - derive_pt f x pr1.

Lemma derive_pt_opp_rev :
  forall f (x:R) (pr1:derivable_pt (- f) x),
    derive_pt (- f) x pr1 = - derive_pt f x (derivable_pt_opp_rev _ _ pr1).

Lemma derive_pt_mirr :
  forall f (x:R) (pr1:derivable_pt f (-x)),
    derive_pt (mirr_fct f) x (derivable_pt_mirr _ _ pr1) = - derive_pt f (-x) pr1.

Lemma derive_pt_mirr_rev :
  forall f (x:R) (pr1:derivable_pt (mirr_fct f) x),
    derive_pt (mirr_fct f) x pr1 = - derive_pt f (-x) (derivable_pt_mirr_prem f x pr1).

Lemma derive_pt_plus :
  forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
    derive_pt (f1 + f2) x (derivable_pt_plus _ _ _ pr1 pr2) =
    derive_pt f1 x pr1 + derive_pt f2 x pr2.

Lemma derive_pt_minus :
  forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
    derive_pt (f1 - f2) x (derivable_pt_minus _ _ _ pr1 pr2) =
    derive_pt f1 x pr1 - derive_pt f2 x pr2.

Lemma derive_pt_mult :
  forall f1 f2 (x:R) (pr1:derivable_pt f1 x) (pr2:derivable_pt f2 x),
    derive_pt (f1 * f2) x (derivable_pt_mult _ _ _ pr1 pr2) =
    derive_pt f1 x pr1 * f2 x + f1 x * derive_pt f2 x pr2.

Lemma derive_pt_const :
  forall a x:R, derive_pt (fct_cte a) x (derivable_pt_const a x) = 0.

Lemma derive_pt_scal :
  forall f (a x:R) (pr:derivable_pt f x),
    derive_pt (mult_real_fct a f) x (derivable_pt_scal _ _ _ pr) =
    a * derive_pt f x pr.

Lemma derive_pt_Rsqr :
  forall x:R, derive_pt Rsqr x (derivable_pt_Rsqr _) = 2 * x.

Definition and derivative of power function with natural number exponent


Definition pow_fct (n:nat) (y:R) : R := y ^ n.

Lemma derivable_pt_lim_pow_pos :
  forall (x:R) (n:nat),
    (0 < n)%nat -> derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).

Lemma derivable_pt_lim_pow :
  forall (x:R) (n:nat),
    derivable_pt_lim (fun y:R => y ^ n) x (INR n * x ^ pred n).

Lemma derivable_pt_pow :
  forall (n:nat) (x:R), derivable_pt (fun y:R => y ^ n) x.

Lemma derivable_pow : forall n:nat, derivable (fun y:R => y ^ n).

Lemma derive_pt_pow :
  forall (n:nat) (x:R),
    derive_pt (fun y:R => y ^ n) x (derivable_pt_pow n x) = INR n * x ^ pred n.

Irrelevance of derivability proof for derivative


Lemma pr_nu :
  forall f (x:R) (pr1 pr2:derivable_pt f x),
    derive_pt f x pr1 = derive_pt f x pr2.

In dependently typed environments it is sometimes hard to rewrite. Having pr_nu for separate x with a proof that they are equal helps.

Lemma pr_nu_xeq :
  forall f (x1 x2:R) (pr1:derivable_pt f x1) (pr2:derivable_pt f x2),
    x1 = x2 -> derive_pt f x1 pr1 = derive_pt f x2 pr2.

Local extremum's condition


Theorem deriv_maximum :
  forall f (a b c:R) (pr:derivable_pt f c),
    a < c ->
    c < b ->
    (forall x:R, a < x -> x < b -> f x <= f c) -> derive_pt f c pr = 0.

Theorem deriv_minimum :
  forall f (a b c:R) (pr:derivable_pt f c),
    a < c ->
    c < b ->
    (forall x:R, a < x -> x < b -> f c <= f x) -> derive_pt f c pr = 0.

Theorem deriv_constant2 :
  forall f (a b c:R) (pr:derivable_pt f c),
    a < c ->
    c < b -> (forall x:R, a < x -> x < b -> f x = f c) -> derive_pt f c pr = 0.

Lemma nonneg_derivative_0 :
  forall f (pr:derivable f),
    increasing f -> forall x:R, 0 <= derive_pt f x (pr x).