Library Coq.Reals.Rtrigo1
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Export Rtrigo_fun.
Require Export Rtrigo_def.
Require Export Rtrigo_alt.
Require Export Cos_rel.
Require Export Cos_plus.
Require Import ZArith_base.
Require Import Zcomplements.
Require Import Classical_Prop.
Require Import Fourier.
Require Import Ranalysis1.
Require Import Rsqrt_def.
Require Import PSeries_reg.
Local Open Scope nat_scope.
Local Open Scope R_scope.
Lemma CVN_R_cos :
forall fn:
nat ->
R ->
R,
fn = (fun (
N:
nat) (
x:
R) =>
(-1
) ^ N / INR (
fact (2
* N))
* x ^ (2
* N)) ->
CVN_R fn.
Lemma continuity_cos :
continuity cos.
Lemma sin_gt_cos_7_8 :
sin (7
/ 8)
> cos (7
/ 8).
Definition PI_2_aux :
{z | 7
/8
<= z <= 7
/4
/\ -cos z = 0
}.
Qed.
Definition PI2 :=
proj1_sig PI_2_aux.
Definition PI := 2
* PI2.
Lemma cos_pi2 :
cos PI2 = 0.
Lemma pi2_int : 7
/8
<= PI2 <= 7
/4.
Lemma cos_minus :
forall x y:
R,
cos (
x - y)
= cos x * cos y + sin x * sin y.
Lemma sin2_cos2 :
forall x:
R,
Rsqr (
sin x)
+ Rsqr (
cos x)
= 1.
Lemma cos2 :
forall x:
R,
Rsqr (
cos x)
= 1
- Rsqr (
sin x).
Lemma sin2 :
forall x:
R,
Rsqr (
sin x)
= 1
- Rsqr (
cos x).
Lemma cos_PI2 :
cos (
PI / 2)
= 0.
Lemma sin_pos_tech :
forall x, 0
< x < 2 -> 0
< sin x.
Lemma sin_PI2 :
sin (
PI / 2)
= 1.
Lemma PI_RGT_0 :
PI > 0.
Lemma PI_4 :
PI <= 4.
Lemma PI_neq0 :
PI <> 0.
Lemma cos_PI :
cos PI = -1.
Lemma sin_PI :
sin PI = 0.
Lemma sin_bound :
forall (
a :
R) (
n :
nat), 0
<= a ->
a <= PI ->
sin_approx a (2
* n + 1)
<= sin a <= sin_approx a (2
* (n + 1
)).
Lemma cos_bound :
forall (
a :
R) (
n :
nat),
- PI / 2
<= a ->
a <= PI / 2 ->
cos_approx a (2
* n + 1)
<= cos a <= cos_approx a (2
* (n + 1
)).
Lemma neg_cos :
forall x:
R,
cos (
x + PI)
= - cos x.
Lemma sin_cos :
forall x:
R,
sin x = - cos (
PI / 2
+ x).
Lemma sin_plus :
forall x y:
R,
sin (
x + y)
= sin x * cos y + cos x * sin y.
Lemma sin_minus :
forall x y:
R,
sin (
x - y)
= sin x * cos y - cos x * sin y.
Definition tan (
x:
R) :
R :=
sin x / cos x.
Lemma tan_plus :
forall x y:
R,
cos x <> 0 ->
cos y <> 0 ->
cos (
x + y)
<> 0 ->
1
- tan x * tan y <> 0 ->
tan (
x + y)
= (tan x + tan y) / (1
- tan x * tan y).
Some properties of cos, sin and tan
Lemma sin_2a :
forall x:
R,
sin (2
* x)
= 2
* sin x * cos x.
Lemma cos_2a :
forall x:
R,
cos (2
* x)
= cos x * cos x - sin x * sin x.
Lemma cos_2a_cos :
forall x:
R,
cos (2
* x)
= 2
* cos x * cos x - 1.
Lemma cos_2a_sin :
forall x:
R,
cos (2
* x)
= 1
- 2
* sin x * sin x.
Lemma tan_2a :
forall x:
R,
cos x <> 0 ->
cos (2
* x)
<> 0 ->
1
- tan x * tan x <> 0 ->
tan (2
* x)
= 2
* tan x / (1
- tan x * tan x).
Lemma sin_neg :
forall x:
R,
sin (
- x)
= - sin x.
Lemma cos_neg :
forall x:
R,
cos (
- x)
= cos x.
Lemma tan_0 :
tan 0
= 0.
Lemma tan_neg :
forall x:
R,
tan (
- x)
= - tan x.
Lemma tan_minus :
forall x y:
R,
cos x <> 0 ->
cos y <> 0 ->
cos (
x - y)
<> 0 ->
1
+ tan x * tan y <> 0 ->
tan (
x - y)
= (tan x - tan y) / (1
+ tan x * tan y).
Lemma cos_3PI2 :
cos (3
* (PI / 2
))
= 0.
Lemma sin_2PI :
sin (2
* PI)
= 0.
Lemma cos_2PI :
cos (2
* PI)
= 1.
Lemma neg_sin :
forall x:
R,
sin (
x + PI)
= - sin x.
Lemma sin_PI_x :
forall x:
R,
sin (
PI - x)
= sin x.
Lemma sin_period :
forall (
x:
R) (
k:
nat),
sin (
x + 2
* INR k * PI)
= sin x.
Lemma cos_period :
forall (
x:
R) (
k:
nat),
cos (
x + 2
* INR k * PI)
= cos x.
Lemma sin_shift :
forall x:
R,
sin (
PI / 2
- x)
= cos x.
Lemma cos_shift :
forall x:
R,
cos (
PI / 2
- x)
= sin x.
Lemma cos_sin :
forall x:
R,
cos x = sin (
PI / 2
+ x).
Lemma PI2_RGT_0 : 0
< PI / 2.
Lemma SIN_bound :
forall x:
R, -1
<= sin x <= 1.
Lemma COS_bound :
forall x:
R, -1
<= cos x <= 1.
Lemma cos_sin_0 :
forall x:
R,
~ (cos x = 0
/\ sin x = 0
).
Lemma cos_sin_0_var :
forall x:
R,
cos x <> 0
\/ sin x <> 0.
Using series definitions of cos and sin
Increasing and decreasing of cos and sin
Theorem sin_gt_0 :
forall x:
R, 0
< x ->
x < PI -> 0
< sin x.
Theorem cos_gt_0 :
forall x:
R,
- (PI / 2
) < x ->
x < PI / 2 -> 0
< cos x.
Lemma sin_ge_0 :
forall x:
R, 0
<= x ->
x <= PI -> 0
<= sin x.
Lemma cos_ge_0 :
forall x:
R,
- (PI / 2
) <= x ->
x <= PI / 2 -> 0
<= cos x.
Lemma sin_le_0 :
forall x:
R,
PI <= x ->
x <= 2
* PI ->
sin x <= 0.
Lemma cos_le_0 :
forall x:
R,
PI / 2
<= x ->
x <= 3
* (PI / 2
) ->
cos x <= 0.
Lemma sin_lt_0 :
forall x:
R,
PI < x ->
x < 2
* PI ->
sin x < 0.
Lemma sin_lt_0_var :
forall x:
R,
- PI < x ->
x < 0 ->
sin x < 0.
Lemma cos_lt_0 :
forall x:
R,
PI / 2
< x ->
x < 3
* (PI / 2
) ->
cos x < 0.
Lemma tan_gt_0 :
forall x:
R, 0
< x ->
x < PI / 2 -> 0
< tan x.
Lemma tan_lt_0 :
forall x:
R,
- (PI / 2
) < x ->
x < 0 ->
tan x < 0.
Lemma cos_ge_0_3PI2 :
forall x:
R, 3
* (PI / 2
) <= x ->
x <= 2
* PI -> 0
<= cos x.
Lemma form1 :
forall p q:
R,
cos p + cos q = 2
* cos (
(p - q) / 2)
* cos (
(p + q) / 2).
Lemma form2 :
forall p q:
R,
cos p - cos q = -2
* sin (
(p - q) / 2)
* sin (
(p + q) / 2).
Lemma form3 :
forall p q:
R,
sin p + sin q = 2
* cos (
(p - q) / 2)
* sin (
(p + q) / 2).
Lemma form4 :
forall p q:
R,
sin p - sin q = 2
* cos (
(p + q) / 2)
* sin (
(p - q) / 2).
Lemma sin_increasing_0 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
sin x < sin y ->
x < y.
Lemma sin_increasing_1 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
x < y ->
sin x < sin y.
Lemma sin_decreasing_0 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
sin x < sin y ->
y < x.
Lemma sin_decreasing_1 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
x < y ->
sin y < sin x.
Lemma cos_increasing_0 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
cos x < cos y ->
x < y.
Lemma cos_increasing_1 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
x < y ->
cos x < cos y.
Lemma cos_decreasing_0 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
cos x < cos y ->
y < x.
Lemma cos_decreasing_1 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
x < y ->
cos y < cos x.
Lemma tan_diff :
forall x y:
R,
cos x <> 0 ->
cos y <> 0 ->
tan x - tan y = sin (
x - y)
/ (cos x * cos y).
Lemma tan_increasing_0 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
tan x < tan y ->
x < y.
Lemma tan_increasing_1 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
x < y ->
tan x < tan y.
Lemma sin_incr_0 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
sin x <= sin y ->
x <= y.
Lemma sin_incr_1 :
forall x y:
R,
- (PI / 2
) <= x ->
x <= PI / 2 ->
- (PI / 2
) <= y ->
y <= PI / 2 ->
x <= y ->
sin x <= sin y.
Lemma sin_decr_0 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
sin x <= sin y ->
y <= x.
Lemma sin_decr_1 :
forall x y:
R,
x <= 3
* (PI / 2
) ->
PI / 2
<= x ->
y <= 3
* (PI / 2
) ->
PI / 2
<= y ->
x <= y ->
sin y <= sin x.
Lemma cos_incr_0 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
cos x <= cos y ->
x <= y.
Lemma cos_incr_1 :
forall x y:
R,
PI <= x ->
x <= 2
* PI ->
PI <= y ->
y <= 2
* PI ->
x <= y ->
cos x <= cos y.
Lemma cos_decr_0 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
cos x <= cos y ->
y <= x.
Lemma cos_decr_1 :
forall x y:
R,
0
<= x ->
x <= PI -> 0
<= y ->
y <= PI ->
x <= y ->
cos y <= cos x.
Lemma tan_incr_0 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
tan x <= tan y ->
x <= y.
Lemma tan_incr_1 :
forall x y:
R,
- (PI / 4
) <= x ->
x <= PI / 4 ->
- (PI / 4
) <= y ->
y <= PI / 4 ->
x <= y ->
tan x <= tan y.
Lemma sin_eq_0_1 :
forall x:
R, (
exists k :
Z, x = IZR k * PI) ->
sin x = 0.
Lemma sin_eq_0_0 (
x:
R) :
sin x = 0 ->
exists k :
Z, x = IZR k * PI.
Lemma cos_eq_0_0 (
x:
R) :
cos x = 0 ->
exists k :
Z, x = IZR k * PI + PI / 2.
Lemma cos_eq_0_1 (
x:
R) :
(
exists k :
Z, x = IZR k * PI + PI / 2) ->
cos x = 0.
Lemma sin_eq_O_2PI_0 (
x:
R) :
0
<= x ->
x <= 2
* PI ->
sin x = 0 ->
x = 0
\/ x = PI \/ x = 2
* PI.
Lemma sin_eq_O_2PI_1 (
x:
R) :
0
<= x ->
x <= 2
* PI ->
x = 0
\/ x = PI \/ x = 2
* PI ->
sin x = 0.
Lemma cos_eq_0_2PI_0 (
x:
R) :
0
<= x ->
x <= 2
* PI ->
cos x = 0 ->
x = PI / 2
\/ x = 3
* (PI / 2
).
Lemma cos_eq_0_2PI_1 (
x:
R) :
0
<= x ->
x <= 2
* PI ->
x = PI / 2
\/ x = 3
* (PI / 2
) ->
cos x = 0.