# Library Coqtail.Reals.Cauchy_lipschitz

Require Import Reals.
Require Import Rintegral Riemann_integrable.
Require Import Rfunction_classes Nth_derivative_def.
Require Import Fourier Ring.
Require Import Ranalysis.
Require Import Rextensionality.

Section Trivial.

Lemma C_Sn_derivable : f n, C (S n) fderivable f.
Proof.
intros.
inversion H. subst. apply pr.
Qed.

Lemma C_Sm_derive_C_m : f n pr, C (S n) fC n (derive f pr).
Proof.
intros.
inversion H.
eapply C_ext. 2: apply H1. intro. apply pr_nu.
Qed.

Lemma C_continuity : f n, C n fcontinuity f.
Proof.
intros.
inversion H. apply H0.
apply derivable_continuous. assumption.
Qed.

Lemma CL_tr : a t0 V0, C 0 a
{y : RR & {pr : (D 1 y) | (t : R), (nth_derive y pr) t = (a t) × (y t) y t0 = V0}}.
Proof.
intros a t0 V0 H ; assert (Hcont : continuity a) by (inversion H ; assumption).
assert ( t0 t, Riemann_integrable a t0 t).
intros ; apply continuity_RiemannInt_1.
intros ; inversion H ; auto.
assert (pr : C 1 (fun tV0 × exp (@RiemannInt a t0 t (X t0 t)))).
apply C_scal; apply (C_comp 1 exp); [apply C_infty_exp |
apply derivable_pt_continuity_Riemann_implies_C1] ; reg.

(fun tV0 × exp (@RiemannInt a t0 t (X t0 t))) ; (C_implies_D _ _ pr).

intro t ; split.
rewrite <- (derive_pt_RiemannInt a t0 t X (Hcont t)), <-(derive_pt_exp ),
<- derive_pt_scal, Rmult_comm, <- (derive_pt_comp (fun t1RiemannInt (X t0 t1))
(mult_real_fct V0 exp)) ; apply pr_nu_var ; reflexivity.
rewrite RiemannInt_singleton, exp_0 ; apply Rmult_1_r.
Qed.

Lemma RiemannInt_continuity : a t0 (Hconta : continuity a) (Ha : t0 t,
Riemann_integrable a t0 t), continuity (fun tRiemannInt (Ha t0 t)).
Proof.
intros ; apply derivable_continuous ; intro ; apply RiemannInt_derivable_pt ; apply Hconta.
Qed.

Lemma CL_tr_second_member : a b t0 V0, C 0 aC 0 b
{y : RR & { pr : (D 1 y) |
(t : R), (nth_derive y pr) t - (a t) × (y t) = b t y t0 = V0}}.
Proof.
intros a b t0 V0 Ha0 Hb0 ;
assert (Ha: t0 t, Riemann_integrable a t0 t)
by (intros ; apply continuity_RiemannInt_1 ; inversion Ha0 ; intuition) ;
assert (Hconta : continuity a)
by (inversion Ha0 ; assumption) ;
assert (Hcontb : continuity b)
by (inversion Hb0 ; assumption).

assert (Hcontsol : t1 t, continuity_pt
(b × (comp exp (- (fun tRiemannInt (Ha t1 t)))))%F t).
intros ; reg ; apply (C_continuity _ 1) ;
apply derivable_pt_continuity_Riemann_implies_C1 ; assumption.

assert (Hsol : t1 t0 t, Riemann_integrable
(b × (comp exp (- (fun tRiemannInt (Ha t1 t)))))%F t0 t)
by (intros ; apply continuity_RiemannInt_1 ; intuition).

assert (pr : C 1 (((fct_cte V0) + (fun tRiemannInt (Hsol t0 t0 t))) ×
(comp exp (fun tRiemannInt (Ha t0 t))))%F).
apply C_mult ; [apply C_plus ; [apply C_infty_const |] | apply C_comp ;
[apply C_infty_exp |]] ; apply derivable_pt_continuity_Riemann_implies_C1 ; reg ;
apply RiemannInt_continuity ; assumption.

(((fct_cte V0) + (fun tRiemannInt (Hsol t0 t0 t))) ×
(comp exp (fun tRiemannInt (Ha t0 t))))%F ; (C_implies_D _ _ pr).

intros t ; simpl ; split.
assert (Hpr1 : derivable_pt (fun tRiemannInt (Hsol t0 t0 t)) t)
by (apply RiemannInt_derivable_pt ; reg ; apply RiemannInt_continuity ;
assumption).
assert (Hpr2 : derivable_pt (fun tRiemannInt (Ha t0 t)) t)
by (apply RiemannInt_derivable_pt ; auto).

unfold derive ; rewrite (pr_nu_var _ (((fct_cte V0) +
(fun tRiemannInt (Hsol t0 t0 t))) × (comp exp (fun tRiemannInt (Ha t0 t))))%F _ _
(derivable_pt_mult _ _ _ (derivable_pt_plus _ _ _ (derivable_pt_const V0 t) Hpr1)
(derivable_pt_comp _ _ _ Hpr2 (derivable_pt_exp _)))).

rewrite derive_pt_mult, derive_pt_comp, derive_pt_exp, derive_pt_RiemannInt_1,
derive_pt_plus, derive_pt_const ; unfold plus_fct, comp, fct_cte, mult_fct ; simpl.
rewrite derive_pt_RiemannInt_1.
ring_simplify ; unfold opp_fct ; rewrite exp_Ropp ; field.
apply Rgt_not_eq ; apply exp_pos.
apply Hcontsol.
apply Hconta.
reflexivity.
unfold comp, plus_fct, mult_fct, fct_cte ; do 2 rewrite RiemannInt_singleton ;
rewrite exp_0 ; ring.
Qed.

End Trivial.