Library Interval.Missing.Coquelicot
This file is part of the Coq.Interval library for proving bounds of
real-valued expressions in Coq: https://coqinterval.gitlabpages.inria.fr/
Copyright (C) 2015-2016, Inria.
Copyright (C) 2015-2016, IRIT.
This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
From Coq Require Import Reals Psatz.
From Coquelicot Require Import Coquelicot.
From mathcomp.ssreflect Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop.
Require Import Stdlib.
Require Import MathComp.
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 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 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 continuous_tan x : cos x ≠ 0 → continuous tan x.
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 continuous_exp x : continuous exp x.
Lemma continuous_exp_comp (f : R → R) x:
continuous f x →
continuous (fun x ⇒ exp (f x)) 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.
Lemma continuous_ln x : (0 < x) → continuous ln x.
Lemma continuous_Rabs_comp f (x : R) :
continuous f x → continuous (fun x0 ⇒ Rabs (f x0)) x.
Lemma is_RInt_translation_add V g a b x Ig :
@is_RInt V g (a + x) (b + x) Ig →
is_RInt (fun y : R ⇒ g (y + x)%R) a b Ig.
Lemma is_RInt_translation_sub V g x a b Ig :
@is_RInt V g (a - x) (b - x) Ig →
is_RInt (fun y : R ⇒ g (y - x)) a b Ig.
Lemma ex_RInt_translation_add V g x a b :
@ex_RInt V g a b → @ex_RInt V (fun t ⇒ g (t + x)) (a - x) (b - x).
Lemma ex_RInt_translation_sub V g a b x :
@ex_RInt V g a b → @ex_RInt V (fun t ⇒ g (t - x)) (a + x) (b + x).
Lemma RInt_translation_add V g a b x :
ex_RInt g (a + x) (b + x) →
@RInt V (fun y : R ⇒ g (y + x)%R) a b = RInt g (a + x) (b + x).
Lemma RInt_translation_sub V g a b x :
ex_RInt g (a - x) (b - x) →
@RInt V (fun y : R ⇒ g (y - x)%R) a b = RInt g (a - x) (b - x).
Lemma ball_to_lra a y eps : ball a eps y ↔ a - eps < y < a + eps.
Lemma Derive_nS f n :
Derive_n f n.+1 = Derive_n (Derive f) n.
Lemma ex_derive_nSS f n :
ex_derive_n f n.+2 = ex_derive_n (Derive f) n.+1.
Lemma ex_derive_n_is_derive_n :
∀ f n x l, is_derive_n f n x l → ex_derive_n f n x.
Lemma ex_derive_is_derive :
∀ (f : R → R) x l, is_derive f x l → ex_derive f x.
Lemma is_derive_ext_alt f g x (f' : R → R) (P : R → Prop) :
P x →
open P →
(∀ t : R, P t → f t = g t) →
(∀ t : R, P t → is_derive f t (f' t)) →
is_derive g x (f' x).
The following two tactics allows one to easily start proving goals
that have the form ∀ n x, is_derive_n f n x (D n x)
or the form ∀ n x, P x → is_derive_n f n x (D n x)
Then, we obtain 3 (resp. 4) subgoals that can be proved by relying
on the auto_derive Coquelicot tactic.
See is_derive_n_exp or is_derive_n_tan for usage examples.
Ltac help_is_derive_n_whole fresh_n fresh_x :=
match goal with
[ |- ∀ n x, is_derive_n ?f n x (@?D n x) ] ⇒
let IHn := fresh "IH" fresh_n in
case;
[ try done
|elim⇒ [/=|fresh_n IHn] fresh_x;
[
|apply: (@is_derive_ext _ _ (D fresh_n.+1) (Derive_n f fresh_n.+1) fresh_x _);
[let t := fresh "t" in
by move⇒ t; rewrite (is_derive_n_unique _ _ _ _ (IHn t))
|
clear IHn]]]
end.
Ltac help_is_derive_n fresh_n fresh_x :=
match goal with
[ |- ∀ n x, @?P x → is_derive_n ?f n x (@?D n x) ] ⇒
let IHn := fresh "IH" fresh_n in
let Hx := fresh "H" fresh_x in
case;
[ try done
|elim⇒ [/=|fresh_n IHn] fresh_x;
[
|move⇒ Hx;
apply: (@is_derive_ext_alt
(D fresh_n.+1) (Derive_n f fresh_n.+1) x (D fresh_n.+2) P Hx);
clear fresh_x Hx;
[
|let t := fresh "t" in
let Ht := fresh "Ht" in
by move⇒ t Ht; rewrite (is_derive_n_unique _ _ _ _ (IHn t Ht))
|
clear IHn]]]
end.
Lemma is_derive_n_exp : ∀ n x, is_derive_n exp n x (exp x).
Lemma is_derive_n_pow :
∀ m, (0 < m)%nat → ∀ n x,
is_derive_n (fun x ⇒ x ^ m)%R n x
(\big[Rmult/1%R]_(i < n) INR (m - i) × x ^ (m - n))%R.
Lemma is_derive_n_inv_pow :
∀ m, (0 < m)%nat → ∀ n x, x ≠ 0 →
is_derive_n (fun x ⇒ / x ^ m)%R n x
(\big[Rmult/1%R]_(i < n) - INR (m + i) / x ^ (m + n))%R.
Lemma is_derive_n_powerRZ m n x :
(0 ≤ m)%Z ∨ x ≠ 0 →
is_derive_n (powerRZ^~ m) n x
(match m with
| Z0 ⇒ if n is O then 1%R else 0%R
| Z.pos p ⇒ \big[Rmult/1%R]_(i < n) INR (Pos.to_nat p - i) ×
x ^ (Pos.to_nat p - n)
| Z.neg p ⇒ \big[Rmult/1%R]_(i < n) - INR (Pos.to_nat p + i) ×
/ x ^ (Pos.to_nat p + n)
end).
Lemma ex_derive_n_powerRZ m n x :
(0 ≤ m)%Z ∨ x ≠ 0 →
ex_derive_n (powerRZ^~ m) n x.
Lemma is_derive_n_Rpower n a x :
0 < x →
is_derive_n (Rpower^~ a) n x
(\big[Rmult/1%R]_(i < n) (a - INR i) × Rpower x (a - INR n)).
Lemma is_derive_n_inv n x :
x ≠ 0 →
is_derive_n Rinv n x
(\big[Rmult/1%R]_(i < n) - INR (1 + i) × / x ^ (1 + n))%R.
Lemma is_derive_n_ln n x :
0 < x →
is_derive_n ln n x
(match n with
| 0 ⇒ ln x
| n.+1 ⇒ (\big[Rmult/1%R]_(i < n) - INR (1 + i) × / x ^ (1 + n))%R
end).
Lemma is_derive_ln x :
0 < x → is_derive ln x (/ x)%R.
Lemma is_derive_n_sqrt n x :
0 < x →
is_derive_n sqrt n x
(\big[Rmult/1%R]_(i < n) (/2 - INR i) × Rpower x (/2 - INR n)).
Lemma is_derive_n_invsqrt n x :
0 < x →
is_derive_n (fun t ⇒ / sqrt t) n x
(\big[Rmult/1%R]_(i < n) (-/2 - INR i) × Rpower x (-/2 - INR n)).
Lemma is_derive_2n_sin n x :
is_derive_n sin (n + n) x ((-1)^n × sin x).
Lemma is_derive_n_sin n (x : R) :
is_derive_n sin n x (if odd n then (-1)^n./2 × cos x
else ((-1)^n./2 × sin x)).
Lemma is_derive_2n_cos n x :
is_derive_n cos (n + n) x ((-1)^n × cos x).
Lemma is_derive_n_cos n (x : R) :
is_derive_n cos n x (if odd n then (-1)^(n./2) × - sin x
else ((-1)^(n./2) × cos x)).
Definition is_derive_atan x :
is_derive atan x (/ (1 + x²)).
Definition is_derive_tan x :
cos x ≠ 0%R → is_derive tan x (tan x ^ 2 + 1)%R.
Lemma filterlimi_lim_ext_loc {T U} {F G} {FF : Filter F} (f : T → U) (g : T → U → Prop) :
F (fun x ⇒ g x (f x)) →
filterlim f F G →
filterlimi g F G.
Lemma prod_to_single {T U V : UniformSpace} {F: (U → Prop) → Prop} {FF : Filter F}
(G : (V → Prop) → Prop) x (f : T → U → V) :
filterlim (fun tu : T × U ⇒ f tu.1 tu.2) (filter_prod (at_point x) F) G ↔
filterlim (fun u : U ⇒ f x u) F G.
Lemma prodi_to_single_l {T U V : UniformSpace} {F: (U → Prop) → Prop} {FF : Filter F}
(G : (V → Prop) → Prop) x (f : T → U → V → Prop) :
filterlimi (fun tu : T × U ⇒ f tu.1 tu.2) (filter_prod (at_point x) F) G ↔
filterlimi (fun u : U ⇒ f x u) F G.
Lemma prodi_to_single_r {T U V : UniformSpace} {F: (U → Prop) → Prop} {FF : Filter F}
(G : (V → Prop) → Prop) x (f : U → T → V → Prop) :
filterlimi (fun tu : U × T ⇒ f tu.1 tu.2) (filter_prod F (at_point x)) G ↔
filterlimi (fun u : U ⇒ f u x) F G.
Lemma is_RInt_gen_exp_infty a lam (Hlam : 0 < lam) :
is_RInt_gen (fun x ⇒ exp (- (lam × x))) (at_point a) (Rbar_locally p_infty) (exp (-(lam × a)) / lam).
Lemma ex_RInt_gen_Chasles :
∀ {V : NormedModule R_AbsRing} {Fa Fc : (R → Prop) → Prop},
∀ {FFa : Filter Fa} {FFc : Filter Fc},
∀ (f : R → V) (b : R),
ex_RInt_gen f Fa (at_point b) →
ex_RInt_gen f (at_point b) Fc →
ex_RInt_gen f Fa Fc.
Lemma RInt_gen_Chasles :
∀ {V : CompleteNormedModule R_AbsRing} {Fa Fc : (R → Prop) → Prop},
∀ {FFa : ProperFilter' Fa} {FFc : ProperFilter' Fc},
∀ (f : R → V) (b : R),
ex_RInt_gen f Fa (at_point b) →
ex_RInt_gen f (at_point b) Fc →
plus (RInt_gen f Fa (at_point b)) (RInt_gen f (at_point b) Fc) = RInt_gen f Fa Fc.
Lemma RInt_gen_ext :
∀ {V : CompleteNormedModule R_AbsRing} {Fa Fb : (R → Prop) → Prop}
{FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R → V),
filter_prod Fa Fb (fun ab ⇒
∀ x, Rmin (fst ab) (snd ab) < x < Rmax (fst ab) (snd ab) → f x = g x) →
RInt_gen f Fa Fb = RInt_gen g Fa Fb.
Lemma RInt_gen_ext_eq :
∀ {V : CompleteNormedModule R_AbsRing} {Fa Fb : (R → Prop) → Prop}
{FFa : ProperFilter Fa} {FFb : ProperFilter Fb} (f g : R → V),
(∀ x, f x = g x) →
RInt_gen f Fa Fb = RInt_gen g Fa Fb.