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.
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import mathcomp_extra.
Require Import reals ereal nsatz_realtype signed topology normedtype landau.
Require Import sequences derive realfun exp.
From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
From mathcomp.classical Require Import boolp classical_sets functions.
From mathcomp.classical Require Import mathcomp_extra.
Require Import reals ereal nsatz_realtype signed topology normedtype landau.
Require Import sequences derive 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.