Library Coq.Reals.Machin

Require Import Lra.
Require Import Rbase.
Require Import Rtrigo1.
Require Import Ranalysis_reg.
Require Import Rfunctions.
Require Import AltSeries.
Require Import Rseries.
Require Import SeqProp.
Require Import PartSum.
Require Import Ratan.
Require Import Omega.

Local Open Scope R_scope.

Definition atan_sub u v := (u - v )/(1 + u * v ).

Lemma atan_sub_correct :
forall u v, 1 + u * v <> 0 -> -PI /2 < atan u - atan v < PI /2 ->
   -PI /2 < atan (atan_sub u v) < PI /2 ->
   atan u = atan v + atan (atan_sub u v).

Lemma tech : forall x y , -1 <= x <= 1 -> -1 < y < 1 ->
  -PI /2 < atan x - atan y < PI /2.

Lemma Machin_2_3 : PI /4 = atan(/2) + atan(/3).

Lemma Machin_4_5_239 : PI /4 = 4 * atan (/5) - atan(/239).

Lemma Machin_2_3_7 : PI /4 = 2 * atan(/3) + (atan (/7)).

Definition PI_2_3_7_tg n :=
  2 * Ratan_seq (/3) n + Ratan_seq (/7) n.

Lemma PI_2_3_7_ineq :
  forall N : nat,
    sum_f_R0 (tg_alt PI_2_3_7_tg) (S (2 * N)) <= PI / 4 <=
    sum_f_R0 (tg_alt PI_2_3_7_tg) (2 * N).

Navigation