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-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 mathcomp.ssreflect.ssreflect.
Require Import Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries.
Require Import Lim_seq RInt_analysis.

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 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.

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))).

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).

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.

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).