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 Lia.
Require Import Lra.
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 sin_inj x y :
-(PI/2
) <= x <= PI/2
-> -(PI/2
) <= y <= PI/2
-> sin x = sin y -> x = y.
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 cos_inj x y : 0
<= x <= PI -> 0
<= y <= PI -> cos x = cos y -> x = y.
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.