Skip to content

Commit 9c3b607

Browse files
mkerjeanCohenCyril
mkerjean
and
CohenCyril
committed
linfun and lcfun are lmodtypes
Co-authored-by: Cyril Cohen <cohen@crans.org>
1 parent 92fd159 commit 9c3b607

2 files changed

Lines changed: 315 additions & 4 deletions

File tree

‎classical/functions.v‎

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,12 @@ Add Search Blacklist "_mixin_".
128128
(* fctE == multi-rule for fct *)
129129
(* ``` *)
130130
(* *)
131+
(* ``` *)
132+
(*Section linfun_lmodtype == canonical lmodtype structure on linear maps *)
133+
(* between lmodtypes. *)
134+
(* *)
135+
(* *)
136+
(* *)
131137
(******************************************************************************)
132138

133139
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.
27502756

27512757
Lemma inv_funK T (R : unitRingType) (f : T -> R) : (f\^-1\^-1)%R = f.
27522758
Proof. by apply/funeqP => x; rewrite /inv_fun/= GRing.invrK. Qed.
2759+
2760+
(* TODO : correct - choicetype on {linear _ -> _} is no longer seen, cf bug in
2761+
derive.v when uncommenting *)
2762+
2763+
(*
2764+
Local Open Scope ring_scope.
2765+
Import GRing.Theory.
2766+
2767+
Section linfun_pred.
2768+
(* Beware that lfun is reserved for vector types, hence this one has been
2769+
renamed linfun *)
2770+
Context {K : numDomainType} {E : lmodType K} {F : lmodType K} {s : K -> F -> F}.
2771+
Definition linfun : {pred E -> F} := mem [set f | linear_for s f ].
2772+
Definition linfun_key : pred_key linfun. Proof. exact. Qed.
2773+
Canonical linfun_keyed := KeyedPred linfun_key.
2774+
2775+
End linfun_pred.
2776+
2777+
Section linfun.
2778+
Context {R : numDomainType} {E : lmodType R}
2779+
{F : lmodType R} {s : GRing.Scale.law R F}.
2780+
Notation T := {linear E -> F | s}.
2781+
Notation linfun := (@linfun _ E F s).
2782+
2783+
Section Sub.
2784+
Context (f : E -> F) (fP : f \in linfun).
2785+
2786+
Definition linfun_Sub_subproof :=
2787+
@GRing.isLinear.Build _ E F s f (set_mem fP).
2788+
2789+
#[local] HB.instance Definition _ := linfun_Sub_subproof.
2790+
Definition linfun_Sub : {linear _ -> _ | _ } := f.
2791+
End Sub.
2792+
2793+
Lemma linfun_rect (K : T -> Type) :
2794+
(forall f (Pf : f \in linfun), K (linfun_Sub Pf)) -> forall u : T, K u.
2795+
Proof.
2796+
move=> Ksub [f] [[[Pf1 Pf2]] [Pf3]].
2797+
set G := (G in K G).
2798+
have Pf : f \in linfun.
2799+
by rewrite inE /= => // x u y; rewrite Pf2 Pf3.
2800+
suff -> : G = linfun_Sub Pf by apply: Ksub.
2801+
rewrite {}/G.
2802+
congr GRing.Linear.Pack.
2803+
congr GRing.Linear.Class.
2804+
- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
2805+
- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
2806+
Qed.
2807+
2808+
Lemma linfun_valP f (Pf : f \in linfun) : linfun_Sub Pf = f :> (_ -> _).
2809+
Proof. by []. Qed.
2810+
2811+
HB.instance Definition _ := isSub.Build _ _ T linfun_rect linfun_valP.
2812+
2813+
Lemma linfuneqP (f g : {linear E -> F | s}) : f = g <-> f =1 g.
2814+
Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
2815+
2816+
HB.instance Definition _ := [Choice of {linear E -> F | s} by <:].
2817+
2818+
Variant linfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
2819+
| Islinfun (l : {linear E -> F | s}) : linfun_spec f l true.
2820+
2821+
(*to be renamed ?*)
2822+
Lemma linfunE (f : E -> F) : (f \in linfun) -> linfun_spec f f (f \in linfun).
2823+
Proof.
2824+
move=> /[dup] f_lc ->.
2825+
have {2}-> :(f = (linfun_Sub f_lc)) by rewrite linfun_valP.
2826+
constructor.
2827+
Qed.
2828+
2829+
End linfun.
2830+
2831+
Section linfun_comp.
2832+
2833+
Context {R : numDomainType} {E F : lmodType R}
2834+
{S : lmodType R} {s : GRing.Scale.law R S}
2835+
(f : {linear E -> F}) (g : {linear F -> S | s}).
2836+
2837+
Lemma linfun_comp_subproof : linear_for s (g \o f).
2838+
Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
2839+
2840+
HB.instance Definition _ := @GRing.isLinear.Build R E S s (g \o f)
2841+
linfun_comp_subproof.
2842+
(* HB warning : no new instance generated but before we have
2843+
Fail Check ( (g \o f) : {linear E -> F | s}). ? *)
2844+
2845+
End linfun_comp.
2846+
2847+
Section linfun_lmodtype.
2848+
Context {R : numFieldType} {E F G: lmodType R}.
2849+
2850+
Implicit Types (r : R) (f g : {linear E -> F}) (h : {linear F -> G}).
2851+
2852+
Import GRing.Theory.
2853+
2854+
Lemma linfun0 : (\0 : {linear E -> F}) =1 cst 0 :> (_ -> _). Proof. by []. Qed.
2855+
2856+
Lemma linfun_submod_closed : submod_closed (@linfun R E F *:%R).
2857+
Proof.
2858+
split; first by rewrite inE; apply/linearP.
2859+
move=> r /= _ _ /linfunE[f] /linfunE[g].
2860+
by rewrite inE /=; exact: linearP.
2861+
Qed.
2862+
2863+
HB.instance Definition _ :=
2864+
@GRing.isSubmodClosed.Build _ _ linfun linfun_submod_closed.
2865+
2866+
HB.instance Definition _ :=
2867+
[SubChoice_isSubLmodule of {linear E -> F } by <:].
2868+
2869+
End linfun_lmodtype.*)

‎theories/normedtype_theory/tvs.v‎

Lines changed: 198 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
1+
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
22
From HB Require Import structures.
33
From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector.
44
From mathcomp Require Import interval_inference.
@@ -37,10 +37,10 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
3737
(* UniformZmodule == HB class, join of UniformNmodule and Zmodule *)
3838
(* with uniformly continuous opposite operator *)
3939
(* PreUniformLmodule K == HB class, join of Uniform and Lmodule over K *)
40-
(* K is a numDomainType. *)
40+
(* K is a numDomainType *)
4141
(* UniformLmodule K == HB class, join of UniformNmodule and Lmodule *)
4242
(* with a uniformly continuous scaling operation *)
43-
(* K is a numFieldType. *)
43+
(* K is a numFieldType *)
4444
(* convexTvsType R == interface type for a locally convex *)
4545
(* tvs on a numDomain R *)
4646
(* A convex tvs is constructed over a uniform *)
@@ -49,7 +49,6 @@ From mathcomp Require Import pseudometric_normed_Zmodule.
4949
(* PreTopologicalLmod_isConvexTvs == factory allowing the construction of a *)
5050
(* convex tvs from an Lmodule which is also a *)
5151
(* topological space *)
52-
(* ``` *)
5352
(* HB instances: *)
5453
(* - The type R^o (R : numFieldType) is endowed with the structure of *)
5554
(* ConvexTvs. *)
@@ -603,3 +602,198 @@ HB.instance Definition _ :=
603602
Uniform_isConvexTvs.Build K (E * F)%type prod_locally_convex.
604603

605604
End prod_ConvexTvs.
605+
606+
HB.structure Definition LinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
607+
(F : NbhsZmodule.type) (s : K -> F -> F) :=
608+
{f of @GRing.Linear K E F s f & @Continuous E F f }.
609+
610+
(* https://github.com/math-comp/math-comp/issues/1536
611+
we use GRing.Scale.law even though it is claimed to be internal *)
612+
HB.factory Structure isLinearContinuous (K : numDomainType) (E : NbhsLmodule.type K)
613+
(F : NbhsZmodule.type) (s : GRing.Scale.law K F) (f : E -> F) := {
614+
linearP : linear_for s f ;
615+
continuousP : continuous f
616+
}.
617+
618+
HB.builders Context K E F s f of @isLinearContinuous K E F s f.
619+
620+
HB.instance Definition _ := GRing.isLinear.Build K E F s f linearP.
621+
HB.instance Definition _ := isContinuous.Build E F f continuousP.
622+
623+
HB.end.
624+
625+
Section lcfun_pred.
626+
Context {K : numDomainType} {E : NbhsLmodule.type K} {F : NbhsZmodule.type} {s : K -> F -> F}.
627+
Definition lcfun : {pred E -> F} := mem [set f | linear_for s f /\ continuous f ].
628+
Definition lcfun_key : pred_key lcfun. Proof. exact. Qed.
629+
Canonical lcfun_keyed := KeyedPred lcfun_key.
630+
631+
End lcfun_pred.
632+
633+
Reserved Notation "'{' 'linear_continuous' U '->' V '|' s '}'"
634+
(at level 0, U at level 98, V at level 99,
635+
format "{ 'linear_continuous' U -> V | s }").
636+
Reserved Notation "'{' 'linear_continuous' U '->' V '}'"
637+
(at level 0, U at level 98, V at level 99,
638+
format "{ 'linear_continuous' U -> V }").
639+
Notation "{ 'linear_continuous' U -> V | s }" := (@LinearContinuous.type _ U%type V%type s)
640+
: type_scope.
641+
Notation "{ 'linear_continuous' U -> V }" := {linear_continuous U%type -> V%type | *:%R}
642+
: type_scope.
643+
644+
Section lcfun.
645+
Context {R : numDomainType} {E : NbhsLmodule.type R}
646+
{F : NbhsZmodule.type} {s : GRing.Scale.law R F}.
647+
Notation T := {linear_continuous E -> F | s}.
648+
Notation lcfun := (@lcfun _ E F s).
649+
650+
Section Sub.
651+
Context (f : E -> F) (fP : f \in lcfun).
652+
653+
Definition lcfun_Sub_subproof :=
654+
@isLinearContinuous.Build _ E F s f (proj1 (set_mem fP)) (proj2 (set_mem fP)).
655+
#[local] HB.instance Definition _ := lcfun_Sub_subproof.
656+
Definition lcfun_Sub : {linear_continuous _ -> _ | _ } := f.
657+
End Sub.
658+
659+
Lemma lcfun_rect (K : T -> Type) :
660+
(forall f (Pf : f \in lcfun), K (lcfun_Sub Pf)) -> forall u : T, K u.
661+
Proof.
662+
move=> Ksub [f [[Pf1] [Pf2] [Pf3]]].
663+
set G := (G in K G).
664+
have Pf : f \in lcfun.
665+
by rewrite inE /=; split => // x u v; rewrite Pf1 Pf2.
666+
suff -> : G = lcfun_Sub Pf by apply: Ksub.
667+
rewrite {}/G.
668+
congr LinearContinuous.Pack.
669+
congr LinearContinuous.Class.
670+
- by congr GRing.isNmodMorphism.Axioms_; apply: Prop_irrelevance.
671+
- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance.
672+
- by congr isContinuous.Axioms_; apply: Prop_irrelevance.
673+
Qed.
674+
675+
Lemma lcfun_valP f (Pf : f \in lcfun) : lcfun_Sub Pf = f :> (_ -> _).
676+
Proof. by []. Qed.
677+
678+
HB.instance Definition _ := isSub.Build _ _ T lcfun_rect lcfun_valP.
679+
680+
Lemma lcfuneqP (f g : {linear_continuous E -> F | s}) : f = g <-> f =1 g.
681+
Proof. by split=> [->//|fg]; apply/val_inj/funext. Qed.
682+
683+
HB.instance Definition _ := [Choice of {linear_continuous E -> F | s} by <:].
684+
685+
Variant lcfun_spec (f : E -> F) : (E -> F) -> bool -> Type :=
686+
| Islcfun (l : {linear_continuous E -> F | s}) : lcfun_spec f l true.
687+
688+
(*to be renamed ?*)
689+
Lemma lcfunE (f : E -> F) : (f \in lcfun) -> lcfun_spec f f (f \in lcfun).
690+
Proof.
691+
move=> /[dup] f_lc ->.
692+
have {2}-> :(f = (lcfun_Sub f_lc)) by rewrite lcfun_valP.
693+
constructor.
694+
Qed.
695+
696+
End lcfun.
697+
698+
Section lcfun_comp.
699+
700+
Context {R : numDomainType} {E F : NbhsLmodule.type R}
701+
{S : NbhsZmodule.type} {s : GRing.Scale.law R S}
702+
(f : {linear_continuous E -> F}) (g : {linear_continuous F -> S | s}).
703+
704+
Lemma lcfun_comp_subproof1 : linear_for s (g \o f).
705+
Proof. by move=> *; move=> */=; rewrite !linearP. Qed.
706+
707+
(* TODO weaken proof continuous_comp to arbitrary nbhsType *)
708+
Lemma lcfun_comp_subproof2 : continuous (g \o f).
709+
Proof. by move=> x; move=> A /cts_fun /cts_fun. Qed.
710+
711+
HB.instance Definition _ := @isLinearContinuous.Build R E S s (g \o f)
712+
lcfun_comp_subproof1 lcfun_comp_subproof2.
713+
714+
End lcfun_comp.
715+
716+
Section lcfun_lmodtype.
717+
Context {R : numFieldType} {E F G: convexTvsType R}.
718+
719+
Implicit Types (r : R) (f g : {linear_continuous E -> F}) (h : {linear_continuous F -> G}).
720+
721+
Import GRing.Theory.
722+
723+
Lemma null_fun_continuous : continuous (\0 : E -> F).
724+
Proof.
725+
by apply: cst_continuous.
726+
Qed.
727+
728+
HB.instance Definition _ := isContinuous.Build E F \0 null_fun_continuous.
729+
730+
Lemma lcfun0 : (\0 : {linear_continuous E -> F}) =1 cst 0 :> (_ -> _).
731+
Proof. by []. Qed.
732+
733+
(* NB : cvgD in pseudometric_normedZmodule should be lowered to some common
734+
structure to tvstype and pseudometric, then lcfun doesn't need to exist
735+
anymore *)
736+
Lemma lcfun_cvgD (U : set_system E) {FF : Filter U} f g a b :
737+
f @ U --> a -> g @ U --> b -> (f \+ g) @ U --> a + b.
738+
Proof.
739+
move=> fa ga.
740+
apply: continuous2_cvg; [|by []..].
741+
apply @add_continuous. (* TODO: why the @ ? *)
742+
Qed.
743+
744+
Lemma lcfun_continuousD f g : continuous (f \+ g).
745+
Proof. move=> /= x; apply: lcfun_cvgD; apply: cts_fun. Qed.
746+
747+
748+
Lemma lcfun_cvgN (U : set_system E) {FF : Filter U} f a : f @ U --> a -> \- f @ U --> - a.
749+
Proof. by move=> ?; apply: continuous_cvg => //; exact: opp_continuous. Qed.
750+
751+
752+
Lemma lcfun_continuousN f : continuous (\- f).
753+
Proof.
754+
by move=> /= x; apply: lcfun_cvgN; apply: cts_fun.
755+
Qed.
756+
757+
HB.instance Definition _ f g := isContinuous.Build E F (f \+ g) (@lcfun_continuousD f g).
758+
759+
Lemma lcfun_cvgZ (U : set_system E) {FF : Filter U} l f r a : l @ U --> r -> f @ U --> a ->
760+
l x *: f x @[x --> U] --> r *: a.
761+
Proof.
762+
move=> ? ?; apply: continuous2_cvg => //; exact: (scale_continuous (_, _)).
763+
Qed.
764+
765+
Lemma lcfun_cvgZr (U : set_system E) {FF : Filter U} k f a : f @ U --> a -> k \*: f @ U --> k *: a.
766+
Proof. apply: lcfun_cvgZ => //; exact: cvg_cst. Qed.
767+
768+
Lemma lcfun_continuousM r g : continuous (r \*: g).
769+
Proof. by move=> /= x; apply: lcfun_cvgZr; apply: cts_fun. Qed.
770+
771+
HB.instance Definition _ r g := isContinuous.Build E F (r \*: g) (@lcfun_continuousM r g).
772+
773+
Lemma lcfun_submod_closed : submod_closed (@lcfun R E F *:%R).
774+
Proof.
775+
split; first by rewrite inE; split; first apply/linearP; apply: cst_continuous.
776+
move=> r /= _ _ /lcfunE[f] /lcfunE[g].
777+
by rewrite inE /=; split; [exact: linearP | exact: lcfun_continuousD].
778+
Qed.
779+
780+
HB.instance Definition _ f := isContinuous.Build E F (\- f) (@lcfun_continuousN f).
781+
782+
HB.instance Definition _ :=
783+
@GRing.isSubmodClosed.Build _ _ lcfun lcfun_submod_closed.
784+
785+
HB.instance Definition _ :=
786+
[SubChoice_isSubLmodule of {linear_continuous E -> F } by <:].
787+
788+
End lcfun_lmodtype.
789+
790+
791+
Section Substructures.
792+
Context (R: numFieldType) (V : convexTvsType R).
793+
Variable (A : pred V).
794+
795+
HB.instance Definition _ := ConvexTvs.on (subspace A).
796+
797+
Check {linear_continuous (subspace A) -> R^o}.
798+
799+
End Substructures.

0 commit comments

Comments
 (0)