Library Coquelicot.ElemFct

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 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 x ⇒ Rabs (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 x ⇒ f x ≠ 0)
    → filterlim (fun x ⇒ Rabs (f x)) (Rbar_locally' x) (at_right 0).

Lemma filterdiff_Rabs (x : R) :
  x ≠ 0 → filterdiff Rabs (locally x) (fun y : R ⇒ scal y (sign x)).
Lemma is_derive_Rabs (f : R → R) (x df : R) :
  is_derive f x df → f x ≠ 0
    → is_derive (fun x ⇒ Rabs (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 x ⇒ f 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 x ⇒ sqrt (f x)) x p_infty.

Lemma filterdiff_sqrt (x : R) :
  0 < x → filterdiff sqrt (locally x) (fun y ⇒ scal 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 x ⇒ sqrt (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 : K ⇒ mult (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 : K ⇒ pow_n y n) (locally x)
    (fun y : K ⇒ scal 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 : R ⇒ x ^ 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 : R ⇒ x ^ 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 : R ⇒ x ^ p) i x 0.
Lemma Derive_n_pow_bigi: ∀ i p x, (p < i) %nat →
                         Derive_n (fun x : R ⇒ x ^ p) i x = 0.

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

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

Lemma is_RInt_pow :
  ∀ a b n,
  is_RInt (fun x ⇒ pow 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 k ⇒ x ^k / INR (fact k)) n ≤ exp x.

Definition

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.

Limits

Lemma is_lim_exp_p : is_lim (fun y ⇒ exp y) p_infty p_infty.
Lemma is_lim_exp_m : is_lim (fun y ⇒ exp y) m_infty 0.

Lemma ex_lim_exp (x : Rbar) : ex_lim (fun y ⇒ exp y) x.
Lemma Lim_exp (x : Rbar) :
  Lim (fun y ⇒ exp y) x =
    match x with
      | Finite x ⇒ exp x
      | p_infty ⇒ p_infty
      | m_infty ⇒ 0
    end.

Lemma is_lim_div_exp_p : is_lim (fun y ⇒ exp y / y) p_infty p_infty.

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

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

Integral

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 y ⇒ ln 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 y ⇒ ln y / y) p_infty 0.

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

Unnormalized sinc

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

ArcTan

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