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

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.