The Coq Proof Assistant

# 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.
Local Ltac Tauto.intuition_solver ::= auto with rorders real arith.

# 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 ->
Rdist (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.
Lemma sin_lt_x x : 0 < x -> sin x < x.
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 -> Rdist 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 ²).
Lemma sin_gt_x x : x < 0 -> x < sin x.