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 : R → Prop) x := ∀ eps, 0 < eps →
  ∃ y, D_x D x y ∧ R_dist y x < eps.

Definition continuity_pt_in (D : R → Prop) f x := D x → limit1_in f D (f x) x.
Definition continuity_in (D : R → Prop) f := ∀ x, continuity_pt_in D f x.
Definition continuity_open_interval (lb ub : R) (f : R → R) :=
  continuity_in (open_interval lb ub) f.
Definition continuity_interval (lb ub : R) (f : R → R) :=
  continuity_in (interval lb ub) f.
Definition continuity_Rball (c r : R) (f : R → R) :=
  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 : R → Prop) f :=
  ∀ x, D x → derivable_pt_in D f x.

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

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

Definition derivable_Rball (c r : R) (f : R → R) :=
  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 P ⇒ derive_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 P ⇒ derive_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 : R → R) :=
∀ (x y : R), D x → D y → f x = f y → x = y.
Definition surjective_in D (f : R → R) := ∀ y, D y → ∃ x, y = f x.

Definition increasing_in D f := ∀ x y, D x → D y → x ≤ y → f x ≤ f y.
Definition decreasing_in D f := ∀ x y, D x → D y → x ≤ y → f 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 x → D y → x < y → f x < f y.
Definition strictly_decreasing_in D f := ∀ x y, D x → D y → x < y → f 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 : R → R) := ∀ x, D x → f (g x) = x.

The interval case

The open interval case

The whole real line case

Definition injective (f : R → R) := injective_in whole_R f.
Definition surjective (f : R → R) := surjective_in whole_R f.
Definition bijective (f : R → R) := injective f ∧ surjective f.

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

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

Definition reciprocal f g := reciprocal_in whole_R f g.