Library Coq.Reals.Ratan
Require
Import
Lra
.
Require
Import
Rbase
.
Require
Import
PSeries_reg
.
Require
Import
Rtrigo1
.
Require
Import
Rtrigo_facts
.
Require
Import
Ranalysis_reg
.
Require
Import
Rfunctions
.
Require
Import
AltSeries
.
Require
Import
Rseries
.
Require
Import
SeqProp
.
Require
Import
Ranalysis5
.
Require
Import
SeqSeries
.
Require
Import
PartSum
.
Require
Import
Lia
.
Local Open
Scope
R_scope
.
Preliminaries
Various generic lemmas which probably should go somewhere else
Lemma
Boule_half_to_interval
:
forall
x
,
Boule
(
/
2)
posreal_half
x
->
0
<=
x
<=
1.
Lemma
Boule_lt
:
forall
c
r
x
,
Boule
c
r
x
->
Rabs
x
<
Rabs
c
+
r
.
Lemma
Un_cv_ext
:
forall
un
vn
,
(
forall
n
,
un
n
=
vn
n
)
->
forall
l
,
Un_cv
un
l
->
Un_cv
vn
l
.
Lemma
Alt_first_term_bound
:
forall
f
l
N
n
,
Un_decreasing
f
->
Un_cv
f
0
->
Un_cv
(
sum_f_R0
(
tg_alt
f
))
l
->
(
N
<=
n
)%
nat
->
R_dist
(
sum_f_R0
(
tg_alt
f
)
n
)
l
<=
f
N
.
Lemma
Alt_CVU
:
forall
(
f
:
nat
->
R
->
R
)
g
h
c
r
,
(
forall
x
,
Boule
c
r
x
->
Un_decreasing
(
fun
n
=>
f
n
x
)
)
->
(
forall
x
,
Boule
c
r
x
->
Un_cv
(
fun
n
=>
f
n
x
) 0
)
->
(
forall
x
,
Boule
c
r
x
->
Un_cv
(
sum_f_R0
(
tg_alt
(
fun
i
=>
f
i
x
))) (
g
x
)
)
->
(
forall
x
n
,
Boule
c
r
x
->
f
n
x
<=
h
n
)
->
(
Un_cv
h
0
)
->
CVU
(
fun
N
x
=>
sum_f_R0
(
tg_alt
(
fun
i
=>
f
i
x
))
N
)
g
c
r
.
Lemma
pow2_ge_0
:
forall
x
, 0
<=
x
^
2.
Lemma
pow2_abs
:
forall
x
,
Rabs
x
^
2
=
x
^
2.
Properties of tangent
Derivative of tangent
Lemma
derivable_pt_tan
:
forall
x
,
-
PI
/
2
<
x
<
PI
/
2
->
derivable_pt
tan
x
.
Lemma
derive_pt_tan
:
forall
x
,
forall
(
Pr1
:
-
PI
/
2
<
x
<
PI
/
2),
derive_pt
tan
x
(
derivable_pt_tan
x
Pr1
)
=
1
+
(
tan
x
)^
2.
Proof that tangent is a bijection
Lemma
derive_increasing_interv
:
forall
(
a
b
:
R
) (
f
:
R
->
R
),
a
<
b
->
forall
(
pr
:
forall
x
,
a
<
x
<
b
->
derivable_pt
f
x
),
(
forall
t
:
R
,
forall
(
t_encad
:
a
<
t
<
b
), 0
<
derive_pt
f
t
(
pr
t
t_encad
)
)
->
forall
x
y
:
R
,
a
<
x
<
b
->
a
<
y
<
b
->
x
<
y
->
f
x
<
f
y
.
Lemma
PI2_lower_bound
:
forall
x
, 0
<
x
<
2
->
0
<
cos
x
->
x
<
PI
/
2.
Lemma
PI2_3_2
: 3
/
2
<
PI
/
2.
Lemma
PI2_1
: 1
<
PI
/
2.
Lemma
tan_increasing
:
forall
x
y
,
-
PI
/
2
<
x
->
x
<
y
->
y
<
PI
/
2
->
tan
x
<
tan
y
.
Lemma
tan_inj
:
forall
x
y
,
-
PI
/
2
<
x
<
PI
/
2
->
-
PI
/
2
<
y
<
PI
/
2
->
tan
x
=
tan
y
->
x
=
y
.
Notation
tan_is_inj
:=
tan_inj
(
only
parsing
).
Lemma
exists_atan_in_frame
:
forall
lb
ub
y
,
lb
<
ub
->
-
PI
/
2
<
lb
->
ub
<
PI
/
2
->
tan
lb
<
y
<
tan
ub
->
{
x
|
lb
<
x
<
ub
/\
tan
x
=
y
}
.
Definition of arctangent
Definition of arctangent as the reciprocal function of tangent and proof of this status
Lemma
tan_1_gt_1
:
tan
1
>
1.
Definition
frame_tan
y
:
{
x
|
0
<
x
<
PI
/
2
/\
Rabs
y
<
tan
x
}
.
Lemma
ub_opp
:
forall
x
,
x
<
PI
/
2
->
-
PI
/
2
<
-
x
.
Lemma
pos_opp_lt
:
forall
x
, 0
<
x
->
-
x
<
x
.
Lemma
tech_opp_tan
:
forall
x
y
,
-
tan
x
<
y
->
tan
(
-
x
)
<
y
.
Definition
pre_atan
(
y
:
R
) :
{
x
:
R
|
-
PI
/
2
<
x
<
PI
/
2
/\
tan
x
=
y
}
.
Definition
atan
x
:=
let
(
v
,
_
) :=
pre_atan
x
in
v
.
Lemma
atan_bound
:
forall
x
,
-
PI
/
2
<
atan
x
<
PI
/
2.
Lemma
tan_atan
:
forall
x
,
tan
(
atan
x
)
=
x
.
Notation
atan_right_inv
:=
tan_atan
(
only
parsing
).
Lemma
atan_opp
:
forall
x
,
atan
(
-
x
)
=
-
atan
x
.
Lemma
derivable_pt_atan
:
forall
x
,
derivable_pt
atan
x
.
Lemma
atan_increasing
:
forall
x
y
,
x
<
y
->
atan
x
<
atan
y
.
Lemma
atan_0
:
atan
0
=
0.
Lemma
atan_eq0
:
forall
x
,
atan
x
=
0
->
x
=
0.
Lemma
atan_1
:
atan
1
=
PI
/
4.
Lemma
atan_tan
:
forall
x
,
-
(
PI
/
2
)
<
x
<
PI
/
2
->
atan
(
tan
x
)
=
x
.
Lemma
atan_inv
:
forall
x
, (0
<
x
)%
R
->
atan
(
/
x
)
=
(
PI
/
2
-
atan
x
)%
R
.
Derivative of arctangent
Lemma
derive_pt_atan
:
forall
x
,
derive_pt
atan
x
(
derivable_pt_atan
x
)
=
1
/
(
1
+
x
²
)
.
Lemma
derivable_pt_lim_atan
:
forall
x
,
derivable_pt_lim
atan
x
(
/
(
1
+
x
^
2
)
).
Definition of the arctangent function as the sum of the arctan power series
Definition
Ratan_seq
x
:=
fun
n
=> (
x
^
(
2
*
n
+
1
)
/
INR
(2
*
n
+
1))%
R
.
Lemma
Ratan_seq_decreasing
:
forall
x
, (0
<=
x
<=
1)%
R
->
Un_decreasing
(
Ratan_seq
x
).
Lemma
Ratan_seq_converging
:
forall
x
, (0
<=
x
<=
1)%
R
->
Un_cv
(
Ratan_seq
x
) 0.
Definition
ps_atan_exists_01
(
x
:
R
) (
Hx
:0
<=
x
<=
1) :
{
l
:
R
|
Un_cv
(
fun
N
:
nat
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
l
}
.
Lemma
Ratan_seq_opp
:
forall
x
n
,
Ratan_seq
(
-
x
)
n
=
-
Ratan_seq
x
n
.
Lemma
sum_Ratan_seq_opp
:
forall
x
n
,
sum_f_R0
(
tg_alt
(
Ratan_seq
(
-
x
)))
n
=
-
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
n
.
Definition
ps_atan_exists_1
(
x
:
R
) (
Hx
: -1
<=
x
<=
1) :
{
l
:
R
|
Un_cv
(
fun
N
:
nat
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
l
}
.
Definition
in_int
(
x
:
R
) :
{
-1
<=
x
<=
1
}+{
~
-1
<=
x
<=
1
}
.
Definition
ps_atan
(
x
:
R
) :
R
:=
match
in_int
x
with
left
h
=>
let
(
v
,
_
) :=
ps_atan_exists_1
x
h
in
v
|
right
h
=>
atan
x
end
.
Proof of the equivalence of the two definitions between -1 and 1
Lemma
ps_atan0_0
:
ps_atan
0
=
0.
Lemma
ps_atan_exists_1_opp
:
forall
x
h
h'
,
proj1_sig
(
ps_atan_exists_1
(
-
x
)
h
)
=
-(
proj1_sig
(
ps_atan_exists_1
x
h'
)
)
.
Lemma
ps_atan_opp
:
forall
x
,
ps_atan
(
-
x
)
=
-
ps_atan
x
.
atan = ps_atan
Lemma
ps_atanSeq_continuity_pt_1
:
forall
(
N
:
nat
) (
x
:
R
),
0
<=
x
->
x
<=
1
->
continuity_pt
(
fun
x
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
x
.
Definition of ps_atan's derivative
Definition
Datan_seq
:=
fun
(
x
:
R
) (
n
:
nat
) =>
x
^
(
2
*
n
)
.
Lemma
pow_lt_1_compat
:
forall
x
n
,
0
<=
x
<
1
->
(0
<
n
)%
nat
->
0
<=
x
^
n
<
1.
Lemma
Datan_seq_Rabs
:
forall
x
n
,
Datan_seq
(
Rabs
x
)
n
=
Datan_seq
x
n
.
Lemma
Datan_seq_pos
:
forall
x
n
, 0
<
x
->
0
<
Datan_seq
x
n
.
Lemma
Datan_sum_eq
:
forall
x
n
,
sum_f_R0
(
tg_alt
(
Datan_seq
x
))
n
=
(
1
-
(
-
x
^
2
)
^
S
n
)/(
1
+
x
^
2
)
.
Lemma
Datan_seq_increasing
:
forall
x
y
n
,
(
n
>
0)%
nat
->
0
<=
x
<
y
->
Datan_seq
x
n
<
Datan_seq
y
n
.
Lemma
Datan_seq_decreasing
:
forall
x
, -1
<
x
->
x
<
1
->
Un_decreasing
(
Datan_seq
x
).
Lemma
Datan_seq_CV_0
:
forall
x
, -1
<
x
->
x
<
1
->
Un_cv
(
Datan_seq
x
) 0.
Lemma
Datan_lim
:
forall
x
, -1
<
x
->
x
<
1
->
Un_cv
(
fun
N
:
nat
=>
sum_f_R0
(
tg_alt
(
Datan_seq
x
))
N
) (
/
(
1
+
x
^
2
)
).
Lemma
Datan_CVU_prelim
:
forall
c
(
r
:
posreal
),
Rabs
c
+
r
<
1
->
CVU
(
fun
N
x
=>
sum_f_R0
(
tg_alt
(
Datan_seq
x
))
N
)
(
fun
y
:
R
=>
/
(
1
+
y
^
2
)
)
c
r
.
Lemma
Datan_is_datan
:
forall
(
N
:
nat
) (
x
:
R
),
-1
<=
x
->
x
<
1
->
derivable_pt_lim
(
fun
x
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
x
(
sum_f_R0
(
tg_alt
(
Datan_seq
x
))
N
).
Lemma
Ratan_CVU'
:
CVU
(
fun
N
x
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
ps_atan
(
/
2)
posreal_half
.
Lemma
Ratan_CVU
:
CVU
(
fun
N
x
=>
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
N
)
ps_atan
0 (
mkposreal
1
Rlt_0_1
).
Lemma
Alt_PI_tg
:
forall
n
,
PI_tg
n
=
Ratan_seq
1
n
.
Lemma
Ratan_is_ps_atan
:
forall
eps
,
eps
>
0
->
exists
N
,
forall
n
, (
n
>=
N
)%
nat
->
forall
x
, -1
<
x
->
x
<
1
->
Rabs
(
sum_f_R0
(
tg_alt
(
Ratan_seq
x
))
n
-
ps_atan
x
)
<
eps
.
Lemma
Datan_continuity
:
continuity
(
fun
x
=>
/(
1
+
x
^
2
)
).
Lemma
derivable_pt_lim_ps_atan
:
forall
x
, -1
<
x
<
1
->
derivable_pt_lim
ps_atan
x
((
fun
y
=>
/(
1
+
y
^
2
)
)
x
).
Lemma
derivable_pt_ps_atan
:
forall
x
, -1
<
x
<
1
->
derivable_pt
ps_atan
x
.
Lemma
ps_atan_continuity_pt_1
:
forall
eps
:
R
,
eps
>
0
->
exists
alp
:
R
,
alp
>
0
/\
(
forall
x
,
x
<
1
->
0
<
x
->
R_dist
x
1
<
alp
->
dist
R_met
(
ps_atan
x
) (
Alt_PI
/
4)
<
eps
)
.
Lemma
Datan_eq_DatanSeq_interv
:
forall
x
, -1
<
x
<
1
->
forall
(
Pratan
:
derivable_pt
ps_atan
x
) (
Prmymeta
:
derivable_pt
atan
x
),
derive_pt
ps_atan
x
Pratan
=
derive_pt
atan
x
Prmymeta
.
Lemma
atan_eq_ps_atan
:
forall
x
, 0
<
x
<
1
->
atan
x
=
ps_atan
x
.
Theorem
Alt_PI_eq
:
Alt_PI
=
PI
.
Lemma
PI_ineq
:
forall
N
:
nat
,
sum_f_R0
(
tg_alt
PI_tg
) (
S
(2
*
N
))
<=
PI
/
4
<=
sum_f_R0
(
tg_alt
PI_tg
) (2
*
N
).
Relation between arctangent and sine and cosine
Lemma
sin_atan
:
forall
x
,
sin
(
atan
x
)
=
x
/
sqrt
(1
+
x
²
).
Lemma
cos_atan
:
forall
x
,
cos
(
atan
x
)
=
1
/
sqrt
(1
+
x
²
).
Definition of arcsine based on arctangent
asin is defined by cases so that it is defined in the full range from -1 .. 1
Definition
asin
x
:=
if
Rle_dec
x
(-1)
then
-
(
PI
/
2
)
else
if
Rle_dec
1
x
then
PI
/
2
else
atan
(
x
/
sqrt
(1
-
x
²
)).
Relation between arcsin and arctangent
Lemma
asin_atan
:
forall
x
, -1
<
x
<
1
->
asin
x
=
atan
(
x
/
sqrt
(1
-
x
²
)).
arcsine of specific values
Lemma
asin_0
:
asin
0
=
0.
Lemma
asin_1
:
asin
1
=
PI
/
2.
Lemma
asin_inv_sqrt2
:
asin
(
/
sqrt
2)
=
PI
/
4.
Lemma
asin_opp
:
forall
x
,
asin
(
-
x
)
=
-
asin
x
.
Bounds of arcsine
Lemma
asin_bound
:
forall
x
,
-
(
PI
/
2
)
<=
asin
x
<=
PI
/
2.
Lemma
asin_bound_lt
:
forall
x
, -1
<
x
<
1
->
-
(
PI
/
2
)
<
asin
x
<
PI
/
2.
arcsine is the left and right inverse of sine
Lemma
sin_asin
:
forall
x
, -1
<=
x
<=
1
->
sin
(
asin
x
)
=
x
.
Lemma
asin_sin
:
forall
x
,
-(
PI
/
2
)
<=
x
<=
PI
/
2
->
asin
(
sin
x
)
=
x
.
Relation between arcsin, cosine and tangent
Lemma
cos_asin
:
forall
x
, -1
<=
x
<=
1
->
cos
(
asin
x
)
=
sqrt
(1
-
x
²
).
Lemma
tan_asin
:
forall
x
, -1
<=
x
<=
1
->
tan
(
asin
x
)
=
x
/
sqrt
(1
-
x
²
).
Derivative of arcsine
Lemma
derivable_pt_asin
:
forall
x
, -1
<
x
<
1
->
derivable_pt
asin
x
.
Lemma
derive_pt_asin
:
forall
(
x
:
R
) (
Hxrange
: -1
<
x
<
1),
derive_pt
asin
x
(
derivable_pt_asin
x
Hxrange
)
=
1
/
sqrt
(1
-
x
²
).
Definition of arccosine based on arctangent
acos is defined by cases so that it is defined in the full range from -1 .. 1
Definition
acos
x
:=
if
Rle_dec
x
(-1)
then
PI
else
if
Rle_dec
1
x
then
0
else
PI
/
2
-
atan
(
x
/
sqrt
(1
-
x
²
)).
Relation between arccosine, arcsine and arctangent
Lemma
acos_atan
:
forall
x
, 0
<
x
->
acos
x
=
atan
(
sqrt
(1
-
x
²
)
/
x
).
Lemma
acos_asin
:
forall
x
, -1
<=
x
<=
1
->
acos
x
=
PI
/
2
-
asin
x
.
Lemma
asin_acos
:
forall
x
, -1
<=
x
<=
1
->
asin
x
=
PI
/
2
-
acos
x
.
arccosine of specific values
Lemma
acos_0
:
acos
0
=
PI
/
2.
Lemma
acos_1
:
acos
1
=
0.
Lemma
acos_opp
:
forall
x
,
acos
(
-
x
)
=
PI
-
acos
x
.
Lemma
acos_inv_sqrt2
:
acos
(
/
sqrt
2)
=
PI
/
4.
Bounds of arccosine
Lemma
acos_bound
:
forall
x
,
0
<=
acos
x
<=
PI
.
Lemma
acos_bound_lt
:
forall
x
, -1
<
x
<
1
->
0
<
acos
x
<
PI
.
arccosine is the left and right inverse of cosine
Lemma
cos_acos
:
forall
x
, -1
<=
x
<=
1
->
cos
(
acos
x
)
=
x
.
Lemma
acos_cos
:
forall
x
, 0
<=
x
<=
PI
->
acos
(
cos
x
)
=
x
.
Relation between arccosine, sine and tangent
Lemma
sin_acos
:
forall
x
, -1
<=
x
<=
1
->
sin
(
acos
x
)
=
sqrt
(1
-
x
²
).
Lemma
tan_acos
:
forall
x
, -1
<=
x
<=
1
->
tan
(
acos
x
)
=
sqrt
(1
-
x
²
)
/
x
.
Derivative of arccosine
Lemma
derivable_pt_acos
:
forall
x
, -1
<
x
<
1
->
derivable_pt
acos
x
.
Lemma
derive_pt_acos
:
forall
(
x
:
R
) (
Hxrange
: -1
<
x
<
1),
derive_pt
acos
x
(
derivable_pt_acos
x
Hxrange
)
=
-1
/
sqrt
(1
-
x
²
).