From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
From mathcomp Require Import interval rat.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
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.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldNormedType.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Lemma
sqrtrV
(
R
: rcfType) (
x
: R)
: 0 <= x -> Num.sqrt (
x^-1)
= (
Num.sqrt x)
^-1.
Proof.
Lemma
eqr_div
(
R
: numFieldType) (
x
y
z
t
: R)
:
y != 0 -> t != 0 -> (
x / y == z / t)
= (
x * t == z * y).
Proof.
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.
Proof.
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).
Proof.
move=> /cvg_ballP cf k0; apply/cvg_ballP => _/posnumP[e].
have := !! cf _ (
gt0 e)
=> -[n _ nl]; near=> m.
rewrite /ball /= [in X in `|_ - X|]/series [in X in `|_ - X|]/= -big_nat_mul.
have /nl : (
n <= m * k)
%N.
by near: m; exists n.
+1 => //= p /ltnW /leq_trans /(
_ (
leq_pmulr _ k0)).
by rewrite /ball /= distrC.
Unshelve.
all: by end_near. Qed.
Lemma
lt_sum_lim_series
(
R
: realFieldType) (
f
: R ^nat)
n
: cvg (
series f)
->
(
forall
d,
0 < f (
n + d.
*2)
%N + f (
n + d.
*2.
+1)
%N)
->
\sum_(
0 <=
i
< n)
f i < lim (
series f).
Proof.
Section
periodic
.
Variables
U
V
: zmodType.
Implicit Type f : U -> V.
Definition
periodic
f
(
T
: U)
:= forall
u,
f (
u + T)
= f u.
Lemma
periodicn
f
(
T
: U)
: periodic f T -> forall
n
a,
f (
a + T *+ n)
= f a.
Proof.
End periodic.
Section
alternating
.
Variables (
U
: zmodType) (
V
: ringType).
Implicit Type f : U -> V.
Definition
alternating
f
(
T
: U)
:= forall
x,
f (
x + T)
= - f x.
Lemma
alternatingn
f
(
T
: U)
: alternating f T ->
forall
n
a,
f (
a + T *+ n)
= (
- 1)
^+ n * f a.
Proof.
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).
Proof.
by apply/funext => i; rewrite /sin_coeff /= -!mulrA [_ / _]mulrC. Qed.
Lemma
sin_coeff_even
n
x
: sin_coeff x n.
*2 = 0.
Proof.
by rewrite /sin_coeff /= odd_double /= !mul0r. Qed.
Lemma
is_cvg_series_sin_coeff
x
: cvg (
series (
sin_coeff x)).
Proof.
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).
Proof.
by apply/funext => x; rewrite /pseries -sin_coeffE. Qed.
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.
Proof.
Lemma
cvg_sin_coeff'
x
: series (
sin_coeff' x)
--> sin x.
Proof.
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).
Proof.
apply/funext => i; rewrite /pseries_diffs /= factS natrM invfM.
by rewrite [_.
+1%:R * _]mulrC -!mulrA [_.
+1%:R^-1 * _]mulrC mulfK.
Qed.
Lemma
series_sin_coeff0
n
: series (
sin_coeff 0)
n.
+1 = 0.
Proof.
Lemma
sin0
: sin 0 = 0.
Proof.
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.
Proof.
by rewrite /cos_coeff /= odd_double /= !mul0r. Qed.
Lemma
cos_coeff_2_0
: cos_coeff 2 0%N = 1 :> R.
Proof.
Lemma
cos_coeff_2_2
: cos_coeff 2 2%N = - 2%:R :> R.
Proof.
Lemma
cos_coeff_2_4
: cos_coeff 2 4%N = 2%:R / 3%:R :> R.
Proof.
Lemma
cos_coeffE
x
:
cos_coeff x = (
fun
n
=> (
fun
n
=> (
~~(
odd n))
%:R * (
-1)
^+ n.
/2 *
(
n`!%:R)
^-1)
n * x ^+ n).
Proof.
by apply/funext => i; rewrite /cos_coeff /= -!mulrA [_ / _]mulrC.
Qed.
Lemma
is_cvg_series_cos_coeff
x
: cvg (
series (
cos_coeff x)).
Proof.
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)).
Proof.
by apply/funext => x; rewrite -cos_coeffE. Qed.
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.
Proof.
Lemma
cvg_cos_coeff'
x
: series (
cos_coeff' x)
--> cos x.
Proof.
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).
Proof.
Lemma
series_cos_coeff0
n
: series (
cos_coeff 0)
n.
+1 = 1.
Proof.
Lemma
cos0
: cos 0 = 1.
Proof.
Global Instance
is_derive_sin
x
: is_derive x 1 sin (
cos x).
Proof.
Lemma
derivable_sin
x
: derivable sin x 1.
Proof.
Lemma
continuous_sin
: continuous sin.
Proof.
by move=> x; apply/differentiable_continuous/derivable1_diffP/derivable_sin.
Qed.
Global Instance
is_derive_cos
x
: is_derive x 1 cos (
- (
sin x)).
Proof.
Lemma
derivable_cos
x
: derivable cos x 1.
Proof.
Lemma
continuous_cos
: continuous cos.
Proof.
by move=> x; exact/differentiable_continuous/derivable1_diffP/derivable_cos.
Qed.
Lemma
cos2Dsin2
x
: (
cos x)
^+ 2 + (
sin x)
^+ 2 = 1.
Proof.
Lemma
cos_max
x
: `| cos x | <= 1.
Proof.
Lemma
cos_geN1
x
: -1 <= cos x.
Proof.
Lemma
cos_le1
x
: cos x <= 1.
Proof.
by have /ler_normlP[] := cos_max x. Qed.
Lemma
sin_max
x
: `| sin x | <= 1.
Proof.
Lemma
sin_geN1
x
: -1 <= sin x.
Proof.
Lemma
sin_le1
x
: sin x <= 1.
Proof.
by have /ler_normlP[] := sin_max x. Qed.
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.
Proof.
Lemma
sinD
x
y
: sin (
x + y)
= sin x * cos y + cos x * sin y.
Proof.
Lemma
cosD
x
y
: cos (
x + y)
= cos x * cos y - sin x * sin y.
Proof.
Lemma
sin2cos2
x
: sin x ^+ 2 = 1 - cos x ^+ 2.
Proof.
Lemma
cos2sin2
x
: cos x ^+ 2 = 1 - sin x ^+ 2.
Proof.
Lemma
sin_mulr2n
x
: sin (
x *+ 2)
= (
cos x * sin x)
*+ 2.
Proof.
Lemma
cos_mulr2n
x
: cos (
x *+ 2)
= cos x ^+2 *+ 2 - 1.
Proof.
Fact
sinN_cosN
x
:
(
sin (
- x)
+ sin x)
^+ 2 + (
cos (
- x)
- cos x)
^+ 2 = 0.
Proof.
Lemma
sinN
x
: sin (
- x)
= - sin x.
Proof.
Lemma
cosN
x
: cos (
- x)
= cos x.
Proof.
Lemma
sin_sg
x
y
: sin (
Num.sg x * y)
= Num.sg x * sin y.
Proof.
by case: sgrP; rewrite ?mul1r ?mulN1r ?sinN // !mul0r sin0. Qed.
Lemma
cos_sg
x
y
: x != 0 -> cos (
Num.sg x * y)
= cos y.
Proof.
by case: sgrP; rewrite ?mul1r ?mulN1r ?cosN. Qed.
Lemma
cosB
x
y
: cos (
x - y)
= cos x * cos y + sin x * sin y.
Proof.
Lemma
sinB
x
y
: sin (
x - y)
= sin x * cos y - cos x * sin y.
Proof.
Lemma
norm_cos_eq1
x
: (
`|cos x| == 1)
= (
sin x == 0).
Proof.
Lemma
norm_sin_eq1
x
: (
`|sin x| == 1)
= (
cos x == 0).
Proof.
Lemma
cos1sin0
x
: `|cos x| = 1 -> sin x = 0.
Proof.
Lemma
sin1cos0
x
: `|sin x| = 1 -> cos x = 0.
Proof.
Lemma
sin0cos1
x
: sin x = 0 -> `|cos x| = 1.
Proof.
by move/eqP; rewrite -norm_cos_eq1 => /eqP. Qed.
Lemma
cos_norm
x
: cos `|x| = cos x.
Proof.
by case: (
ler0P x)
; rewrite ?cosN. Qed.
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].
Proof.
Lemma
cos2_lt0
: cos 2 < 0 :> R.
Proof.
Lemma
sin2_gt0
x
: 0 < x < 2 -> 0 < sin x.
Proof.
Lemma
cos1_gt0
: cos 1 > 0 :> R.
Proof.
Lemma
cos_exists
: exists2
pih
: R, 1 <= pih <= 2 & cos pih = 0.
Proof.
Lemma
cos_02_uniq
x
y
:
0 <= x <= 2 -> cos x = 0 -> 0 <= y <= 2 -> cos y = 0 -> x = y.
Proof.
wlog xLy : x y / x <= y => [H xB cx0 yB cy0|].
by case: (
lerP x y)
=> [/H //| /ltW /H H1]; [exact|exact/esym/H1].
move=> /andP[x_ge0 x_le2] cx0 /andP[y_ge0 y_le2] cy0.
case: (
x =P y)
=> // /eqP xDy.
have xLLs : x < y by rewrite le_eqVlt (
negPf xDy)
in xLy.
have /(
Rolle xLLs)
[x1 _|x1|x1 x1I [_ x1D]] : cos x = cos y by rewrite cy0.
- exact: derivable_cos.
- by apply/continuous_subspaceT => ?; exact: continuous_cos.
- have [_ /esym/eqP] := is_derive_cos x1; rewrite x1D oppr_eq0 => /eqP Hs.
suff : 0 < sin x1 by rewrite Hs ltxx.
apply/sin2_gt0/andP; split.
+ by rewrite (
le_lt_trans x_ge0)
// (
itvP x1I).
+ by rewrite (
lt_le_trans _ y_le2)
// (
itvP x1I).
Qed.
Lemma
pihalf_02_cos_pihalf
: 0 <= pi / 2 <= 2 /\ cos (
pi / 2)
= 0.
Proof.
#[deprecated(
note="Use pihalf_ge1 and pihalf_lt2 instead")
]
Lemma
pihalf_02
: 0 < pi / 2 < 2.
Proof.
Let
pihalf_12
: 1 <= pi / 2 < 2.
Proof.
Lemma
pihalf_ge1
: 1 <= pi / 2.
Proof.
Lemma
pihalf_lt2
: pi / 2 < 2.
Proof.
Lemma
pi_ge2
: 2 <= pi.
Proof.
Lemma
pi_gt0
: 0 < pi
Proof.
Lemma
pi_ge0
: 0 <= pi
Proof.
Lemma
sin_gt0_pihalf
x
: 0 < x < pi / 2 -> 0 < sin x.
Proof.
Lemma
cos_gt0_pihalf
x
: -(
pi / 2)
< x < pi / 2 -> 0 < cos x.
Proof.
Lemma
cos_pihalf
: cos (
pi / 2)
= 0
Proof.
Lemma
sin_pihalf
: sin (
pi / 2)
= 1.
Proof.
Lemma
cos_ge0_pihalf
x
: -(
pi / 2)
<= x <= pi / 2 -> 0 <= cos x.
Proof.
Lemma
cospi
: cos pi = - 1.
Proof.
Lemma
sinpi
: sin pi = 0.
Proof.
Lemma
cos2pi
: cos (
pi *+ 2)
= 1.
Proof.
Lemma
sin2pi
: sin (
pi *+ 2)
= 0.
Proof.
Lemma
sinDpi
: alternating sin pi.
Proof.
Lemma
cosDpi
: alternating cos pi.
Proof.
Lemma
sinD2pi
: periodic sin (
pi *+ 2).
Proof.
Lemma
cosD2pi
: periodic cos (
pi *+ 2).
Proof.
Lemma
cosDpihalf
a
: cos (
a + pi / 2)
= - sin a.
Proof.
Lemma
cosBpihalf
a
: cos (
a - pi / 2)
= sin a.
Proof.
Lemma
sinDpihalf
a
: sin (
a + pi / 2)
= cos a.
Proof.
Lemma
sinBpihalf
a
: sin (
a - pi / 2)
= - cos a.
Proof.
Lemma
sin_ge0_pi
x
: 0 <= x <= pi -> 0 <= sin x.
Proof.
Lemma
sin_gt0_pi
x
: 0 < x < pi -> 0 < sin x.
Proof.
Lemma
ltr_cos
: {in `[0, pi] &, {mono cos :
x
y
/~ y < x}}.
Proof.
Lemma
ltr_sin
: {in `[ (
- (
pi/2))
, pi/2] &, {mono sin :
x
y
/ x < y}}.
Proof.
Lemma
cos_inj
: {in `[0,pi] &, injective (
@cos R)
}.
Proof.
move=> x y x0pi y0pi xy; apply/eqP; rewrite eq_le; apply/andP; split.
- by have := ltr_cos y0pi x0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt.
- by have := ltr_cos x0pi y0pi; rewrite xy ltxx => /esym/negbT; rewrite -leNgt.
Qed.
Lemma
sin_inj
: {in `[(
- (
pi/2))
, (
pi/2)
] &, injective sin}.
Proof.
move=> x y /itvP xpi /itvP ypi sinE; have : - sin x = - sin y by rewrite sinE.
rewrite -!cosDpihalf => /cos_inj h; apply/(
addIr (
pi/2))
/h; rewrite !in_itv/=.
- by rewrite -ler_subl_addr sub0r xpi/= [leRHS]splitr ler_add2r xpi.
- by rewrite -ler_subl_addr sub0r ypi/= [leRHS]splitr ler_add2r ypi.
Qed.
End Pi.
Arguments pi {R}.
Section
Tan
.
Variable
R
: realType.
Definition
tan
(
x
: R)
:= sin x / cos x.
Lemma
tan0
: tan 0 = 0 :> R.
Proof.
Lemma
tanpi
: tan pi = 0.
Proof.
Lemma
tanN
x
: tan (
- x)
= - tan x.
Proof.
Lemma
tanD
x
y
: cos x != 0 -> cos y != 0 ->
tan (
x + y)
= (
tan x + tan y)
/ (
1 - tan x * tan y).
Proof.
move=> cxNZ cyNZ.
rewrite /tan sinD cosD !addf_div // [sin y * cos x]mulrC -!mulrA -invfM.
congr (
_ / _).
rewrite mulrBr mulr1 !mulrA.
rewrite -[_ * _ * sin x]mulrA [cos x * (
_ * _)
]mulrC mulfK //.
by rewrite -[_ * _ * sin y]mulrA [cos y * (
_ * _)
]mulrC mulfK.
Qed.
Lemma
tan_mulr2n
x
:
cos x != 0 -> tan (
x *+ 2)
= tan x *+ 2 / (
1 - tan x ^+ 2).
Proof.
Lemma
cos2_tan2
x
: cos x != 0 -> (
cos x)
^- 2 = 1 + (
tan x)
^+ 2.
Proof.
Lemma
tan_pihalf
: tan (
pi / 2)
= 0.
Proof.
Lemma
tan_piquarter
: tan (
pi / 4%:R)
= 1.
Proof.
Lemma
tanDpi
x
: tan (
x + pi)
= tan x.
Proof.
Lemma
continuous_tan
x
: cos x != 0 -> {for x, continuous tan}.
Proof.
Lemma
is_derive_tan
x
:
cos x != 0 -> is_derive x 1 tan ((
cos x)
^-2).
Proof.
Lemma
derivable_tan
x
: cos x != 0 -> derivable tan x 1.
Proof.
by move=> /is_derive_tan[]. Qed.
Lemma
ltr_tan
: {in `](
- (
pi/2))
, (
pi/2)
[ &, {mono tan :
x
y
/ x < y}}.
Proof.
move=> x y; wlog xLy : x y / x <= y => [H xB yB|/itvP xB /itvP yB].
case: (
lerP x y)
=> [/H //->//|yLx].
by rewrite !ltNge ltW ?(
ltW yLx)
// H // ltW.
case: (
x =P y)
=> [->| /eqP xDy]; first by rewrite ltxx.
have xLLs : x < y by rewrite le_eqVlt (
negPf xDy)
in xLy.
rewrite -subr_gt0 xLLs; rewrite -subr_gt0 in xLLs; apply/idP.
have [x1 /itvP x1I|z |] := @MVT_segment _ tan (
fun
x
=> (
cos x)
^-2)
_ _ xLy.
- apply: is_derive_tan.
rewrite gt_eqF // cos_gt0_pihalf // (
@lt_le_trans _ _ x)
?x1I ?xB//=.
by rewrite (
@le_lt_trans _ _ y)
?x1I ?yB.
- apply/continuous_in_subspaceT => ? -/[!(
@mem_setE R)
] /itvP inI.
apply: continuous_tan; rewrite gt_eqF// cos_gt0_pihalf//.
by rewrite (
@lt_le_trans _ _ x)
?xB ?inI// (
@le_lt_trans _ _ y)
?yB ?inI.
- move=> x1 /itvP x1I ->.
rewrite mulr_gt0 // invr_gt0 // exprn_gte0 // cos_gt0_pihalf //.
by rewrite (
@lt_le_trans _ _ x)
?x1I ?xB//= (
@le_lt_trans _ _ y)
?x1I ?yB.
Qed.
Lemma
tan_inj
: {in `](
- (
pi/2))
, (
pi/2)
[ &, injective tan}.
Proof.
move=> x y xB yB tanE.
by case: (
ltrgtP x y)
; rewrite // -ltr_tan ?tanE ?ltxx.
Qed.
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.
Proof.
Lemma
acos_ge0
x
: -1 <= x <= 1 -> 0 <= acos x.
Proof.
by move=> /acos_def[/andP[]]. Qed.
Lemma
acos_lepi
x
: -1 <= x <= 1 -> acos x <= pi.
Proof.
by move=> /acos_def[/andP[]]. Qed.
Lemma
acosK
: {in `[(
-1)
,1], cancel acos cos}.
Proof.
by move=> x; rewrite in_itv/==> /acos_def[/andP[]]. Qed.
Lemma
acos_gt0
x
: -1 <= x < 1 -> 0 < acos x.
Proof.
Lemma
acos_ltpi
x
: -1 < x <= 1 -> acos x < pi.
Proof.
Lemma
cosK
: {in `[0, pi], cancel cos acos}.
Proof.
move=> x xB; apply: cos_inj => //; rewrite ?acosK//; last first.
by move: xB; rewrite !in_itv/= => /andP[? ?];rewrite cos_geN1 cos_le1.
move: xB; rewrite !in_itv/= => /andP[? ?].
by rewrite acos_ge0 ?acos_lepi ?cos_geN1 ?cos_le1.
Qed.
Lemma
acos1
: acos (
1 : R)
= 0.
Proof.
Lemma
acos0
: acos (
0 : R)
= pi / 2%:R.
Proof.
Lemma
acosN
a
: -1 <= a <= 1 -> acos (
- a)
= pi - acos a.
Proof.
Lemma
acosN1
: acos (
- 1)
= (
pi : R).
Proof.
Lemma
cosKN
a
: - pi <= a <= 0 -> acos (
cos a)
= - a.
Proof.
Lemma
sin_acos
x
: -1 <= x <= 1 -> sin (
acos x)
= Num.sqrt (
1 - x^+2).
Proof.
Lemma
continuous_acos
x
: -1 < x < 1 -> {for x, continuous acos}.
Proof.
Lemma
is_derive1_acos
(
x
: R)
:
-1 < x < 1 -> is_derive x 1 acos (
- (
Num.sqrt (
1 - x ^+ 2))
^-1).
Proof.
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.
Proof.
Lemma
asin_geNpi2
x
: -1 <= x <= 1 -> -(
pi / 2)
<= asin x.
Proof.
by move=> /asin_def[/andP[]]. Qed.
Lemma
asin_lepi2
x
: -1 <= x <= 1 -> asin x <= pi / 2.
Proof.
by move=> /asin_def[/andP[]]. Qed.
Lemma
asinK
: {in `[(
-1)
,1], cancel asin sin}.
Proof.
by move=> x; rewrite in_itv/= => /asin_def[/andP[]]. Qed.
Lemma
asin_ltpi2
x
: -1 <= x < 1 -> asin x < pi/2.
Proof.
Lemma
asin_gtNpi2
x
: -1 < x <= 1 -> - (
pi / 2)
< asin x.
Proof.
Lemma
sinK
: {in `[(
- (
pi / 2))
, pi / 2], cancel sin asin}.
Proof.
Lemma
cos_asin
x
: -1 <= x <= 1 -> cos (
asin x)
= Num.sqrt (
1 - x^+2).
Proof.
Lemma
continuous_asin
x
: -1 < x < 1 -> {for x, continuous asin}.
Proof.
Lemma
is_derive1_asin
(
x
: R)
:
-1 < x < 1 -> is_derive x 1 asin ((
Num.sqrt (
1 - x ^+ 2))
^-1).
Proof.
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.
Proof.
Lemma
atan_gtNpi2
x
: - (
pi / 2)
< atan x.
Proof.
by case: (
atan_def x)
=> [] /andP[]. Qed.
Lemma
atan_ltpi2
x
: atan x < pi / 2.
Proof.
by case: (
atan_def x)
=> [] /andP[]. Qed.
Lemma
atanK
: cancel atan tan.
Proof.
Lemma
atan0
: atan 0 = 0 :> R.
Proof.
Lemma
atan1
: atan 1 = pi / 4%:R :> R.
Proof.
Lemma
atanN
x
: atan (
- x)
= - atan x.
Proof.
Lemma
tanK
: {in `](
- (
pi / 2))
, (
pi / 2)
[ , cancel tan atan}.
Proof.
Lemma
continuous_atan
x
: {for x, continuous atan}.
Proof.
Lemma
cos_atan
x
: cos (
atan x)
= (
Num.sqrt (
1 + x ^+ 2))
^-1.
Proof.
Global Instance
is_derive1_atan
(
x
: R)
: is_derive x 1 atan (
1 + x ^+ 2)
^-1.
Proof.
End Atan.