Linear_continuous structure

classical/functions.v

@@ -128,6 +128,12 @@ Add Search Blacklist "_mixin_".
 (*                   fctE == multi-rule for fct                               *)
 (* ```                                                                        *)
 (*                                                                            *)
+(* ```                                                                        *)
+(*Section linfun_lmodtype == canonical lmodtype structure on linear maps      *)
+(*                           between lmodtypes.                               *)
+(*                                                                            *)
+(*                                                                            *)
+(*                                                                            *)
 (******************************************************************************)
 
 Set SsrOldRewriteGoalsOrder.  (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
@@ -2750,3 +2756,114 @@ End function_space_lemmas.
 
 Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
 Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
+
+(* TODO : correct - choicetype on {linear _ -> _} is no longer seen, cf bug in
+derive.v when uncommenting *)
+
+(*
+Local Open Scope ring_scope.
+Import GRing.Theory.
+
+Section linfun_pred.
+(* Beware that lfun is reserved for vector types, hence this one has been
+renamed linfun *)
+Context  {K : numDomainType} {E : lmodType K}  {F : lmodType K} {s : K -> F -> F}.
+Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
+Definition linfun_key : pred_key linfun. Proof. exact. Qed.
+Canonical linfun_keyed := KeyedPred linfun_key.
+
+End linfun_pred.
+
+Section linfun.
+Context {R : numDomainType} {E : lmodType R}
+  {F : lmodType R} {s : GRing.Scale.law R F}.
+Notation T := {linear E -> F | s}.
+Notation linfun := (@linfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in linfun).
+
+Definition linfun_Sub_subproof :=
+  @GRing.isLinear.Build _ E F s f  (set_mem fP).
+
+#[local] HB.instance Definition _ := linfun_Sub_subproof.
+Definition linfun_Sub : {linear _  -> _ | _ } := f.
+End Sub.
+
+Lemma linfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
+set G := (G in K G).
+have Pf : f \in linfun.
+  by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
+suff -> : G = linfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr GRing.Linear.Pack. 
+congr GRing.Linear.Class.
+- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance. 
+- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
+
+Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
+
+Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+  | Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
+
+(*to be renamed ?*)
+Lemma linfunE (f : E -> F) : (f \in linfun) -> linfun_spec f f (f \in linfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
+constructor.
+Qed.
+
+End linfun.
+
+Section linfun_comp.
+
+Context {R : numDomainType} {E F : lmodType R}
+  {S : lmodType R} {s : GRing.Scale.law R S}
+  (f : {linear E -> F}) (g : {linear F -> S | s}).
+
+Lemma linfun_comp_subproof : linear_for s (g \o f). 
+Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+
+HB.instance Definition _ := @GRing.isLinear.Build R E S s (g \o f)
+  linfun_comp_subproof.  
+(* HB warning : no new instance generated but before we have 
+Fail Check ( (g \o f) : {linear E -> F | s}). ? *)
+
+End linfun_comp.
+
+Section linfun_lmodtype.
+Context {R : numFieldType} {E F G: lmodType R}. 
+
+Implicit Types (r : R) (f g : {linear E -> F}) (h : {linear F -> G}).  
+
+Import GRing.Theory.
+
+Lemma linfun0 : (\0 : {linear E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
+
+Lemma linfun_submod_closed  : submod_closed (@linfun R E F *:%R).
+Proof.
+split; first by rewrite inE; apply/linearP.  
+move=> r /= _ _  /linfunE[f] /linfunE[g].
+by rewrite inE /=; exact: linearP.
+Qed. 
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ linfun linfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear E -> F } by <:].
+
+End linfun_lmodtype.*)

theories/normedtype_theory/tvs.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *) 
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
 From mathcomp Require Import interval_inference.
@@ -37,10 +37,10 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (*           UniformZmodule == HB class, join of UniformNmodule and Zmodule   *)
 (*                             with uniformly continuous opposite operator    *)
 (*      PreUniformLmodule K == HB class, join of Uniform and Lmodule over K   *)
-(*                             K is a numDomainType.                          *)
+(*                             K is a numDomainType                           *)
 (*         UniformLmodule K == HB class, join of UniformNmodule and Lmodule   *)
 (*                             with a uniformly continuous scaling operation  *)
-(*                             K is a numFieldType.                           *)
+(*                             K is a numFieldType                            *)
 (*         convexTvsType R  == interface type for a locally convex            *)
 (*                             tvs on a numDomain R                           *)
 (*                             A convex tvs is constructed over a uniform     *)
@@ -49,7 +49,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
 (* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a   *)
 (*                             convex tvs from an Lmodule which is also a     *)
 (*                             topological space                              *)
-(*  ```                                                                       *)
 (* HB instances:                                                              *)
 (* - The type R^o (R : numFieldType) is endowed with the structure of         *)
 (*   ConvexTvs.                                                               *)
@@ -603,3 +602,198 @@ HB.instance Definition _ :=
   Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex.
 
 End prod_ConvexTvs.
+
+HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : K -> F -> F) :=
+  {f of @GRing.Linear K E F s f &  @Continuous E F f }.
+
+(* https://github.com/math-comp/math-comp/issues/1536
+   we use GRing.Scale.law even though it is claimed to be internal *)
+HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
+  (F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := {
+    linearP : linear_for s f ;
+    continuousP : continuous f
+  }.
+
+HB.builders Context K E F s f of @isLinearContinuous K E F s f.
+
+HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
+HB.instance Definition _ := isContinuous.Build E F f continuousP.
+
+HB.end.
+
+Section lcfun_pred.
+Context  {K : numDomainType} {E : NbhsLmodule.type K}  {F : NbhsZmodule.type} {s : K -> F -> F}.
+Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ].
+Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
+Canonical lcfun_keyed := KeyedPred lcfun_key.
+
+End lcfun_pred.
+
+Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V  |  s }").
+Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
+  (at level 0, U at level 98, V at level 99,
+   format "{ 'linear_continuous'  U  ->  V }").
+Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
+  : type_scope.
+Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
+  : type_scope.
+
+Section lcfun.
+Context {R : numDomainType} {E : NbhsLmodule.type R}
+  {F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
+Notation T := {linear_continuous E -> F | s}.
+Notation lcfun := (@lcfun _ E F s).
+
+Section Sub.
+Context (f : E -> F) (fP : f \in lcfun).
+
+Definition lcfun_Sub_subproof :=
+  @isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
+#[local] HB.instance Definition _ := lcfun_Sub_subproof.
+Definition lcfun_Sub : {linear_continuous _  -> _ | _ } := f.
+End Sub.
+
+Lemma lcfun_rect (K : T -> Type) :
+  (forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u.
+Proof.
+move=> Ksub [f [[Pf1] [Pf2] [Pf3]]].
+set G := (G in K G).
+have Pf : f \in lcfun.
+  by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
+suff -> : G = lcfun_Sub Pf by apply: Ksub.
+rewrite {}/G.
+congr LinearContinuous.Pack.
+congr LinearContinuous.Class.
+- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
+- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
+- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
+Qed.
+
+Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
+Proof. by []. Qed.
+
+HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
+
+Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
+Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
+
+HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
+
+Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
+  | Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
+
+(*to be renamed ?*)
+Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
+Proof.
+move=> /[dup] f_lc ->.
+have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
+constructor.
+Qed.
+
+End lcfun.
+
+Section lcfun_comp.
+
+Context {R : numDomainType} {E F : NbhsLmodule.type R}
+  {S : NbhsZmodule.type} {s : GRing.Scale.law R S}
+  (f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}).
+
+Lemma lcfun_comp_subproof1 : linear_for s (g \o f). 
+Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
+
+(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
+Lemma lcfun_comp_subproof2 : continuous (g \o f). 
+Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
+
+HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
+  lcfun_comp_subproof1 lcfun_comp_subproof2.
+
+End lcfun_comp.
+
+Section lcfun_lmodtype.
+Context {R : numFieldType} {E F G: convexTvsType R}. 
+
+Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).  
+
+Import GRing.Theory.
+
+Lemma null_fun_continuous : continuous (\0 : E -> F).
+Proof.
+by apply: cst_continuous.
+Qed.
+
+HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
+
+Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _).
+Proof. by []. Qed.
+
+(* NB : cvgD in pseudometric_normedZmodule should be lowered to some common
+structure to tvstype and pseudometric, then lcfun doesn't need to exist
+anymore *)
+Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
+  f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
+Proof.
+move=> fa ga.
+apply: continuous2_cvg; [|by []..].
+apply @add_continuous. (* TODO: why the @ ? *)
+Qed.
+
+Lemma lcfun_continuousD f g : continuous (f \+ g).
+Proof. move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
+
+
+Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : f @ U --> a -> \- f @ U --> - a.
+Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
+
+
+Lemma lcfun_continuousN f : continuous (\- f).
+Proof.
+by move=> /= x; apply: lcfun_cvgN; apply: cts_fun. 
+Qed.
+
+HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
+
+Lemma lcfun_cvgZ  (U : set_system E) {FF : Filter U} l f r a : l @ U  --> r -> f @ U --> a ->
+                     l x *: f x @[x --> U] --> r *: a.
+Proof.
+move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
+Qed.
+
+Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
+Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
+
+Lemma lcfun_continuousM r g : continuous (r \*: g).
+Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
+
+HB.instance Definition _ r g := isContinuous.Build E F (r \*: g)  (@lcfun_continuousM r g).
+
+Lemma lcfun_submod_closed  : submod_closed (@lcfun R E F *:%R).
+Proof.
+split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
+move=> r /= _ _  /lcfunE[f] /lcfunE[g].
+by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
+Qed.
+
+HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
+
+HB.instance Definition _ :=
+  @GRing.isSubmodClosed.Build _  _ lcfun lcfun_submod_closed.
+
+HB.instance Definition _ :=
+  [SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
+
+End lcfun_lmodtype.
+
+
+Section Substructures.
+Context (R: numFieldType) (V : convexTvsType R).
+Variable (A : pred V).
+
+HB.instance Definition _ := ConvexTvs.on (subspace A).
+
+Check {linear_continuous (subspace A) -> R^o}.
+
+End Substructures.