Require Import Fourier.
Require Import Rbase.
Require Import PSeries_reg.
Require Import Rtrigo1.
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.

Local Open Scope R_scope.

Lemma Ropp_div : forall x y, -x/y = -(x/y).

Definition pos_half_prf : 0 < /2.

Definition pos_half := mkposreal (/2) pos_half_prf.

Lemma Boule_half_to_interval :
  forall x , Boule (/2) pos_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.

Lemma derivable_pt_tan : forall x, -PI/2 < x < PI/2 -> derivable_pt tan x.

Lemma derive_pt_tan : forall (x:R),
 forall (Pr1: -PI/2 < x < PI/2),
 derive_pt tan x (derivable_pt_tan x Pr1) = 1 + (tan x)^2.

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:R,
    -PI/2 < x ->
    x < y ->
    y < PI/2 -> tan x < tan y.

Lemma tan_is_inj : forall x y, -PI/2 < x < PI/2 -> -PI/2 < y < PI/2 ->
   tan x = tan y -> x = y.

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}.

Lemma tan_1_gt_1 : tan 1 > 1.

Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}.
Qed.

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}.
Qed.

Definition atan x := let (v, _) := pre_atan x in v.

Lemma atan_bound : forall x, -PI/2 < atan x < PI/2.

Lemma atan_right_inv : forall x, tan (atan x) = x.

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_1 : atan 1 = PI/4.

Lemma derive_pt_atan : forall x,
      derive_pt atan x (derivable_pt_atan x) =
         1 / (1 + x²).

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}.
Defined.

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}.
Qed.

Definition in_int (x : R) : {-1 <= x <= 1}+{~ -1 <= x <= 1}.
Qed.

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.

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.

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 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) (mkposreal (/2) pos_half_prf).

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).