# Library Coqtail.Reals.Ediff.Evect

Require Export Reals.

Set Implicit Arguments.

Open Scope R_scope.

Section R_normed_vector_space.

Variable V : Type.
Variable N : VR.
Variable (vO:V).
Variable smul : RVV.
Variable dim : nat.
Variable base : natV.

Variable p : natVR.
Fixpoint finite_sum (n:nat) (v:natV) {struct n} := match n with
| 0 ⇒ vO
| S ivadd (v n) (finite_sum i v)
end.

Record R_vector_space : Type := {

smul_distr_vadd : a x y, smul a (vadd x y) = vadd (smul a x) (smul a y);
smul_distr_radd : a b x, smul (a + b) x = vadd (smul a x) (smul b x);
smul_compat_rmul : a b x, smul a (smul b x) = smul (a × b) x;
smul_identity : x, smul R1 x = x;

Nzero : x, N x = 0 → x = vO;
Nmul : lambda x, N (smul lambda x) = Rabs (lambda) × N x;
Ntriang : x y, N (vadd x y) N x + N y;

basis : (v : V), v = finite_sum dim (fun nsmul (p n v) (base n))
}.

End R_normed_vector_space.

Require Import integrales.

Module integral_vector (Import I : Integrals).

Variable V : Type.
Variable N : VR.
Variable (vO:V).
Variable smul : RVV.
Variable dim : nat.
Variable base : natV.
Variable p : natVR.

Hypothesis vect_space : R_vector_space N vO vadd smul dim base p.

Definition vect_Riemann_integrable (f : RV) (a b : R) := n, Riemann_integrable (fun xp n (f x)) a b.

Definition vect_RiemannInt (f : RV) (a b : R) (pr : vect_Riemann_integrable f a b) : V :=
(fun n ⇒ (smul (RiemannInt (pr n)) (base n))).

End integral_vector.

Section Useful_definitions.

Variable V : Type.
Variable N : VR.
Variable (vO:V).
Variable smul : RVV.
Variable dim : nat.
Variable base : natV.
Variable p : natVR.

Hypothesis vect_space : R_vector_space N vO vadd smul dim base p.

Definition vsub : VVV.
Proof.
intros.
destruct vect_space.
Qed.

Definition being_in_ball (x : V) (r : R) (y : V) := N (vsub x y) < r.

Definition Open_space (I : VProp) := x, I x{r : R | r > 0 ( y, being_in_ball x r yI y)}.

Definition Vcontinuity_pt (f : RV) (I : RProp) (x : R) := I x eps : R, eps > 0 →
{alp : R | alp > 0 ( y, I y → (Rabs (x - y) alpN (vsub (f y) (f x)) eps))}.

Definition Vcontinuity (f : RV) (I : RProp) := x : R, Vcontinuity_pt f I x.

Definition Vderivable_pt_lim (f : RV) (I : RProp) (x : R) (l : V) := I x eps : R,
0 < eps
{delta : R | delta > 0 ( h : R,
h 0 → Rabs h < deltaI (x + h) → (N (vsub (smul (/h) (vsub (f (x + h)) (f x) )) l )) < eps)}.

Definition Vderivable_pt_abs (f : RV) (I : RProp) (x : R) (l : V) := Vderivable_pt_lim f I x l.

Definition Vderivable_pt (f : RV) (I : RProp) (x : R) := {l : V & (Vderivable_pt_abs f I x l)}.

Definition Vderivable (f : RV) (I : RProp) := x : R, Vderivable_pt f I x.

Definition Vderive_pt (f : RV) (I : RProp) (x : R) (pr : Vderivable_pt f I x) :=
projT1 pr.

Definition Vderive (f : RV) (I : RProp) (pr : Vderivable f I) (x : R) := Vderive_pt (pr x).

Inductive VClass (f : RV) (I : RProp) : natType :=
| C_0 : Vcontinuity f IVClass f I 0
| C_Sn : n (pr : Vderivable f I), VClass (Vderive pr) I nVClass f I (S n).

Definition VC n (I : RProp) (f : RV) := (VClass f I n).

Being C_infty

Definition VC_infty (I : RProp) (f : RV) := n, VC n I f.

Definition VCn (n : nat) (I : RProp) := sigT (VC n I).
Definition VCinfty (I : RProp) := sigT (VC_infty I).

Lemma VC_derivable : (f : RV) (I : RProp), VC 1 I fVderivable f I.
Proof.
intros.
inversion X.
apply pr.
Qed.

Definition VVcontinuity_pt (f : VV) (K : VProp) (open : Open_space K) (x : V) := K x eps : R, eps > 0 →
{alp : R | alp > 0 ( y, K yN (vsub x y) alpN (vsub (f y) (f x)) eps)}.

Definition VVcontinuity (f : VV) (K : VProp) (open : Open_space K) := (x : V), VVcontinuity_pt f open x.

Definition lipschitz (f : VV) (K : VProp) (open : Open_space K) := {k | k > 0 (x x' : V), K xK x'N (vsub x x') < k × N (vsub (f x) (f x'))}.

End Useful_definitions.