# Library Coqtail.Reals.Ranalysis.Ranalysis_def

Require Import Rbase Rpower Fourier.
Require Import Ranalysis1 Ranalysis2.
Require Import Rfunctions.
Require Import MyRIneq.
Require Import Rtopology.
Require Import Rinterval Rfunction_facts.

Require Import Ass_handling.

Local Open Scope R_scope.

Definition dense (D : RProp) x := eps, 0 < eps
y, D_x D x y R_dist y x < eps.

Definition continuity_pt_in (D : RProp) f x := D xlimit1_in f D (f x) x.
Definition continuity_in (D : RProp) f := x, continuity_pt_in D f x.
Definition continuity_open_interval (lb ub : R) (f : RR) :=
continuity_in (open_interval lb ub) f.
Definition continuity_interval (lb ub : R) (f : RR) :=
continuity_in (interval lb ub) f.
Definition continuity_Rball (c r : R) (f : RR) :=
continuity_in (Rball c r) f.

# (Re)defining the derivability predicate.

The usual definition of the derivability predicate is, contrary to the one of the continuity not modular at all. Here we define a derivability predicate based on the ideas used in the continuity definition. We can then now use this new definitions in specific cases (intervals, balls).

Definition growth_rate f x := (fun y(f y - f x) / (y - x)).

Definition derivable_pt_lim_in D f x l := limit1_in (growth_rate f x) (D_x D x) l x.

Definition derivable_pt_in D f x := { l | derivable_pt_lim_in D f x l }.

Definition derivable_in (D : RProp) f :=
x, D xderivable_pt_in D f x.

Definition derivable_open_interval (lb ub : R) (f : RR) :=
derivable_in (open_interval lb ub) f.

Definition derivable_interval (lb ub : R) (f : RR) :=
derivable_in (interval lb ub) f.

Definition derivable_Rball (c r : R) (f : RR) :=
derivable_in (Rball c r) f.

We can now define the appropriate projection (aka. derive functions).

Definition derive_pt_in D f x (pr : derivable_pt_in D f x) :=
match pr with | exist l _l end.

Definition derive_in D f (pr : derivable_in D f) x (Dx: D x) :=
derive_pt_in D f x (pr x Dx).

Definition derive_open_interval lb ub f (pr : derivable_open_interval lb ub f) x :=
match in_open_interval_dec lb ub x with
| left Pderive_pt_in (open_interval lb ub) f x (pr x P)
| right P ⇒ 0
end.

Definition derive_Rball c r f (pr : derivable_Rball c r f) x :=
match in_Rball_dec c r x with
| left Pderive_pt_in (Rball c r) f x (pr x P)
| right P ⇒ 0
end.

# Generic notions (injective, surjective, increasing, reciprocal, etc.)

Definition injective_in D (f : RR) :=
(x y : R), D xD yf x = f yx = y.
Definition surjective_in D (f : RR) := y, D y x, y = f x.

Definition increasing_in D f := x y, D xD yx yf x f y.
Definition decreasing_in D f := x y, D xD yx yf y f x.
Definition monotonous_in D f := { decreasing_in D f } + { increasing_in D f }.
Definition strictly_increasing_in D f := x y, D xD yx < yf x < f y.
Definition strictly_decreasing_in D f := x y, D xD yx < yf y < f x.
Definition strictly_monotonous_in D f :=
{ strictly_decreasing_in D f } + { strictly_increasing_in D f }.

Definition reciprocal_in D (f g : RR) := x, D xf (g x) = x.

The interval case

Definition injective_interval (lb ub : R) (f : RR) := injective_in (interval lb ub) f.
Definition surjective_interval (lb ub : R) (f : RR) := surjective_in (interval lb ub) f.

Definition increasing_interval (lb ub : R) (f : RR) := increasing_in (interval lb ub) f.
Definition decreasing_interval (lb ub : R) (f : RR) := decreasing_in (interval lb ub) f.
Definition monotonous_interval (lb ub : R) (f : RR) := monotonous_in (interval lb ub) f.

Definition strictly_increasing_interval (lb ub : R) (f : RR) :=
strictly_increasing_in (interval lb ub) f.
Definition strictly_decreasing_interval (lb ub : R) (f : RR) :=
strictly_decreasing_in (interval lb ub) f.
Definition strictly_monotonous_interval (lb ub : R) (f : RR) :=
strictly_monotonous_in (interval lb ub) f.

Definition reciprocal_interval (lb ub : R) f g := reciprocal_in (interval lb ub) f g.

The open interval case

Definition injective_open_interval (lb ub : R) (f : RR) :=
injective_in (open_interval lb ub) f.
Definition surjective_open_interval (lb ub : R) (f : RR) :=
surjective_in (open_interval lb ub) f.

Definition increasing_open_interval (lb ub : R) (f : RR) := increasing_in (open_interval lb ub) f.
Definition decreasing_open_interval (lb ub : R) (f : RR) := decreasing_in (open_interval lb ub) f.
Definition monotonous_open_interval (lb ub : R) (f : RR) := monotonous_in (open_interval lb ub) f.

Definition strictly_increasing_open_interval (lb ub : R) (f : RR) :=
strictly_increasing_in (open_interval lb ub) f.
Definition strictly_decreasing_open_interval (lb ub : R) (f : RR) :=
strictly_decreasing_in (open_interval lb ub) f.
Definition strictly_monotonous_open_interval (lb ub : R) (f : RR) :=
strictly_monotonous_in (open_interval lb ub) f.

Definition reciprocal_open_interval (lb ub : R) f g := reciprocal_in (open_interval lb ub) f g.

The whole real line case

Definition injective (f : RR) := injective_in whole_R f.
Definition surjective (f : RR) := surjective_in whole_R f.
Definition bijective (f : RR) := injective f surjective f.

Definition increasing (f : RR) := increasing_in whole_R f.
Definition decreasing (f : RR) := decreasing_in whole_R f.
Definition monotonous (f : RR) := monotonous_in whole_R f.

Definition strictly_increasing (f : RR) := strictly_increasing_in whole_R f.
Definition strictly_decreasing (f : RR) := strictly_decreasing_in whole_R f.
Definition strictly_monotonous (f : RR) := strictly_monotonous_in whole_R f.

Definition reciprocal f g := reciprocal_in whole_R f g.