Library LM.hierarchyD

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

From Coq Require Import Reals ssreflect.

From Coquelicot Require Import Coquelicot.
Close Scope R_scope.

From Numbers Require Import R_compl.
From Algebra Require Import Algebra.

From LM Require Import continuous_linear_map.

Local Open Scope R_scope.

Complete Dependant uniform spaces

Module CompleteSpaceD.

Record mixin_of (T : UniformSpace) := Mixin {
  lim : (F:(TProp)->Prop) (H1:ProperFilter F) (H2:cauchy F), T ;
  ax1 : F (H1:ProperFilter F) (H2:cauchy F), eps : posreal,
        F (ball (lim F H1 H2) eps)
}.

Section ClassDef.

Record class_of (T : Type) := Class {
  base : UniformSpace.class_of T ;
  mixin : mixin_of (UniformSpace.Pack _ base T)
}.
Local Coercion base : class_of >-> UniformSpace.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition UniformSpace := UniformSpace.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> UniformSpace.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Notation CompleteSpaceD := type.

End Exports.

End CompleteSpaceD.

Export CompleteSpaceD.Exports.

Section CompleteSpace1.

Context {T : CompleteSpaceD}.

Definition lim (F:(TProp)->Prop) (H1:ProperFilter F) (H2:cauchy F): T
  := CompleteSpaceD.lim _ (CompleteSpaceD.class T) F H1 H2.

Lemma complete_cauchyD :
   (F : (T Prop) Prop)
  (H1:ProperFilter F) (H2:cauchy F),
   eps : posreal,
  F (ball (lim F H1 H2) eps).
Proof.
apply CompleteSpaceD.ax1.
Qed.

Dependant iota

Lemma iotaD'_correct_weak_aux1: (P : T Prop) (H: x:T, P x),
  ProperFilter (fun A : T Prop t : T, P t A t).
Proof.
intros P (x,Hx).
constructor.
intros Q FQ.
x.
now apply FQ.
constructor.
now intro x0.
intros A B HA HB x0 Hx0.
split.
now apply HA.
now apply HB.
intros A B HAB HA x0 Hx0.
apply HAB ; now apply HA.
Qed.

Lemma iotaD'_correct_weak_aux2: (P : T Prop) (H: x:T, P x),
  ( x y, P x P y eps : posreal, ball x eps y)
    cauchy (fun A : T Prop t : T, P t A t).
Proof.
intros P (x,Hx) H e.
x.
intros y Hy.
now apply H.
Qed.

Definition iotaD' (P : T Prop) (H: x:T, P x)
     (HP: x y, P x P y eps : posreal, ball x eps y)
   := lim (fun A ⇒ ( x, P x A x)) (iotaD'_correct_weak_aux1 P H)
            (iotaD'_correct_weak_aux2 P H HP).

Lemma iotaD'_correct_weak :
   (P : T Prop)
  (HP: x y, P x P y eps : posreal, ball x eps y)
   (H:( x:T, P x)) (eps : posreal),
      y, P y ball (iotaD' P H HP) eps y.
Proof.
intros P HP H eps.
set (F := fun A : T Prop t : T, P t A t).
assert ( eps : posreal, F (ball (iotaD' P H HP) eps)) as HF.
apply complete_cauchyD.
assert (F (ball (iotaD' P H HP) eps)) as Heps.
apply HF.
now apply Heps.
Qed.

End CompleteSpace1.

Dependant functional CompleteSpace

Section fct_CompleteSpaceD.

Context {T : Type} {U : CompleteSpaceD}.

Let Fr := fun (F : ((T U) Prop) Prop)
   (t : T) (P : U Prop) ⇒ F (fun gP (g t)).

Lemma lim_fct_aux1: (F : ((T U) Prop) Prop),
    (ProperFilter F) t, ProperFilter (Fr F t).
Proof.
  intros F FF.
   case: FFHF FF t.
    split.
    - moveP Hp.
      case: (HF _ Hp) ⇒ f Hf.
      by (f t).
    - split.
      + by apply FF.
      + moveP P' Hp Hp'.
      by apply FF.
      + moveP P' Hpp'.
      apply FF.
      movef ; by apply Hpp'.
Qed.

Lemma lim_fct_aux2: (F : ((T U) Prop) Prop),
    (ProperFilter F) (cauchy F) t, cauchy (Fr F t).
Proof.
intros F FF HFc t.
   moveeps.
    case: (HFc eps) ⇒ f Hf.
     (f t).
    move: Hf ; apply FFg.
    by [].
Qed.

Definition lim_fct (F : ((T U) Prop) Prop) (H1: ProperFilter F)
  (H2: cauchy F) (t : T) :=
  lim (Fr F t) (lim_fct_aux1 F H1 t) (lim_fct_aux2 F H1 H2 t).

Lemma complete_cauchy_fct :
   (F : ((T U) Prop) Prop)
  (H1: ProperFilter F) (H2: cauchy F)
   (eps : posreal), F (ball (lim_fct F H1 H2) eps).
Proof.
  moveF FF HFc.
  assert ( t (eps : posreal), (Fr F t) (fun xball (lim_fct F FF HFc t) eps x)).
  movet.
  apply complete_cauchyD.
  moveeps.
  generalize (proj1 cauchy_distance HFc) ⇒ HFc1.
  case: (HFc1 (pos_div_2 eps)) ⇒ {HFc1} P ; simpl ; caseHP H0.
  apply filter_imp with (2 := HP).
  moveg Hg t.
  move: (fun hH0 g h Hg) ⇒ {H0} ⇒ H0.
  move: (H t (pos_div_2 eps)) ; simpl ⇒ {H} ⇒ H.
  unfold Fr in H ; generalize (filter_and _ _ H HP) ⇒ {H} ⇒ H.
  apply filter_ex in H ; case: Hh H.
  rewrite <- (Rplus_half_diag eps).
  apply ball_triangle with (h t).
  by apply H.
  apply ball_sym, H0.
  by apply H.
Qed.

Definition fct_CompleteSpaceD_mixin :=
  CompleteSpaceD.Mixin _ lim_fct complete_cauchy_fct.

Canonical fct_CompleteSpaceD :=
  CompleteSpaceD.Pack (T U) (CompleteSpaceD.Class _ _ fct_CompleteSpaceD_mixin) (T U).

End fct_CompleteSpaceD.

Dependant Complete Normed Modules

Module CompleteNormedModuleD.

Section ClassDef.

Variable K : AbsRing.

Record class_of (T : Type) := Class {
  base : NormedModule.class_of K T ;
  mixin : CompleteSpaceD.mixin_of (UniformSpace.Pack T base T)
}.
Local Coercion base : class_of >-> NormedModule.class_of.
Definition base2 T (cT : class_of T) : CompleteSpaceD.class_of T :=
  CompleteSpaceD.Class _ (base T cT) (mixin T cT).
Local Coercion base2 : class_of >-> CompleteSpaceD.class_of.

Structure type := Pack { sort; _ : class_of sort ; _ : Type }.
Local Coercion sort : type >-> Sortclass.

Variable cT : type.

Definition class := let: Pack _ c _ := cT return class_of cT in c.

Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition AbelianMonoid := AbelianMonoid.Pack cT xclass xT.
Definition AbelianGroup := AbelianGroup.Pack cT xclass xT.
Definition ModuleSpace := ModuleSpace.Pack _ cT xclass xT.
Definition NormedModuleAux := NormedModuleAux.Pack _ cT xclass xT.
Definition NormedModule := NormedModule.Pack _ cT xclass xT.
Definition UniformSpace := UniformSpace.Pack cT xclass xT.
Definition CompleteSpaceD := CompleteSpaceD.Pack cT xclass xT.

End ClassDef.

Module Exports.

Coercion base : class_of >-> NormedModule.class_of.
Coercion mixin : class_of >-> CompleteSpaceD.mixin_of.
Coercion base2 : class_of >-> CompleteSpaceD.class_of.
Coercion sort : type >-> Sortclass.
Coercion AbelianMonoid : type >-> AbelianMonoid.type.
Canonical AbelianMonoid.
Coercion AbelianGroup : type >-> AbelianGroup.type.
Canonical AbelianGroup.
Coercion ModuleSpace : type >-> ModuleSpace.type.
Canonical ModuleSpace.
Coercion NormedModuleAux : type >-> NormedModuleAux.type.
Canonical NormedModuleAux.
Coercion NormedModule : type >-> NormedModule.type.
Canonical NormedModule.
Coercion UniformSpace : type >-> UniformSpace.type.
Canonical UniformSpace.
Coercion CompleteSpaceD : type >-> CompleteSpaceD.type.
Canonical CompleteSpaceD.
Notation CompleteNormedModuleD := type.

End Exports.

End CompleteNormedModuleD.

Export CompleteNormedModuleD.Exports.

Section CompleteNormedModuleD1.

Context {T : Type} {K : AbsRing} {V : CompleteNormedModuleD K}.

Lemma iotaD_aux1: P : V Prop,
  (! x : V, P x)
   ( x y, P x P y eps : posreal, ball x eps y).
Proof.
intros P [x [Px HP]].
intros u v Pu Pv eps.
replace v with u.
apply ball_center.
apply eq_trans with x.
now apply eq_sym, HP.
now apply HP.
Qed.

Lemma iotaD_aux2: (P : V Prop),
  (! x : V, P x) ( x : V, P x).
Proof.
intros P [x [Px HP]].
now x.
Qed.

Definition iotaD (P : V Prop) (HP: (! x : V, P x))
   := iotaD' P (iotaD_aux2 P HP) (iotaD_aux1 P HP).

Lemma iota_correct :
   (P : V Prop) (HP: ! x : V, P x),
  P (iotaD P HP).
Proof.
intros P HP.
elim HP; intros x [Px H].
replace (iotaD P HP) with x.
exact Px.
apply eq_sym, eq_close.
intros eps.
unfold iotaD.
now apply: iotaD'_correct_weak.
Qed.

End CompleteNormedModuleD1.

CompleteSpace CompleteSpaceD

Section CS_is_CSD.

Context {E: CompleteSpace}.

Definition lime : ((E Prop)-> Prop) E
    := CompleteSpace.lim _ (CompleteSpace.class E).

Lemma CS_is_CSD_aux: F (H1:ProperFilter F) (H2:cauchy F),
   eps : posreal, F (ball (lime F) eps).
Proof.
intros.
now apply: complete_cauchy.
Qed.

Definition CompleteSpace_CompleteSpaceD_mixin :=
  CompleteSpaceD.Mixin _ (fun F _ _ ⇒ (lime F))
     (CS_is_CSD_aux).

Canonical CompleteSpace_CompleteSpaceD :=
  CompleteSpaceD.Pack _ (CompleteSpaceD.Class _ _ CompleteSpace_CompleteSpaceD_mixin) E.

End CS_is_CSD.

CompleteNormedModule CompleteNormedModuleD

Section CNM_is_CNMD.

Context {E: CompleteNormedModule R_AbsRing}.

Canonical CompleteNormedModule_CompleteNormedModuleD :=
  CompleteNormedModuleD.Pack R_AbsRing E
     (CompleteNormedModuleD.Class R_AbsRing E
            (NormedModule.class R_AbsRing E)
            (@CompleteSpace_CompleteSpaceD_mixin
               (CompleteSpace.Pack E (CompleteSpace.class E) E))) E.

End CNM_is_CNMD.

Clm is CompleteNormedModuleD

Section clm_complete.

Variable E : NormedModule R_AbsRing.
Variable F : CompleteNormedModuleD R_AbsRing.

Definition cleanFilter (Fi: ((clm E F) Prop) Prop):
  (((E F) Prop) Prop)
    := fun A : (EF) Prop V : clm E F Prop,
           Fi V ( f, V f A (m f)).

Let Fr := fun (FF : ((E F) Prop) Prop)
   (t : E) (P : F Prop) ⇒ FF (fun gP (g t)).

Let Fri := fun (Fi: ((clm E F) Prop) Prop)
    (t : E) (P : F Prop) ⇒ Fr (cleanFilter Fi) t P.

Lemma cleanFilterProper: (Fi: ((clm E F) Prop) Prop),
  ProperFilter Fi ProperFilter (cleanFilter Fi).
Proof.
intros Fi (FF1,FF2).
constructor.
unfold cleanFilter.
intros P (V,(HV1,HV2)).
destruct (FF1 V HV1) as (f,Hf).
f; now apply HV2.
constructor; unfold cleanFilter.
(fun _True); split.
apply FF2.
easy.
intros P Q (Vp,(HP1,HP2)) (Vq,(HQ1,HQ2)).
(fun xVp x Vq x); split.
now apply FF2.
intros f (Hf1,Hf2); split.
now apply HP2.
now apply HQ2.
intros P Q H (Vp,(HP1,HP2)).
Vp; split.
easy.
intros f Hf.
apply H; now apply HP2.
Qed.

Lemma clm_lim_aux1: (Fi : ((clm E F) Prop) Prop),
    (ProperFilter Fi) t, ProperFilter (Fri Fi t).
Proof.
intros Fi FFi t.
apply lim_fct_aux1.
now apply cleanFilterProper.
Qed.

Lemma clm_lim_aux2: (Fi : ((clm E F) Prop) Prop),
    (ProperFilter Fi) (cauchy Fi) t, cauchy (Fri Fi t).
Proof.
intros Fi FFi HFc t eps.
case (is_zero_dec t); intros Ht.
zero.
unfold Fri, Fr, cleanFilter.
(fun _True).
split.
apply FFi.
intros f _.
replace (f t) with (@zero F).
apply ball_center.
rewrite Ht.
apply sym_eq.
apply: lm_zero.
apply f.
assert (K1: 0 < norm t) by now apply norm_gt_0.
assert (K2: 0 < / norm t) by now apply Rinv_0_lt_compat.
assert (K:0 < eps/norm t).
apply Rmult_lt_0_compat.
apply eps.
exact K2.
destruct (HFc (mkposreal _ K)) as (f,Hf).
(f t).
unfold Fri, Fr, cleanFilter.
(ball f (eps/norm t)).
split.
exact Hf.
intros g Hg.
unfold ball in Hg; simpl in Hg; unfold clm_ball in Hg.
apply: norm_compat1.
replace (minus (g t) (f t)) with ((minus g f) t) by reflexivity.
apply Rle_lt_trans with (operator_norm (minus g f)×norm t).
apply operator_norm_helper'; try assumption.
apply is_finite_operator_norm_plus.
apply (Cf _ _ g).
apply is_finite_operator_norm_opp.
apply (Cf _ _ f).
apply Rmult_lt_reg_r with (/ norm t); try assumption.
apply Rle_lt_trans with (2:=Hg).
right; field.
now apply Rgt_not_eq.
Qed.

Definition clm_lim (Fi : ((clm E F) Prop) Prop)
   (H1: ProperFilter Fi) (H2: cauchy Fi) (t:E) :=
      lim (Fri Fi t) (clm_lim_aux1 Fi H1 t) (clm_lim_aux2 Fi H1 H2 t).

Lemma ball_plus_plus: (x a y b:F) (eps:posreal), ball x eps a ball y eps b
      ball (plus x y) (2*(@norm_factor R_AbsRing F)*eps) (plus a b).
Proof.
intros x a y b eps Hx Hy.
pose (v:=@norm_factor R_AbsRing F); fold v.
apply: norm_compat1.
apply Rle_lt_trans with (norm (plus (minus a x) (minus b y))).
right; f_equal.
unfold minus.
rewrite <- 2!plus_assoc; f_equal.
rewrite opp_plus plus_comm; rewrite <- plus_assoc; f_equal.
apply plus_comm.
apply: (Rle_lt_trans _ _ _ (norm_triangle _ _)).
replace (2×v×eps) with (v×eps+v×eps) by ring.
apply Rplus_lt_compat; unfold v.
now apply: norm_compat2.
now apply: norm_compat2.
Qed.

Lemma ball_scal_scal: (x a:F) l (eps:posreal),
      l 0 ball x eps a
      ball (scal l x) (Rabs l×@norm_factor R_AbsRing F × eps) (scal l a).
Proof.
intros x a l eps Hl Hx.
pose (v:=@norm_factor R_AbsRing F); fold v.
apply: norm_compat1.
apply Rle_lt_trans with (norm (scal l (minus a x))).
right; f_equal.
unfold minus.
rewrite scal_distr_l; f_equal.
apply sym_eq; apply: scal_opp_r.
rewrite norm_scal_R.
unfold abs; simpl; rewrite Rmult_assoc.
apply Rmult_lt_compat_l.
now apply Rabs_pos_lt.
now apply: norm_compat2.
Qed.

Lemma clm_lim_lm: (Fi : ((clm E F) Prop) Prop)
   (H1: ProperFilter Fi) (H2: cauchy Fi),
     lin_map (clm_lim Fi H1 H2).
Proof.
intros Fi H1 H2; split.
intros x y.
apply eq_close; intros eps.
pose (v:=@norm_factor R_AbsRing F).
assert (K:0 < eps /4 / v).
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply eps.
apply Rinv_0_lt_compat.
apply Rmult_lt_0_compat; apply Rlt_0_2.
apply Rinv_0_lt_compat.
apply norm_factor_gt_0.
assert (HX:((fun P : F PropcleanFilter Fi (fun g : E FP (g x)))
        (ball (clm_lim Fi H1 H2 x) (mkposreal _ K)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HX as (Vx, (Hx1,Hx2)).
assert (HY:((fun P : F PropcleanFilter Fi (fun g : E FP (g y)))
        (ball (clm_lim Fi H1 H2 y) (mkposreal _ K)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HY as (Vy, (Hy1,Hy2)).
assert (HXY:((fun P : F PropcleanFilter Fi (fun g : E FP (g (plus x y))))
        (ball (clm_lim Fi H1 H2 (plus x y)) (pos_div_2 eps)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HXY as (Vxy, (Hxy1,Hxy2)).
assert (H:(Fi (fun fVx f Vy f Vxy f))).
apply H1; try assumption.
apply H1; assumption.
apply H1 in H.
destruct H as (l,Hl).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps).
2: simpl; field.
apply ball_triangle with (l (plus x y)).
apply (Hxy2 l), Hl.
replace (l (plus x y)) with (plus (l x) (l y)).
2: apply sym_eq, (Lf _ _ l).
replace (pos (pos_div_2 eps)) with (2×v*(mkposreal _ K)).
apply ball_plus_plus.
apply ball_sym, (Hx2 l), Hl.
apply ball_sym, (Hy2 l), Hl.
simpl; field.
apply Rgt_not_eq, norm_factor_gt_0.
intros l x.
case (Req_dec l 0); intros Hl.
rewrite Hl 2!scal_zero_l.
apply eq_close; intros eps.
assert (H:((fun P : F PropcleanFilter Fi (fun g : E FP (g zero)))
        (ball (clm_lim Fi H1 H2 zero) (eps)))).
unfold clm_lim.
apply complete_cauchyD.
destruct H as (V,(HV1,HV2)).
apply H1 in HV1; destruct HV1 as (f,Hf).
specialize (HV2 f Hf).
replace (f zero) with (@zero F) in HV2.
exact HV2.
apply sym_eq; apply: lm_zero.
apply (Lf _ _ f).
apply eq_close; intros eps.
pose (v:=@norm_factor R_AbsRing F).
assert (K:0 < pos_div_2 eps /Rabs l / v).
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply (pos_div_2 eps).
apply Rinv_0_lt_compat.
now apply Rabs_pos_lt.
apply Rinv_0_lt_compat.
apply norm_factor_gt_0.
assert (HX:((fun P : F PropcleanFilter Fi (fun g : E FP (g x)))
        (ball (clm_lim Fi H1 H2 x) (mkposreal _ K)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HX as (Vx, (Hx1,Hx2)).
assert (HLX:((fun P : F PropcleanFilter Fi (fun g : E FP (g (scal l x))))
        (ball (clm_lim Fi H1 H2 (scal l x)) (pos_div_2 eps)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HLX as (Vlx, (Hlx1,Hlx2)).
assert (H:(Fi (fun fVx f Vlx f))).
apply H1; assumption.
apply H1 in H.
destruct H as (f,Hf).
replace (pos eps) with (pos_div_2 eps + pos_div_2 eps).
2: simpl; field.
apply ball_triangle with (f (scal l x)).
apply (Hlx2 f), Hf.
replace (f (scal l x)) with (scal l (f x)).
2: apply sym_eq, (Lf _ _ f).
replace (pos (pos_div_2 eps)) with (Rabs l×v*(mkposreal _ K)).
apply ball_scal_scal; try assumption.
apply ball_sym, (Hx2 f), Hf.
simpl; field; split.
apply Rgt_not_eq, Rabs_pos_lt; assumption.
apply Rgt_not_eq, norm_factor_gt_0.
Qed.

Lemma clm_lim_continuous: (Fi : ((clm E F) Prop) Prop)
   (H1: ProperFilter Fi) (H2: cauchy Fi),
     is_finite (operator_norm (clm_lim Fi H1 H2)).
Proof.
intros Fi H1 H2.
pose (v:=@norm_factor R_AbsRing F).
elim (H2 (mkposreal _ Rlt_0_1)); intros f Hf; simpl in Hf.
replace (clm_lim Fi H1 H2) with
    (plus (m f) (plus (clm_lim Fi H1 H2) (opp f))).
apply is_finite_operator_norm_plus.
apply (Cf _ _ f).
apply operator_norm_helper3 with (2).
left; apply Rlt_0_2.
intros x NZx.
assert (K: 0 < norm x /v).
apply Rmult_lt_0_compat.
now apply norm_gt_0.
apply Rinv_0_lt_compat.
apply norm_factor_gt_0.
assert (HX:((fun P : F PropcleanFilter Fi (fun g : E FP (g x)))
        (ball (clm_lim Fi H1 H2 x) (mkposreal _ K)))).
unfold clm_lim.
apply complete_cauchyD.
destruct HX as (V,(HV1,HV2)); simpl in HV2.
assert (H:(Fi (fun zV z (ball f 1 z)))).
apply H1; assumption.
apply H1 in H.
destruct H as (g,(Hg1,Hg2)).
specialize (HV2 g Hg1).
unfold ball in Hg2; simpl in Hg2; unfold clm_ball in Hg2.
apply Rle_trans with
  (norm (plus (minus (clm_lim Fi H1 H2 x) (g x))
              (minus (g x) (f x)))).
right; f_equal.
unfold minus; rewrite <- plus_assoc.
apply trans_eq with (plus (clm_lim Fi H1 H2 x) (opp (f x))).
reflexivity.
f_equal.
rewrite plus_assoc.
rewrite (plus_opp_l (g x)).
apply sym_eq, plus_zero_l.
apply Rle_trans with (norm (minus (clm_lim Fi H1 H2 x) (g x))
      + norm (minus (g x) (f x))).
apply: norm_triangle.
replace (2×norm x) with (v*(mkposreal _ K)+ norm x).
apply Rplus_le_compat.
left; unfold v; apply: norm_compat2.
now simpl; apply ball_sym.
replace (minus (g x) (f x)) with ((minus g f) x) by reflexivity.
apply Rle_trans with (operator_norm (minus g f)×norm x).
apply operator_norm_helper'; try assumption.
apply is_finite_operator_norm_plus.
apply (Cf _ _ g).
apply is_finite_operator_norm_opp.
apply (Cf _ _ f).
rewrite <- (Rmult_1_l (norm x)) at 2.
apply Rmult_le_compat_r.
apply norm_ge_0.
now left.
simpl; field.
apply Rgt_not_eq, norm_factor_gt_0.
rewrite plus_comm - plus_assoc.
rewrite plus_opp_l.
apply plus_zero_r.
Qed.

Definition Clm_lim:= fun (Fi : ((clm E F) Prop) Prop)
   (H1: ProperFilter Fi) (H2: cauchy Fi) ⇒
      Clm E F (clm_lim Fi H1 H2) (clm_lim_lm Fi H1 H2)
                                 (clm_lim_continuous Fi H1 H2).

Lemma complete_cauchy_clm :
   (Fi : ((clm E F) Prop) Prop)
         (H1:ProperFilter Fi) (H2:cauchy Fi),
        eps : posreal, Fi (ball (Clm_lim Fi H1 H2) eps).
Proof.
intros Fi H1 H2 eps.
pose (v:=@norm_factor R_AbsRing F).
generalize (proj1 cauchy_distance H2) ⇒ HFc1.
destruct (HFc1 (pos_div_2 (pos_div_2 eps))) as (P, (HP1,HP2)).
apply filter_imp with (2:=HP1).
intros f Hf.
unfold ball; simpl; unfold clm_ball; simpl.
apply Rle_lt_trans with (pos_div_2 eps).
apply operator_norm_helper3'.
left; apply (pos_div_2 eps).
intros u Hu.
assert (K:0 < eps/4×norm u/v).
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply Rmult_lt_0_compat.
apply (eps).
apply Rinv_0_lt_compat.
apply Rmult_lt_0_compat; apply Rlt_0_2.
now apply norm_gt_0.
apply Rinv_0_lt_compat.
apply norm_factor_gt_0.
assert (HH:((fun P : F PropcleanFilter Fi (fun g : E FP (g u)))
        (ball (clm_lim Fi H1 H2 u) (mkposreal _ K)))).
unfold clm_lim.
apply complete_cauchyD.
simpl in HH; destruct HH as (V,(HV1,HV2)).
assert (H:(Fi (fun zV z P z))).
apply H1; assumption.
apply H1 in H.
destruct H as (g,(Hg1,Hg2)).
specialize (HV2 g Hg1).
apply Rle_trans with (norm (plus (minus (g u) (clm_lim Fi H1 H2 u)) (opp (minus (g u) (f u))))).
right; f_equal.
apply trans_eq with (plus (f u) (opp (clm_lim Fi H1 H2 u))).
reflexivity.
unfold minus; rewrite plus_comm (plus_comm (g u) _).
rewrite <- plus_assoc; f_equal.
rewrite opp_plus opp_opp.
now rewrite plus_assoc plus_opp_r plus_zero_l.
apply Rle_trans with (1:=norm_triangle _ _).
replace (pos_div_2 eps×norm u) with (v*(mkposreal _ K)+eps/2/2×norm u).
apply Rplus_le_compat.
left; unfold v; apply: norm_compat2.
exact HV2.
rewrite norm_opp.
specialize (HP2 f g Hf Hg2).
unfold ball in HP2; simpl in HP2; unfold clm_ball in HP2.
apply Rle_trans with (norm ((minus g f) u)).
right; reflexivity.
apply Rle_trans with (operator_norm (minus g f)×norm u).
apply operator_norm_helper'; try assumption.
apply is_finite_operator_norm_plus.
apply (Cf _ _ g).
apply is_finite_operator_norm_opp.
apply (Cf _ _ f).
apply Rmult_le_compat_r.
apply norm_ge_0.
now left.
simpl; field.
apply Rgt_not_eq.
apply norm_factor_gt_0.
rewrite <- (Rmult_1_r eps).
unfold pos_div_2; simpl; unfold Rdiv.
apply Rmult_lt_compat_l.
apply eps.
apply Rmult_lt_reg_l with 2.
apply Rlt_0_2.
rewrite Rinv_r.
rewrite Rmult_1_r.
apply Rplus_lt_reg_l with (-1); ring_simplify.
apply Rlt_0_1.
apply Rgt_not_eq, Rlt_0_2.
Qed.

Definition clm_CompleteSpaceD_mixin :=
  CompleteSpaceD.Mixin _ Clm_lim complete_cauchy_clm.

Canonical clm_CompleteSpaceD :=
  CompleteSpaceD.Pack (clm E F) (CompleteSpaceD.Class _ _ clm_CompleteSpaceD_mixin) (clm E F).

Canonical clm_CompleteNormedModuleD :=
  CompleteNormedModuleD.Pack _ (clm E F)
     (CompleteNormedModuleD.Class R_AbsRing _
       (NormedModule.class _ (clm_NormedModule E F))
      clm_CompleteSpaceD_mixin) (clm E F).

End clm_complete.