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.