Library Stdlib.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.