Library Coq.Reals.Ratan
Require Import Lra.
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.
Require Import Lia.
Local Open Scope R_scope.
Tools
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.
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: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}.
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 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.
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 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.
atan's derivative value is the function 1 / (1+x²)
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 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.
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) (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).