# Library Coq.Reals.Rtrigo_def

Require Import Rbase Rfunctions SeqSeries Rtrigo_fun Max.
Local Open Scope R_scope.

# Definition of exponential

Definition exp_in (x l:R) : Prop :=
infinite_sum (fun i:nat => / INR (fact i) * x ^ i) l.
Lemma exp_cof_no_R0 : forall n:nat, / INR (fact n) <> 0.
Lemma exist_exp : forall x:R, { l:R | exp_in x l }.
Definition exp (x:R) : R := proj1_sig (exist_exp x).
Lemma pow_i : forall i:nat, (0 < i)%nat -> 0 ^ i = 0.
Lemma exist_exp0 : { l:R | exp_in 0 l }.
Lemma exp_0 : exp 0 = 1.

# Definition of hyperbolic functions

Definition cosh (x:R) : R := (exp x + exp (- x)) / 2.
Definition sinh (x:R) : R := (exp x - exp (- x)) / 2.
Definition tanh (x:R) : R := sinh x / cosh x.
Lemma cosh_0 : cosh 0 = 1.
Lemma sinh_0 : sinh 0 = 0.
Definition cos_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n)).
Lemma simpl_cos_n :
forall n:nat, cos_n (S n) / cos_n n = - / INR (2 * S n * (2 * n + 1)).
Lemma archimed_cor1 :
forall eps:R, 0 < eps -> exists N : nat, / INR N < eps /\ (0 < N)%nat.
Lemma Alembert_cos : Un_cv (fun n:nat => Rabs (cos_n (S n) / cos_n n)) 0.
Lemma cosn_no_R0 : forall n:nat, cos_n n <> 0.
Definition cos_in (x l:R) : Prop :=
infinite_sum (fun i:nat => cos_n i * x ^ i) l.
Lemma exist_cos : forall x:R, { l:R | cos_in x l }.
Definition of cosinus
Definition cos (x:R) : R := let (a,_) := exist_cos (Rsqr x) in a.
Definition sin_n (n:nat) : R := (-1) ^ n / INR (fact (2 * n + 1)).
Lemma simpl_sin_n :
forall n:nat, sin_n (S n) / sin_n n = - / INR ((2 * S n + 1) * (2 * S n)).
Lemma Alembert_sin : Un_cv (fun n:nat => Rabs (sin_n (S n) / sin_n n)) 0.
Lemma sin_no_R0 : forall n:nat, sin_n n <> 0.
Definition sin_in (x l:R) : Prop :=
infinite_sum (fun i:nat => sin_n i * x ^ i) l.
Lemma exist_sin : forall x:R, { l:R | sin_in x l }.
Definition sin (x:R) : R := let (a,_) := exist_sin (Rsqr x) in x * a.

# Properties

Lemma cos_sym : forall x:R, cos x = cos (- x).
Lemma sin_antisym : forall x:R, sin (- x) = - sin x.
Lemma sin_0 : sin 0 = 0.
Lemma exist_cos0 : { l:R | cos_in 0 l }.
Lemma cos_0 : cos 0 = 1.