Library Interval.Missing.Stdlib
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) 2007-2016, Inria
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 ZArith Reals Psatz.
From Flocq Require Import Raux.
Ltac evar_last :=
match goal with
| |- ?f ?x ⇒
let tx := type of x in
let tx := eval simpl in tx in
let tmp := fresh "tmp" in
evar (tmp : tx) ;
refine (@eq_ind tx tmp f _ x _) ;
unfold tmp ; clear tmp
end.
Lemma Rmult_le_compat_neg_r :
∀ r r1 r2 : R,
(r ≤ 0)%R → (r1 ≤ r2)%R → (r2 × r ≤ r1 × r)%R.
Lemma Rsqr_plus1_pos x : (0 < 1 + Rsqr x)%R.
Lemma Rsqr_plus1_neq0 x : (1 + Rsqr x ≠ 0)%R.
Lemma Rmin_Rle :
∀ r1 r2 r,
(Rmin r1 r2 ≤ r)%R ↔ (r1 ≤ r)%R ∨ (r2 ≤ r)%R.
Lemma Rle_Rinv_pos :
∀ x y : R,
(0 < x)%R → (x ≤ y)%R → (/y ≤ /x)%R.
Lemma Rle_Rinv_neg :
∀ x y : R,
(y < 0)%R → (x ≤ y)%R → (/y ≤ /x)%R.
Lemma Rmult_le_pos_pos :
∀ x y : R,
(0 ≤ x)%R → (0 ≤ y)%R → (0 ≤ x × y)%R.
Lemma Rmult_le_pos_neg :
∀ x y : R,
(0 ≤ x)%R → (y ≤ 0)%R → (x × y ≤ 0)%R.
Lemma Rmult_le_neg_pos :
∀ x y : R,
(x ≤ 0)%R → (0 ≤ y)%R → (x × y ≤ 0)%R.
Lemma Rmult_le_neg_neg :
∀ x y : R,
(x ≤ 0)%R → (y ≤ 0)%R → (0 ≤ x × y)%R.
Lemma Rabs_def1_le :
∀ x a,
(x ≤ a)%R → (-a ≤ x)%R →
(Rabs x ≤ a)%R.
Lemma Rabs_def2_le :
∀ x a,
(Rabs x ≤ a)%R →
(-a ≤ x ≤ a)%R.
Theorem derivable_pt_lim_eq :
∀ f g,
(∀ x, f x = g x) →
∀ x l,
derivable_pt_lim f x l → derivable_pt_lim g x l.
Definition locally_true x (P : R → Prop) :=
∃ delta, (0 < delta)%R ∧
∀ h, (Rabs h < delta)%R → P (x + h)%R.
Theorem derivable_pt_lim_eq_locally :
∀ f g x l,
locally_true x (fun v ⇒ f v = g v) →
derivable_pt_lim f x l → derivable_pt_lim g x l.
Theorem locally_true_and :
∀ P Q x,
locally_true x P →
locally_true x Q →
locally_true x (fun x ⇒ P x ∧ Q x).
Theorem locally_true_imp :
∀ P Q : R → Prop,
(∀ x, P x → Q x) →
∀ x,
locally_true x P →
locally_true x Q.
Theorem continuity_pt_lt :
∀ f x y,
(f x < y)%R →
continuity_pt f x →
locally_true x (fun u ⇒ (f u < y)%R).
Theorem continuity_pt_gt :
∀ f x y,
(y < f x)%R →
continuity_pt f x →
locally_true x (fun u ⇒ (y < f u)%R).
Theorem continuity_pt_ne :
∀ f x y,
f x ≠ y →
continuity_pt f x →
locally_true x (fun u ⇒ f u ≠ y).
Theorem derivable_pt_lim_tan :
∀ x,
(cos x ≠ 0)%R →
derivable_pt_lim tan x (1 + Rsqr (tan x))%R.
Definition connected (P : R → Prop) :=
∀ x y, P x → P y →
∀ z, (x ≤ z ≤ y)%R → P z.
Lemma connected_and :
∀ d1 d2, connected d1 → connected d2 → connected (fun t ⇒ d1 t ∧ d2 t).
Lemma connected_ge :
∀ x, connected (Rle x).
Lemma connected_le :
∀ x, connected (fun t ⇒ Rle t x).
Theorem derivable_pos_imp_increasing :
∀ f f' dom,
connected dom →
(∀ x, dom x → derivable_pt_lim f x (f' x) ∧ (0 ≤ f' x)%R) →
∀ u v, dom u → dom v → (u ≤ v)%R → (f u ≤ f v)%R.
Theorem derivable_neg_imp_decreasing :
∀ f f' dom,
connected dom →
(∀ x, dom x → derivable_pt_lim f x (f' x) ∧ (f' x ≤ 0)%R) →
∀ u v, dom u → dom v → (u ≤ v)%R → (f v ≤ f u)%R.
Lemma even_or_odd :
∀ n : nat, ∃ k, n = 2 × k ∨ n = S (2 × k).
Lemma alternated_series_ineq' :
∀ u l,
Un_decreasing u →
Un_cv u 0 →
Un_cv (fun n ⇒ sum_f_R0 (tg_alt u) n) l →
∀ n,
(0 ≤ (-1)^(S n) × (l - sum_f_R0 (tg_alt u) n) ≤ u (S n))%R.
Lemma Un_decreasing_exp :
∀ x : R,
(0 ≤ x ≤ 1)%R →
Un_decreasing (fun n ⇒ / INR (fact n) × x ^ n)%R.
Lemma Un_decreasing_cos :
∀ x : R,
(Rabs x ≤ 1)%R →
Un_decreasing (fun n ⇒ / INR (fact (2 × n)) × x ^ (2 × n))%R.
Lemma Un_cv_subseq :
∀ (u : nat → R) (f : nat → nat) (l : R),
(∀ n, f n < f (S n)) →
Un_cv u l → Un_cv (fun n ⇒ u (f n)) l.
Definition sinc (x : R) := proj1_sig (exist_sin (Rsqr x)).
Lemma sin_sinc :
∀ x,
sin x = (x × sinc x)%R.
Lemma sinc_0 :
sinc 0 = 1%R.
Lemma Un_decreasing_sinc :
∀ x : R,
(Rabs x ≤ 1)%R →
Un_decreasing (fun n : nat ⇒ (/ INR (fact (2 × n + 1)) × x ^ (2 × n)))%R.
Lemma atan_plus_PI4 :
∀ x, (-1 < x)%R →
(atan ((x - 1) / (x + 1)) + PI / 4)%R = atan x.
Lemma atan_inv :
∀ x, (0 < x)%R →
atan (/ x) = (PI / 2 - atan x)%R.
Lemma Un_decreasing_atanc :
∀ x : R,
(Rabs x ≤ 1)%R →
Un_decreasing (fun n : nat ⇒ (/ INR (2 × n + 1) × x ^ (2 × n)))%R.
Lemma Un_cv_atanc :
∀ x : R,
(Rabs x ≤ 1)%R →
Un_cv (fun n : nat ⇒ (/ INR (2 × n + 1) × x ^ (2 × n)))%R 0.
Lemma atanc_exists :
∀ x,
(Rabs x ≤ 1)%R →
{ l : R | Un_cv (sum_f_R0 (tg_alt (fun n ⇒ / INR (2 × n + 1) × x ^ (2 × n))%R)) l }.
Definition atanc x :=
match Ratan.in_int x with
| left H ⇒ proj1_sig (atanc_exists x (Rabs_le _ _ H))
| right _ ⇒ (atan x / x)%R
end.
Lemma atanc_opp :
∀ x,
atanc (- x) = atanc x.
Lemma atan_atanc :
∀ x,
atan x = (x × atanc x)%R.
Lemma Un_decreasing_ln1pc :
∀ x : R,
(0 ≤ x ≤ 1)%R →
Un_decreasing (fun n : nat ⇒ (/ INR (n + 1) × x ^ n))%R.
Lemma Un_cv_ln1pc :
∀ x : R,
(Rabs x ≤ 1)%R →
Un_cv (fun n : nat ⇒ (/ INR (n + 1) × x ^ n))%R 0.
Lemma ln1pc_exists :
∀ x,
(0 ≤ x < 1)%R →
{ l : R | Un_cv (sum_f_R0 (tg_alt (fun n ⇒ / INR (n + 1) × x ^ n)%R)) l }.
Lemma ln1pc_in_int :
∀ x,
{ (0 ≤ x < 1)%R } + { ¬(0 ≤ x < 1)%R }.
Definition ln1pc x :=
match ln1pc_in_int x with
| left H ⇒ proj1_sig (ln1pc_exists x H)
| right _ ⇒ (ln (1 + x) / x)%R
end.
Require Import Coquelicot.Coquelicot.
Lemma ln1p_ln1pc :
∀ x,
ln (1 + x) = (x × ln1pc x)%R.
Define a shorter name
Notation Rmult_neq0 := Rmult_integral_contrapositive_currified.
Lemma Rdiv_eq_reg a b c d :
(a × d = b × c → b ≠ 0%R → d ≠ 0%R → a / b = c / d)%R.
Lemma Rlt_neq_sym (x y : R) :
(x < y → y ≠ x)%R.
Lemma Rdiv_pos_compat (x y : R) :
(0 ≤ x → 0 < y → 0 ≤ x / y)%R.
Lemma Rdiv_pos_compat_rev (x y : R) :
(0 ≤ x / y → 0 < y → 0 ≤ x)%R.
Lemma Rdiv_neg_compat (x y : R) :
(x ≤ 0 → 0 < y → x / y ≤ 0)%R.
Lemma Rdiv_neg_compat_rev (x y : R) :
(x / y ≤ 0 → 0 < y → x ≤ 0)%R.
Lemma Rdiv_eq_reg a b c d :
(a × d = b × c → b ≠ 0%R → d ≠ 0%R → a / b = c / d)%R.
Lemma Rlt_neq_sym (x y : R) :
(x < y → y ≠ x)%R.
Lemma Rdiv_pos_compat (x y : R) :
(0 ≤ x → 0 < y → 0 ≤ x / y)%R.
Lemma Rdiv_pos_compat_rev (x y : R) :
(0 ≤ x / y → 0 < y → 0 ≤ x)%R.
Lemma Rdiv_neg_compat (x y : R) :
(x ≤ 0 → 0 < y → x / y ≤ 0)%R.
Lemma Rdiv_neg_compat_rev (x y : R) :
(x / y ≤ 0 → 0 < y → x ≤ 0)%R.
The following definition can be used by doing rewrite !Rsimpl
Definition Rsimpl :=
(Rplus_0_l, Rplus_0_r, Rmult_1_l, Rmult_1_r, Rmult_0_l, Rmult_0_r, Rdiv_1).
Section Integral.
Variables (f : R → R) (ra rb : R).
Hypothesis Hab : ra < rb.
Hypothesis Hint : ex_RInt f ra rb.
Lemma RInt_le_r (u : R) :
(∀ x : R, ra ≤ x ≤ rb → f x ≤ u) → RInt f ra rb / (rb - ra) ≤ u.
Lemma RInt_le_l (l : R) :
(∀ x : R, ra ≤ x ≤ rb → l ≤ f x) → l ≤ RInt f ra rb / (rb - ra).
End Integral.
Module Compatibility.
Definition Q2R x := (IZR (QArith_base.Qnum x) / IZR (Z.pos (QArith_base.Qden x)))%R.
End Compatibility.
Lemma Z_div_mod_eq : ∀ a b : Z, (b > 0)%Z → a = (b × (a / b) + a mod b)%Z.
(Rplus_0_l, Rplus_0_r, Rmult_1_l, Rmult_1_r, Rmult_0_l, Rmult_0_r, Rdiv_1).
Section Integral.
Variables (f : R → R) (ra rb : R).
Hypothesis Hab : ra < rb.
Hypothesis Hint : ex_RInt f ra rb.
Lemma RInt_le_r (u : R) :
(∀ x : R, ra ≤ x ≤ rb → f x ≤ u) → RInt f ra rb / (rb - ra) ≤ u.
Lemma RInt_le_l (l : R) :
(∀ x : R, ra ≤ x ≤ rb → l ≤ f x) → l ≤ RInt f ra rb / (rb - ra).
End Integral.
Module Compatibility.
Definition Q2R x := (IZR (QArith_base.Qnum x) / IZR (Z.pos (QArith_base.Qden x)))%R.
End Compatibility.
Lemma Z_div_mod_eq : ∀ a b : Z, (b > 0)%Z → a = (b × (a / b) + a mod b)%Z.