Library Coqtail.Reals.Ranalysis.Ranalysis_usual

Require Import Rbase Ranalysis Rfunctions Rfunction_def.
Require Import MyRIneq.
Require Import Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_facts.

Local Open Scope R_scope.

Derivability (thus continuity) of usual functions.

Identity


Lemma derivable_pt_lim_in_id: D x,
  derivable_pt_lim_in D id x 1.
Proof.
intros D x eps eps_pos ; eps ; intros ; split.
 assumption.
 intros y [[_ Hneq] _] ; unfold growth_rate, id ; simpl.
  apply Rle_lt_trans with (Rabs 0) ; [| rewrite Rabs_R0 ; assumption].
  right ; apply Rabs_eq_compat ; field ; apply Rminus_eq_contra ;
  symmetry ; assumption.
Qed.

Lemma derivable_pt_in_id: (D : RProp) (x : R),
  derivable_pt_in D id x.
Proof.
intros ; eexists ; eapply derivable_pt_lim_in_id.
Qed.

Lemma derivable_in_id: (D : RProp),
  derivable_in D id.
Proof.
intros D x x_in ; eapply derivable_pt_in_id.
Qed.

Lemma derive_pt_open_interval_id : a b x pr,
  open_interval a b x
 (derive_pt_in (open_interval a b) id x pr = 1)%R.
intros a b x pr x_in ; rewrite derive_open_interval_pt with (pr' := derivable_pt_id x).
 apply derive_pt_id.
 assumption.
Qed.

Powers

Definition Dpow (n : nat) := match n with
  | Ofun _ ⇒ 0
  | S mfun x(INR (S m)) × pow x m
end.


Monomials
Inverse
Negative powers