Library Stdlib.Reals.Ratan

From Stdlib Require Import Lra.
From Stdlib Require Import Rbase.
From Stdlib Require Import PSeries_reg.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Rtrigo_facts.
From Stdlib Require Import Ranalysis_reg.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import AltSeries.
From Stdlib Require Import Rseries.
From Stdlib Require Import SeqProp.
From Stdlib Require Import Ranalysis5.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import PartSum.
From Stdlib Require Import Lia.
From Stdlib Require Import Znat.

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.