Library mathcomp.analysis.trigo
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
Require Import mathcomp_extra boolp reals ereal nsatz_realtype classical_sets.
Require Import signed functions topology normedtype landau sequences derive.
Require Import realfun exp.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
Require Import mathcomp_extra boolp reals ereal nsatz_realtype classical_sets.
Require Import signed functions topology normedtype landau sequences derive.
Require Import realfun exp.
Theory of trigonometric functions
This file provides the definitions of basic trigonometric functions and
develops their theories.
periodic f T == f is a periodic function of period T
alternating f T == f is an alternating function of period T
sin_coeff x == the sequence of coefficients of sin x
sin x == the sine function, i.e., lim (series (sin_coeff x))
sin_coeff' x == the sequence of odd coefficients of sin x
cos_coeff x == the sequence of coefficients of cos x
cos x == the cosine function, i.e., lim (series (cos_coeff x))
cos_coeff' x == the sequence of even coefficients of cos x
pi == pi
tan x == the tangent function
acos x == the arccos function
asin x == the arcsin function
atan x == the arctangent function
Acknowledgments: the proof of cos 2 < 0 is inspired from HOL-light, some
proofs of trigonometric relations are taken from
https://github.com/affeldt-aist/coq-robot.
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
NB: backport to mathcomp in progress
Lemma sqrtrV (R : rcfType) (x : R) : 0 ≤ x → Num.sqrt (x^-1) = (Num.sqrt x)^-1.
Lemma eqr_div (R : numFieldType) (x y z t : R):
y != 0 → t != 0 → (x / y == z / t) = (x × t == z × y).
Lemma big_nat_mul (R : zmodType) (f : R ^nat) (n k : nat) :
\sum_(0 ≤ i < n × k) f i =
\sum_(0 ≤ i < n) \sum_(i × k ≤ j < i.+1 × k) f j.
Lemma eqr_div (R : numFieldType) (x y z t : R):
y != 0 → t != 0 → (x / y == z / t) = (x × t == z × y).
Lemma big_nat_mul (R : zmodType) (f : R ^nat) (n k : nat) :
\sum_(0 ≤ i < n × k) f i =
\sum_(0 ≤ i < n) \sum_(i × k ≤ j < i.+1 × k) f j.
/NB: backport to mathcomp in progress
Lemma cvg_series_cvg_series_group (R : realFieldType) (f : R ^nat) k :
cvg (series f) → (0 < k)%N →
[series \sum_(n × k ≤ i < n.+1 × k) f i]_n --> lim (series f).
Lemma lt_sum_lim_series (R : realFieldType) (f : R ^nat) n : cvg (series f) →
(∀ d, 0 < f (n + d.*2)%N + f (n + d.*2.+1)%N) →
\sum_(0 ≤ i < n) f i < lim (series f).
Section periodic.
Variables U V : zmodType.
Implicit Type f : U → V.
Definition periodic f (T : U) := ∀ u, f (u + T) = f u.
Lemma periodicn f (T : U) : periodic f T → ∀ n a, f (a + T *+ n) = f a.
End periodic.
Section alternating.
Variables (U : zmodType) (V : ringType).
Implicit Type f : U → V.
Definition alternating f (T : U) := ∀ x, f (x + T) = - f x.
Lemma alternatingn f (T : U) : alternating f T →
∀ n a, f (a + T *+ n) = (- 1) ^+ n × f a.
End alternating.
Section CosSin.
Variable R : realType.
Implicit Types x y : R.
Definition sin_coeff x :=
[sequence (odd n)%:R × (-1) ^+ n.-1./2 × x ^+ n / n`!%:R]_n.
Lemma sin_coeffE x : sin_coeff x =
(fun n ⇒ (fun n ⇒ (odd n)%:R × (-1) ^+ n.-1./2 × (n`!%:R)^-1) n × x ^+ n).
Lemma sin_coeff_even n x : sin_coeff x n.*2 = 0.
Lemma is_cvg_series_sin_coeff x : cvg (series (sin_coeff x)).
Definition sin x : R := lim (series (sin_coeff x)).
Lemma sinE : sin = fun x ⇒
lim (pseries (fun n ⇒ (odd n)%:R × (-1) ^+ n.-1./2 × (n`!%:R)^-1) x).
Definition sin_coeff' x (n : nat) := (-1)^n × x ^+ n.*2.+1 / n.*2.+1`!%:R.
Lemma sin_coeff'E x n : sin_coeff' x n = sin_coeff x n.*2.+1.
Lemma cvg_sin_coeff' x : series (sin_coeff' x) --> sin x.
Lemma diffs_sin :
pseries_diffs (fun n ⇒ (odd n)%:R × (-1) ^+ n.-1./2 × (n`!%:R)^-1) =
(fun n ⇒ (~~(odd n))%:R × (-1) ^+ n./2 × (n`!%:R)^-1 : R).
Lemma series_sin_coeff0 n : series (sin_coeff 0) n.+1 = 0.
Lemma sin0 : sin 0 = 0.
Definition cos_coeff x :=
[sequence (~~ odd n)%:R × (-1)^n./2 × x ^+ n / n`!%:R]_n.
Lemma cos_coeff_odd n x : cos_coeff x n.*2.+1 = 0.
Lemma cos_coeff_2_0 : cos_coeff 2 0%N = 1 :> R.
Lemma cos_coeff_2_2 : cos_coeff 2 2%N = - 2%:R :> R.
Lemma cos_coeff_2_4 : cos_coeff 2 4%N = 2%:R / 3%:R :> R.
Lemma cos_coeffE x :
cos_coeff x = (fun n ⇒ (fun n ⇒ (~~(odd n))%:R × (-1) ^+ n./2 ×
(n`!%:R)^-1) n × x ^+ n).
Lemma is_cvg_series_cos_coeff x : cvg (series (cos_coeff x)).
Definition cos x : R := lim (series (cos_coeff x)).
Lemma cosE : cos = fun x ⇒
lim (series (fun n ⇒
(fun n ⇒ (~~(odd n))%:R × (-1)^+ n./2 × (n`!%:R)^-1) n
× x ^+ n)).
Definition cos_coeff' x (n : nat) := (-1)^n × x ^+ n.*2 / n.*2`!%:R.
Lemma cos_coeff'E x n : cos_coeff' x n = cos_coeff x n.*2.
Lemma cvg_cos_coeff' x : series (cos_coeff' x) --> cos x.
Lemma diffs_cos :
pseries_diffs (fun n ⇒ (~~(odd n))%:R × (-1) ^+ n./2 × (n`!%:R)^-1) =
(fun n ⇒ - ((odd n)%:R × (-1) ^+ n.-1./2 × (n`!%:R)^-1): R).
Lemma series_cos_coeff0 n : series (cos_coeff 0) n.+1 = 1.
Lemma cos0 : cos 0 = 1.
Global Instance is_derive_sin x : is_derive x 1 sin (cos x).
Lemma derivable_sin x : derivable sin x 1.
Lemma continuous_sin : continuous sin.
Global Instance is_derive_cos x : is_derive x 1 cos (- (sin x)).
Lemma derivable_cos x : derivable cos x 1.
Lemma continuous_cos : continuous cos.
Lemma cos2Dsin2 x : (cos x) ^+ 2 + (sin x) ^+ 2 = 1.
Lemma cos_max x : `| cos x | ≤ 1.
Lemma cos_geN1 x : -1 ≤ cos x.
Lemma cos_le1 x : cos x ≤ 1.
Lemma sin_max x : `| sin x | ≤ 1.
Lemma sin_geN1 x : -1 ≤ sin x.
Lemma sin_le1 x : sin x ≤ 1.
Fact sinD_cosD x y :
(sin (x + y) - (sin x × cos y + cos x × sin y)) ^+ 2 +
(cos (x + y) - (cos x × cos y - sin x × sin y)) ^+ 2 = 0.
Lemma sinD x y : sin (x + y) = sin x × cos y + cos x × sin y.
Lemma cosD x y : cos (x + y) = cos x × cos y - sin x × sin y.
Lemma sin2cos2 x : sin x ^+ 2 = 1 - cos x ^+ 2.
Lemma cos2sin2 x : cos x ^+ 2 = 1 - sin x ^+ 2.
Lemma sin_mulr2n x : sin (x *+ 2) = (cos x × sin x) *+ 2.
Lemma cos_mulr2n x : cos (x *+ 2) = cos x ^+2 *+ 2 - 1.
Fact sinN_cosN x :
(sin (- x) + sin x) ^+ 2 + (cos (- x) - cos x) ^+ 2 = 0.
Lemma sinN x : sin (- x) = - sin x.
Lemma cosN x : cos (- x) = cos x.
Lemma sin_sg x y : sin (Num.sg x × y) = Num.sg x × sin y.
Lemma cos_sg x y : x != 0 → cos (Num.sg x × y) = cos y.
Lemma cosB x y : cos (x - y) = cos x × cos y + sin x × sin y.
Lemma sinB x y : sin (x - y) = sin x × cos y - cos x × sin y.
Lemma norm_cos_eq1 x : (`|cos x| == 1) = (sin x == 0).
Lemma norm_sin_eq1 x : (`|sin x| == 1) = (cos x == 0).
Lemma cos1sin0 x : `|cos x| = 1 → sin x = 0.
Lemma sin1cos0 x : `|sin x| = 1 → cos x = 0.
Lemma sin0cos1 x : sin x = 0 → `|cos x| = 1.
Lemma cos_norm x : cos `|x| = cos x.
End CosSin.
Arguments sin {R}.
Arguments cos {R}.
Section Pi.
Variable R : realType.
Implicit Types (x y : R) (n k : nat).
Definition pi : R := get [set x | 0 ≤ x ≤ 2 ∧ cos x = 0] *+ 2.
Lemma pihalfE : pi / 2 = get [set x | 0 ≤ x ≤ 2 ∧ cos x = 0].
Lemma cos2_lt0 : cos 2 < 0 :> R.
Lemma sin2_gt0 x : 0 < x < 2 → 0 < sin x.
Lemma cos1_gt0 : cos 1 > 0 :> R.
Lemma cos_exists : exists2 pih : R, 1 ≤ pih ≤ 2 & cos pih = 0.
Lemma cos_02_uniq x y :
0 ≤ x ≤ 2 → cos x = 0 → 0 ≤ y ≤ 2 → cos y = 0 → x = y.
Lemma pihalf_02_cos_pihalf : 0 ≤ pi / 2 ≤ 2 ∧ cos (pi / 2) = 0.
#[deprecated(note="Use pihalf_ge1 and pihalf_lt2 instead")]
Lemma pihalf_02 : 0 < pi / 2 < 2.
Let pihalf_12 : 1 ≤ pi / 2 < 2.
Lemma pihalf_ge1 : 1 ≤ pi / 2.
Lemma pihalf_lt2 : pi / 2 < 2.
Lemma pi_ge2 : 2 ≤ pi.
Lemma pi_gt0 : 0 < pi.
Lemma pi_ge0 : 0 ≤ pi.
Lemma sin_gt0_pihalf x : 0 < x < pi / 2 → 0 < sin x.
Lemma cos_gt0_pihalf x : -(pi / 2) < x < pi / 2 → 0 < cos x.
Lemma cos_pihalf : cos (pi / 2) = 0.
Lemma sin_pihalf : sin (pi / 2) = 1.
Lemma cos_ge0_pihalf x : -(pi / 2) ≤ x ≤ pi / 2 → 0 ≤ cos x.
Lemma cospi : cos pi = - 1.
Lemma sinpi : sin pi = 0.
Lemma cos2pi : cos (pi *+ 2) = 1.
Lemma sin2pi : sin (pi *+ 2) = 0.
Lemma sinDpi : alternating sin pi.
Lemma cosDpi : alternating cos pi.
Lemma sinD2pi : periodic sin (pi *+ 2).
Lemma cosD2pi : periodic cos (pi *+ 2).
Lemma cosDpihalf a : cos (a + pi / 2) = - sin a.
Lemma cosBpihalf a : cos (a - pi / 2) = sin a.
Lemma sinDpihalf a : sin (a + pi / 2) = cos a.
Lemma sinBpihalf a : sin (a - pi / 2) = - cos a.
Lemma sin_ge0_pi x : 0 ≤ x ≤ pi → 0 ≤ sin x.
Lemma sin_gt0_pi x : 0 < x < pi → 0 < sin x.
Lemma ltr_cos : {in `[0, pi] &, {mono cos : x y /~ y < x}}.
Lemma ltr_sin : {in `[ (- (pi/2)), pi/2] &, {mono sin : x y / x < y}}.
Lemma cos_inj : {in `[0,pi] &, injective (@cos R)}.
Lemma sin_inj : {in `[(- (pi/2)), (pi/2)] &, injective sin}.
End Pi.
Arguments pi {R}.
Section Tan.
Variable R : realType.
Definition tan (x : R) := sin x / cos x.
Lemma tan0 : tan 0 = 0 :> R.
Lemma tanpi : tan pi = 0.
Lemma tanN x : tan (- x) = - tan x.
Lemma tanD x y : cos x != 0 → cos y != 0 →
tan (x + y) = (tan x + tan y) / (1 - tan x × tan y).
Lemma tan_mulr2n x :
cos x != 0 → tan (x *+ 2) = tan x *+ 2 / (1 - tan x ^+ 2).
Lemma cos2_tan2 x : cos x != 0 → (cos x) ^- 2 = 1 + (tan x) ^+ 2.
Lemma tan_pihalf : tan (pi / 2) = 0.
Lemma tan_piquarter : tan (pi / 4%:R) = 1.
Lemma tanDpi x : tan (x + pi) = tan x.
Lemma continuous_tan x : cos x != 0 → {for x, continuous tan}.
Lemma is_derive_tan x :
cos x != 0 → is_derive x 1 tan ((cos x)^-2).
Lemma derivable_tan x : cos x != 0 → derivable tan x 1.
Lemma ltr_tan : {in `](- (pi/2)), (pi/2)[ &, {mono tan : x y / x < y}}.
Lemma tan_inj : {in `](- (pi/2)), (pi/2)[ &, injective tan}.
End Tan.
Arguments tan {R}.
#[global] Hint Extern 0 (is_derive _ _ tan _) ⇒
(eapply is_derive_tan; first by []) : typeclass_instances.
Section Acos.
Variable R : realType.
Definition acos (x : R) : R := get [set y | 0 ≤ y ≤ pi ∧ cos y = x].
Lemma acos_def x :
-1 ≤ x ≤ 1 → 0 ≤ acos x ≤ pi ∧ cos (acos x) = x.
Lemma acos_ge0 x : -1 ≤ x ≤ 1 → 0 ≤ acos x.
Lemma acos_lepi x : -1 ≤ x ≤ 1 → acos x ≤ pi.
Lemma acosK : {in `[(-1),1], cancel acos cos}.
Lemma acos_gt0 x : -1 ≤ x < 1 → 0 < acos x.
Lemma acos_ltpi x : -1 < x ≤ 1 → acos x < pi.
Lemma cosK : {in `[0, pi], cancel cos acos}.
Lemma acos1 : acos (1 : R) = 0.
Lemma acos0 : acos (0 : R) = pi / 2%:R.
Lemma acosN a : -1 ≤ a ≤ 1 → acos (- a) = pi - acos a.
Lemma acosN1 : acos (- 1) = (pi : R).
Lemma cosKN a : - pi ≤ a ≤ 0 → acos (cos a) = - a.
Lemma sin_acos x : -1 ≤ x ≤ 1 → sin (acos x) = Num.sqrt (1 - x^+2).
Lemma continuous_acos x : -1 < x < 1 → {for x, continuous acos}.
Lemma is_derive1_acos (x : R) :
-1 < x < 1 → is_derive x 1 acos (- (Num.sqrt (1 - x ^+ 2))^-1).
End Acos.
#[global] Hint Extern 0 (is_derive _ 1 (@acos _) _) ⇒
(eapply is_derive1_acos; first by []) : typeclass_instances.
Section Asin.
Variable R : realType.
Definition asin (x : R) : R := get [set y | -(pi / 2) ≤ y ≤ pi / 2 ∧ sin y = x].
Lemma asin_def x :
-1 ≤ x ≤ 1 → -(pi / 2) ≤ asin x ≤ pi / 2 ∧ sin (asin x) = x.
Lemma asin_geNpi2 x : -1 ≤ x ≤ 1 → -(pi / 2) ≤ asin x.
Lemma asin_lepi2 x : -1 ≤ x ≤ 1 → asin x ≤ pi / 2.
Lemma asinK : {in `[(-1),1], cancel asin sin}.
Lemma asin_ltpi2 x : -1 ≤ x < 1 → asin x < pi/2.
Lemma asin_gtNpi2 x : -1 < x ≤ 1 → - (pi / 2) < asin x.
Lemma sinK : {in `[(- (pi / 2)), pi / 2], cancel sin asin}.
Lemma cos_asin x : -1 ≤ x ≤ 1 → cos (asin x) = Num.sqrt (1 - x^+2).
Lemma continuous_asin x : -1 < x < 1 → {for x, continuous asin}.
Lemma is_derive1_asin (x : R) :
-1 < x < 1 → is_derive x 1 asin ((Num.sqrt (1 - x ^+ 2))^-1).
End Asin.
#[global] Hint Extern 0 (is_derive _ 1 (@asin _) _) ⇒
(eapply is_derive1_asin; first by []) : typeclass_instances.
Section Atan.
Variable R : realType.
Definition atan (x : R) : R :=
get [set y | -(pi / 2) < y < pi / 2 ∧ tan y = x].
Lemma atan_def x : -(pi / 2) < atan x < pi / 2 ∧ tan (atan x) = x.
Lemma atan_gtNpi2 x : - (pi / 2) < atan x.
Lemma atan_ltpi2 x : atan x < pi / 2.
Lemma atanK : cancel atan tan.
Lemma atan0 : atan 0 = 0 :> R.
Lemma atan1 : atan 1 = pi / 4%:R :> R.
Lemma atanN x : atan (- x) = - atan x.
Lemma tanK : {in `](- (pi / 2)), (pi / 2)[ , cancel tan atan}.
Lemma continuous_atan x : {for x, continuous atan}.
Lemma cos_atan x : cos (atan x) = (Num.sqrt (1 + x ^+ 2)) ^-1.
Global Instance is_derive1_atan (x : R) : is_derive x 1 atan (1 + x ^+ 2)^-1.
End Atan.