Library Stdlib.Reals.Rtrigo_reg


From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Rtrigo1.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import PSeries_reg.
From Stdlib Require Import Lra.
From Stdlib Require Import Arith.Factorial.
Local Open Scope nat_scope.
Local Open Scope R_scope.

Lemma continuity_sin : continuity sin.

Lemma CVN_R_sin :
  forall fn:nat -> R -> R,
    fn =
    (fun (N:nat) (x:R) => (-1) ^ N / INR (fact (2 * N + 1)) * x ^ (2 * N)) ->
    CVN_R fn.

(sin h)/h -> 1 when h -> 0
Lemma derivable_pt_lim_sin_0 : derivable_pt_lim sin 0 1.

((cos h)-1)/h -> 0 when h -> 0
Lemma derivable_pt_lim_cos_0 : derivable_pt_lim cos 0 0.

Theorem derivable_pt_lim_sin : forall x:R, derivable_pt_lim sin x (cos x).

Lemma derivable_pt_lim_cos : forall x:R, derivable_pt_lim cos x (- sin x).

Lemma derivable_pt_sin : forall x:R, derivable_pt sin x.

Lemma derivable_pt_cos : forall x:R, derivable_pt cos x.

Lemma derivable_sin : derivable sin.

Lemma derivable_cos : derivable cos.

Lemma derive_pt_sin :
  forall x:R, derive_pt sin x (derivable_pt_sin _) = cos x.

Lemma derive_pt_cos :
  forall x:R, derive_pt cos x (derivable_pt_cos _) = - sin x.