Library Coquelicot.ElemFct

This file is part of the Coquelicot formalization of real analysis in Coq:
Copyright (C) 2011-2015 Sylvie Boldo
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2020 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.
This file describes basic properties (such as limits or differentiability) about basic functions: absolute value, inverse, square root, power, exponential and so on.

Absolute value

in an AbsRing

Lemma continuous_abs {K : AbsRing} (x : K) :
  continuous abs x.

Lemma filterlim_abs_0 {K : AbsRing} :
  ( x : K, abs x = 0 x = zero)
  filterlim (abs (K := K)) (locally' (zero (G := K))) (at_right 0).

in R

Lemma continuous_Rabs (x : R) :
  continuous Rabs x.

Lemma continuous_Rabs_comp f (x : R) :
  continuous f x continuous (fun x0Rabs (f x0)) x.

Lemma filterlim_Rabs (x : Rbar) :
  filterlim Rabs (Rbar_locally' x) (Rbar_locally (Rbar_abs x)).

Lemma is_lim_Rabs (f : R R) (x l : Rbar) :
  is_lim f x l is_lim (fun xRabs (f x)) x (Rbar_abs l).

Lemma filterlim_Rabs_0 :
  filterlim Rabs (Rbar_locally' 0) (at_right 0).

Lemma is_lim_Rabs_0 (f : R R) (x : Rbar) :
  is_lim f x 0 Rbar_locally' x (fun xf x 0)
     filterlim (fun xRabs (f x)) (Rbar_locally' x) (at_right 0).

Lemma filterdiff_Rabs (x : R) :
  x 0 filterdiff Rabs (locally x) (fun y : Rscal y (sign x)).

Lemma is_derive_Rabs (f : R R) (x df : R) :
  is_derive f x df f x 0
     is_derive (fun xRabs (f x)) x (sign (f x) × df).

Inverse function

Lemma filterlim_Rinv_0_right :
  filterlim Rinv (at_right 0) (Rbar_locally p_infty).

Lemma is_lim_Rinv_0_right (f : R R) (x : Rbar) :
  is_lim f x 0 Rbar_locally' x (fun x ⇒ 0 < f x)
  is_lim (fun x/ (f x)) x p_infty.

Lemma filterlim_Rinv_0_left :
  filterlim Rinv (at_left 0) (Rbar_locally m_infty).

Lemma is_lim_Rinv_0_left (f : R R) (x : Rbar) :
  is_lim f x 0 Rbar_locally' x (fun xf x < 0)
  is_lim (fun x/ (f x)) x m_infty.

Lemma continuous_Rinv x :
  x 0
  continuous (fun x/ x) x.

Lemma continuous_Rinv_comp (f : R R) x:
  continuous f x
  f x 0
  continuous (fun x/ (f x)) x.

Square root function

Lemma filterlim_sqrt_p : filterlim sqrt (Rbar_locally' p_infty) (Rbar_locally p_infty).

Lemma is_lim_sqrt_p (f : R R) (x : Rbar) :
  is_lim f x p_infty
   is_lim (fun xsqrt (f x)) x p_infty.

Lemma filterdiff_sqrt (x : R) :
  0 < x filterdiff sqrt (locally x) (fun yscal y (/ (2 × sqrt x))).

Lemma is_derive_sqrt (f : R R) (x df : R) :
  is_derive f x df 0 < f x
   is_derive (fun xsqrt (f x)) x (df / (2 × sqrt (f x))).

Lemma continuous_sqrt (x : R) : continuous sqrt x.

Lemma continuous_sqrt_comp (f : R R) x:
  continuous f x
  continuous (fun xsqrt (f x)) x.

Power function

Section nat_to_ring.

Context {K : Ring}.

Definition nat_to_ring (n : nat) : K :=
  sum_n_m (fun _one) 1 n.

Lemma nat_to_ring_O :
  nat_to_ring O = zero.

Lemma nat_to_ring_Sn (n : nat) :
  nat_to_ring (S n) = plus (nat_to_ring n) one.

End nat_to_ring.

Section is_derive_mult.

Context {K : AbsRing}.

Lemma is_derive_mult (f g : K K) x (df dg : K) :
  is_derive f x df is_derive g x dg
   ( n m : K, mult n m = mult m n)
   is_derive (fun x : Kmult (f x) (g x)) x (plus (mult df (g x)) (mult (f x) dg)).

End is_derive_mult.

Lemma filterdiff_pow_n {K : AbsRing} (x : K) (n : nat) :
  ( a b : K, mult a b = mult b a)
   filterdiff (fun y : Kpow_n y n) (locally x)
    (fun y : Kscal y (mult (nat_to_ring n) (pow_n x (pred n)))).

Lemma is_derive_n_pow_smalli: i p x, (i p)%nat
  is_derive_n (fun x : Rx ^ p) i x
    (INR (fact p) / INR (fact (p - i)%nat) × x ^ (p - i)%nat).

Lemma Derive_n_pow_smalli: i p x, (i p)%nat
  Derive_n (fun x : Rx ^ p) i x
    = INR (fact p) / INR (fact (p - i)%nat) × x ^ (p - i)%nat.

Lemma is_derive_n_pow_bigi: i p x, (p < i) %nat
                         is_derive_n (fun x : Rx ^ p) i x 0.

Lemma Derive_n_pow_bigi: i p x, (p < i) %nat
                         Derive_n (fun x : Rx ^ p) i x = 0.

Lemma Derive_n_pow i p x:
  Derive_n (fun x : Rx ^ p) i x =
    match (le_dec i p) with
    | left _INR (fact p) / INR (fact (p -i)%nat) × x ^ (p - i)%nat
    | right _ ⇒ 0

Lemma ex_derive_n_pow i p x: ex_derive_n (fun x : Rx ^ p) i x.

Lemma is_RInt_pow :
   a b n,
  is_RInt (fun xpow x n) a b (pow b (S n) / INR (S n) - pow a (S n) / INR (S n)).

Exponential function

Lemma exp_ge_taylor (x : R) (n : nat) :
  0 x sum_f_R0 (fun kx^k / INR (fact k)) n exp x.


Lemma is_exp_Reals (x : R) :
  is_pseries (fun n/ INR (fact n)) x (exp x).

Lemma exp_Reals (x : R) :
  exp x = PSeries (fun n/ INR (fact n)) x.


Lemma is_lim_exp_p : is_lim (fun yexp y) p_infty p_infty.

Lemma is_lim_exp_m : is_lim (fun yexp y) m_infty 0.

Lemma ex_lim_exp (x : Rbar) : ex_lim (fun yexp y) x.

Lemma Lim_exp (x : Rbar) :
  Lim (fun yexp y) x =
    match x with
      | Finite xexp x
      | p_inftyp_infty
      | m_infty ⇒ 0

Lemma is_lim_div_exp_p : is_lim (fun yexp y / y) p_infty p_infty.

Lemma is_lim_mul_exp_m : is_lim (fun yy × exp y) m_infty 0.

Lemma is_lim_div_expm1_0 : is_lim (fun y(exp y - 1) / y) 0 1.


Lemma is_RInt_exp :
   a b,
  is_RInt exp a b (exp b - exp a).


Lemma continuous_exp x : continuous exp x.

Lemma continuous_exp_comp (f : R R) x:
  continuous f x
  continuous (fun xexp (f x)) x.


Lemma is_derive_exp : x, is_derive exp x (exp x).

Lemma is_derive_n_exp : n x, is_derive_n exp n x (exp x).

Natural logarithm

Lemma is_lim_ln_p : is_lim (fun yln y) p_infty p_infty.

Lemma is_lim_ln_0 :
  filterlim ln (at_right 0) (Rbar_locally m_infty).

Lemma is_lim_div_ln_p : is_lim (fun yln y / y) p_infty 0.

Lemma is_lim_div_ln1p_0 : is_lim (fun yln (1+y) / y) 0 1.

Lemma continuous_ln x : (0 < x) continuous ln x.

Lemma is_derive_ln x :
  0 < x is_derive ln x (/ x)%R.

Unnormalized sinc

Lemma is_lim_sinc_0 : is_lim (fun xsin x / x) 0 1.


Lemma CV_radius_atan : CV_radius (fun n(-1)^n / (INR (S (n + n)))) = 1.

Lemma atan_Reals (x : R) : Rabs x < 1
   atan x = x × PSeries (fun n(-1)^n / (INR (S (n + n)))) (x ^ 2).

Lemma continuous_atan x : continuous atan x.

Lemma continuous_atan_comp (f : R R) x:
  continuous f x
  continuous (fun xatan (f x)) x.

Lemma is_derive_atan x :
  is_derive atan x (/ (1 + x²)).


Lemma continuous_cos x : continuous cos x.

Lemma continuous_cos_comp (f : R R) x:
  continuous f x
  continuous (fun xcos (f x)) x.

Lemma is_derive_cos x : is_derive cos x (- sin x).


Lemma continuous_sin x : continuous sin x.

Lemma continuous_sin_comp (f : R R) x:
  continuous f x
  continuous (fun xsin (f x)) x.

Lemma is_derive_sin x : is_derive sin x (cos x).


Lemma continuous_tan x : cos x 0 continuous tan x.

Lemma is_derive_tan x :
  cos x 0%R is_derive tan x (tan x ^ 2 + 1)%R.