Library Coquelicot.ElemFct
This file is part of the Coquelicot formalization of real
analysis in Coq: http://coquelicot.saclay.inria.fr/
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.
Copyright (C) 2011-2015 Catherine Lelay
Copyright (C) 2011-2020 Guillaume Melquiond
From Coq Require Import Reals Lia ssreflect.
Require Import Rbar Rcomplements Continuity Derive Hierarchy RInt PSeries 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 continuous_Rabs_comp f (x : R) :
continuous f x → continuous (fun x0 ⇒ Rabs (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 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).
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.
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.
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))).
Lemma continuous_sqrt (x : R) : continuous sqrt x.
Lemma continuous_sqrt_comp (f : R → R) x:
continuous f x →
continuous (fun x ⇒ sqrt (f x)) x.
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)).
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
Continuity
Lemma continuous_exp x : continuous exp x.
Lemma continuous_exp_comp (f : R → R) x:
continuous f x →
continuous (fun x ⇒ exp (f x)) x.
Derivative
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).
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.
Lemma continuous_ln x : (0 < x) → continuous ln x.
Lemma is_derive_ln x :
0 < x → is_derive ln x (/ x)%R.
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 x ⇒ atan (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 x ⇒ cos (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 x ⇒ sin (f x)) x.
Lemma is_derive_sin x : is_derive sin x (cos x).