From df561e45d42eda9ba4182d1e6ff7a1d92e1ecdb9 Mon Sep 17 00:00:00 2001 From: qvermande Date: Mon, 29 Sep 2025 18:20:55 +0200 Subject: [PATCH 1/9] algebraic structures on continuousType --- theories/tvs.v | 85 ++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 83 insertions(+), 2 deletions(-) diff --git a/theories/tvs.v b/theories/tvs.v index fe43593043..39096edf01 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -84,12 +84,42 @@ HB.structure Definition PreTopologicalNmodule := HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M of PreTopologicalNmodule M := { - add_continuous : continuous (fun x : M * M => x.1 + x.2) ; + add_continuous : continuous (fst \+ snd : M * M -> M) ; }. HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. +Section TopologicalNmoduleTheory. +Variables (M N : TopologicalNmodule.type). + +Let addfun_continuous (f g : continuousType M N) : continuous (f \+ g). +Proof. +move=> x. +apply: (@continuous_comp _ _ _ (fun x => (f x, g x)) (fst \+ snd)); last first. + exact: add_continuous. +apply: cvg_pair; apply: cts_fun. +Qed. + +HB.instance Definition _ (f g : continuousType M N) := + isContinuous.Build M N (f \+ g) (@addfun_continuous f g). + +Let addrA : associative (fun f g : continuousType M N => f \+ g). +Proof. by move=> f g h; apply/continuousEP => x; apply: addrA. Qed. + +Let addrC : @commutative _ (continuousType M N) + (fun f g : continuousType M N => f \+ g). +Proof. by move=> f g; apply/continuousEP => x; apply: addrC. Qed. + +Let add0r : @left_id (continuousType M N) _ (cst 0) + (fun f g : continuousType M N => f \+ g). +Proof. by move=> f; apply/continuousEP => x; apply: add0r. Qed. + +HB.instance Definition _ := + GRing.isNmodule.Build (continuousType M N) addrA addrC add0r. + +End TopologicalNmoduleTheory. + HB.structure Definition PreTopologicalZmodule := {M of Topological M & GRing.Zmodule M}. @@ -141,7 +171,7 @@ HB.instance Definition _ := HB.end. Section TopologicalZmoduleTheory. -Variables (M : topologicalZmodType). +Variables (M N : topologicalZmodType). Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). Proof. @@ -151,6 +181,21 @@ apply: cvg_pair; first exact: cvg_fst. by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. Qed. +Lemma oppfun_continuous (f : continuousType M N) : continuous (\- f). +Proof. +move=> x; apply: (continuous_comp (@cts_fun _ _ f _) (@opp_continuous N _)). +Qed. + +HB.instance Definition _ (f : continuousType M N) := + isContinuous.Build _ _ (\- f) (@oppfun_continuous f). + +Let addNr : @left_inverse (continuousType M N) _ _ + 0%R (fun f : continuousType M N => \- f) +%R. +Proof. by move=> f; apply/continuousEP => x; apply: addNr. Qed. + +HB.instance Definition _ := + GRing.Nmodule_isZmodule.Build (continuousType M N) addNr. + End TopologicalZmoduleTheory. #[short(type="preTopologicalLmodType")] @@ -192,6 +237,42 @@ HB.instance Definition _ := HB.end. +Section TopologicalLmoduleTheory. +Variables (K : numDomainType) (M N : topologicalLmodType K). + +Lemma scalefun_continuous (k : K) (f : continuousType M N) : + continuous (k \*: f). +Proof. +move=> x. +apply: (@continuous_comp _ _ _ (fun x => (k : K^o, f x)) (fun x => x.1 *: x.2)); + last exact: scale_continuous. +apply: (cvg_pair (@cst_continuous _ K^o k x)). +exact: cts_fun. +Qed. + +HB.instance Definition _ (k : K) (f : continuousType M N) := + isContinuous.Build _ _ (k \*: f) (@scalefun_continuous k f). + +Let scalerA (a b : K) (f : continuousType M N) : + a \*: (b \*: f) = (a * b) \*: f :> continuousType M N. +Proof. by apply/continuousEP => x; apply: scalerA. Qed. + +Let scale1r : left_id 1 (fun k (f : continuousType M N) => k \*: f). +Proof. by move=> f; apply/continuousEP => x; apply: scale1r. Qed. + +Let scalerDr : + right_distributive (fun k (f : continuousType M N) => k \*: f) +%R. +Proof. by move=> f g h; apply/continuousEP => x; apply: scalerDr. Qed. + +Let scalerDl (f : continuousType M N) : + {morph (fun k => k \*: f : continuousType M N) : a b / a + b}. +Proof. by move=> a b; apply/continuousEP => x; apply: scalerDl. Qed. + +HB.instance Definition _ := GRing.Zmodule_isLmodule.Build K (continuousType M N) + scalerA scale1r scalerDr scalerDl. + +End TopologicalLmoduleTheory. + HB.structure Definition PreUniformNmodule := {M of Uniform M & GRing.Nmodule M}. HB.mixin Record PreUniformNmodule_isUniformNmodule M of PreUniformNmodule M := { From 55f3fb147966364d2b7795343fcb28d70400dfb5 Mon Sep 17 00:00:00 2001 From: qvermande Date: Wed, 1 Oct 2025 10:15:56 +0200 Subject: [PATCH 2/9] LinearContinuous --- theories/normedtype_theory/normed_module.v | 64 ++++++++++++++ theories/tvs.v | 99 ++++++++++++++++++++-- 2 files changed, 157 insertions(+), 6 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 65de09594c..2ba27fb01f 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2079,3 +2079,67 @@ by rewrite interior_closed_ballE //; exact: ballxx. Qed. End Closed_Ball_normedModType. + +Section LinearContinuous. +Variables (R : realType) (M N : normedModType R). + +Let norm (f : c0linType M N) := sup [set `|f x| | x in [set x | `|x| <= 1]]. + +Let normP (f : c0linType M N) : has_sup [set `|f x| | x in [set x | `|x| <= 1]]. +Proof. +have := @cts_fun _ _ f 0 (ball 0 1) => /(_ _)/wrap[]. + by rewrite linear0; apply: nbhsx_ballx. +move=> /nbhs_closedballP => -[] [] e/= /andP[_]. +rewrite /map_itv/= in_itv/= mulr0z andbT => e0 fe. +split; first by exists 0, 0 => /=; rewrite ?linear0 normr0. +exists (e^-1)%R => d [] x/= x1 <-. +rewrite -[leRHS]mul1r ler_pdivlMr// -(gtr0_norm e0) mulrC -normrZ -linearZ. +move: fe => /(_ (e *: x))/= /(_ _)/wrap[]; last first. + by rewrite -ball_normE/= add0r normrN => /ltW. +rewrite closed_ballE//= /closed_ball_/= add0r normrN normrZ gtr0_norm//. +by rewrite -ler_pdivlMl// mulVf// lt0r_neq0. +Qed. + +Let ler_normD f g : norm (f + g) <= norm f + norm g. +Proof. +apply: sup_le_ub; first by case: (normP (f + g)). +move=> _ []/= x x1 <-. +apply/(le_trans (ler_normD _ _))/lerD. + by apply: (sup_upper_bound (normP f)); exists x. +by apply: (sup_upper_bound (normP g)); exists x. +Qed. + +Let normr0_eq0 f : norm f = 0 -> f = 0. +Proof. +move=> f0; apply/c0linEP => x. +have [->|] := eqVneq x 0; first exact: linear0. +rewrite -normr_gt0 -invr_gt0 => x0. +apply/eqP; rewrite -normr_le0. +rewrite -(pmulr_rle0 _ x0) -(gtr0_norm x0) -normrZ -linearZ -f0. +apply: (sup_upper_bound (normP f)); exists (`|x|^-1 *: x) => //=. +by rewrite normrZ (gtr0_norm x0) mulVf// lt0r_neq0// -invr_gt0. +Qed. + +Let normrZ l f : norm (l *: f) = `|l| * norm f. +Proof. +apply/le_anti/andP; split. + apply: sup_le_ub; first by case: (normP (l *: f)). + move=> _ []/= x x1 <-. + rewrite normrZ; apply: ler_pM => //. + by apply: (sup_upper_bound (normP f)); exists x. +have [->|] := eqVneq l 0. + rewrite normr0 mul0r scale0r. + by apply: (sup_upper_bound (normP 0)); exists 0 => /=; rewrite ?cstE normr0. +rewrite -normr_gt0 => l0. +rewrite -ler_pdivlMl//. +apply: sup_le_ub; first by case: (normP f). +move=> _ []/= x x1 <-. +rewrite ler_pdivlMl// -normrZ. +by apply: (sup_upper_bound (normP (l *: f))); exists x. +Qed. + + +HB.instance Definition _ := Lmodule_isNormed.Build R (c0linType M N) + ler_normD normrZ normr0_eq0. + +End LinearContinuous. diff --git a/theories/tvs.v b/theories/tvs.v index 39096edf01..193659a0b9 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -91,7 +91,7 @@ HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. Section TopologicalNmoduleTheory. -Variables (M N : TopologicalNmodule.type). +Variables (M : topologicalType) (N : TopologicalNmodule.type). Let addfun_continuous (f g : continuousType M N) : continuous (f \+ g). Proof. @@ -171,12 +171,12 @@ HB.instance Definition _ := HB.end. Section TopologicalZmoduleTheory. -Variables (M N : topologicalZmodType). +Variables (M : topologicalType) (N : topologicalZmodType). -Lemma sub_continuous : continuous (fun x : M * M => x.1 - x.2). +Lemma sub_continuous : continuous (fun x : N * N => x.1 - x.2). Proof. -move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) - (fun x : M * M => x.1 + x.2)); last exact: add_continuous. +move=> x; apply: (@continuous_comp _ _ _ (fun x => (x.1, - x.2)) (fst \+ snd)); + last exact: add_continuous. apply: cvg_pair; first exact: cvg_fst. by apply: continuous_comp; [exact: cvg_snd|exact: opp_continuous]. Qed. @@ -238,7 +238,7 @@ HB.instance Definition _ := HB.end. Section TopologicalLmoduleTheory. -Variables (K : numDomainType) (M N : topologicalLmodType K). +Variables (K : numDomainType) (M : topologicalType) (N : topologicalLmodType K). Lemma scalefun_continuous (k : K) (f : continuousType M N) : continuous (k \*: f). @@ -734,3 +734,90 @@ HB.instance Definition _ := Uniform_isTvs.Build K (E * F)%type prod_locally_convex. End prod_Tvs. + +#[short(type="c0linType")] +HB.structure Definition ContinuousLinear + (K : numDomainType) (M N : preTopologicalLmodType K) := + {f of @Continuous M N f & @GRing.Linear K M N *:%R f}. + +HB.instance Definition _ (K : numDomainType) (M : preTopologicalLmodType K) := + Continuous.on (@idfun M). + +HB.instance Definition _ (K : numDomainType) (M N T : preTopologicalLmodType K) + (f : c0linType M N) (g : c0linType N T) := + Continuous.on (comp g f). + +HB.instance Definition _ (K : numDomainType) (M N : topologicalLmodType K) + (f g : c0linType M N) := + Continuous.on (f \+ g). + +HB.instance Definition _ (K : numDomainType) (M N : topologicalLmodType K) + (f : c0linType M N) := + Continuous.on (\- f). + +HB.instance Definition _ (K : numDomainType) (M N : topologicalLmodType K) + (k : K) (f : c0linType M N) := + Continuous.on (k \*: f). + +Section ContinuousLinear_sub_Continuous. +Variables (K : numDomainType) (M N : preTopologicalLmodType K). + +Lemma c0linEP (f g : c0linType M N) : f = g <-> f =1 g. +Proof. +split=> [-> //|/funext]. +case: f g => f + [] g +/= fg. +rewrite fg => -[] [] fc0 [] fadd [] fscal [] [] gc0 [] gadd [] gscal. +congr ContinuousLinear.Pack. +congr ContinuousLinear.Class. +- by congr isContinuous.Axioms_; apply: Prop_irrelevance. +- by congr GRing.isSemiAdditive.Axioms_; apply: Prop_irrelevance. +- by congr GRing.isScalable.Axioms_; apply: Prop_irrelevance. +Qed. + +Let val (f : c0linType M N) := f : continuousType M N. + +Let sub_subproof (f : continuousType M N) : `[< linear_for *:%R f >] -> + ContinuousLinear.axioms_ (f : continuousType M N). +Proof. +move=> /asboolP flin. +set g := (HB.pack_for (c0linType M N) (Continuous.sort f) + (GRing.isLinear.Build K M N *:%R f flin)). +exact: (ContinuousLinear.class g). +Qed. + +Let sub (f : continuousType M N) : `[< linear_for *:%R f >] -> c0linType M N. +Proof. by exists f; apply: sub_subproof. Defined. + +Let subK f Pf : val (@sub f Pf) = f. +Proof. exact/continuousEP. Qed. + +Let sub_rect P : (forall f Pf, P (@sub f Pf)) -> forall f, P f. +Proof. +move=> /[swap] f /(_ f _)/wrap[]. + by apply/asboolP => k x y; rewrite [LHS]raddfD/= linearZ. +by move=> xP; congr P; apply/c0linEP. +Qed. + +HB.instance Definition _ := isSub.Build _ _ (c0linType M N) sub_rect subK. + +HB.instance Definition _ := + Choice.copy (c0linType M N) (sub_type (c0linType M N)). + +End ContinuousLinear_sub_Continuous. + +Section ContinuousLinear_sub_Continuous. +Variables (K : numDomainType) (M : preTopologicalLmodType K) (N : topologicalLmodType K). + +Let submod_closed : @submod_closed K (continuousType M N) + (fun f => `[< linear_for *:%R f >]). +Proof. +split=> [|k f g]; first by rewrite inE => k x y; rewrite addr0 scaler0. +rewrite !inE => flin glin r x y. +rewrite [X in _ *: X + _ = _]flin [X in _ + X = _]glin !scalerDr !scalerA. +by rewrite addrACA mulrC. +Qed. + +HB.instance Definition _ := GRing.SubChoice_isSubLmodule.Build + K (continuousType M N) _ (c0linType M N) submod_closed. + +End ContinuousLinear_sub_Continuous. From 1581ebad7afbd2191c535ab13e1655fb044f3e67 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 14 Oct 2025 14:36:33 +0200 Subject: [PATCH 3/9] make diff use c0linType --- theories/derive.v | 234 ++++++++++-------- .../normedtype_theory/matrix_normedtype.v | 1 + theories/tvs.v | 3 + 3 files changed, 129 insertions(+), 109 deletions(-) diff --git a/theories/derive.v b/theories/derive.v index 3e9e0608fd..bee1c43882 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -67,7 +67,7 @@ Section Differential. Context {K : numDomainType} {V W : normedModType K}. Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) := - (get (fun (df : {linear V -> W}) => continuous df /\ forall x, + (get (fun (df : c0linType V W) => forall x, f x = f (lim F) + df (x - lim F) +o_(x \near F) (x - lim F))). Local Notation "''d' f x" := (@diff _ (Phantom _ (nbhs x)) f). @@ -75,8 +75,7 @@ Local Notation "''d' f x" := (@diff _ (Phantom _ (nbhs x)) f). Fact diff_key : forall T, T -> unit. Proof. by constructor. Qed. CoInductive differentiable_def (f : V -> W) (x : filter_on V) (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of - (continuous ('d f x) /\ - f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))). + f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x)). Local Notation differentiable f F := (@differentiable_def f _ (Phantom _ (nbhs F))). @@ -90,20 +89,19 @@ Hint Mode is_diff_def - - ! - : typeclass_instances. Lemma diffP (F : filter_on V) (f : V -> W) : differentiable f F <-> - continuous ('d f F) /\ (forall x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F)). Proof. by split=> [[] |]; last constructor; rewrite funeqE. Qed. Lemma diff_continuous (x : filter_on V) (f : V -> W) : - differentiable f x -> continuous ('d f x). -Proof. by move=> /diffP []. Qed. + continuous ('d f x). +Proof. exact: cts_fun. Qed. (* We should have a continuous class or structure *) Hint Extern 0 (continuous _) => solve[apply: diff_continuous] : core. Lemma diffE (F : filter_on V) (f : V -> W) : differentiable f F -> forall x, f x = f (lim F) + 'd f F (x - lim F) +o_(x \near F) (x - lim F). -Proof. by move=> /diffP []. Qed. +Proof. by move=> /diffP. Qed. Lemma littleo_center0 (x : V) (f : V -> W) (e : V -> V) : [o_x e of f] = [o_ 0 (e \o shift x) of f \o shift x] \o center x. @@ -128,14 +126,14 @@ Local Notation "''d' f x" := (@diff _ _ _ _ (Phantom _ (nbhs x)) f). Hint Extern 0 (continuous _) => solve[now apply: diff_continuous] : core. Lemma diff_locallyxP (x : V) (f : V -> W) : - differentiable f x <-> continuous ('d f x) /\ + differentiable f x <-> forall h, f (h + x) = f x + 'd f x h +o_(h \near 0) h. Proof. -split=> [dxf|[dfc dxf]]. - split => //; apply: eqaddoEx => h; have /diffE -> := dxf. +split=> dxf. + apply: eqaddoEx => h; have /diffE -> := dxf. rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK. by congr ('o); rewrite funeqE => k /=; rewrite addrK. -apply/diffP; split=> //; apply: eqaddoEx; move=> y. +apply/diffP/eqaddoEx; move=> y. rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _). rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x). by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0. @@ -143,7 +141,7 @@ Qed. Lemma diff_locallyx (x : V) (f : V -> W) : differentiable f x -> forall h, f (h + x) = f x + 'd f x h +o_(h \near 0) h. -Proof. by move=> /diff_locallyxP []. Qed. +Proof. by move=> /diff_locallyxP. Qed. Lemma diff_locallyxC (x : V) (f : V -> W) : differentiable f x -> forall h, f (x + h) = f x + 'd f x h +o_(h \near 0) h. @@ -151,12 +149,12 @@ Proof. by move=> ?; apply/eqaddoEx => h; rewrite [x + h]addrC diff_locallyx. Qed Lemma diff_locallyP (x : V) (f : V -> W) : differentiable f x <-> - continuous ('d f x) /\ (f \o shift x = cst (f x) + 'd f x +o_ 0 id). + f \o shift x = cst (f x) + 'd f x +o_ 0 id. Proof. by apply: iff_trans (diff_locallyxP _ _) _; rewrite funeqE. Qed. Lemma diff_locally (x : V) (f : V -> W) : differentiable f x -> (f \o shift x = cst (f x) + 'd f x +o_ 0 id). -Proof. by move=> /diff_locallyP []. Qed. +Proof. by move=> /diff_locallyP. Qed. End Differential_numFieldType. @@ -192,11 +190,11 @@ Context {R : numFieldType} {V W : normedModType R}. Lemma differentiable_continuous (x : V) (f : V -> W) : differentiable f x -> {for x, continuous f}. Proof. -move=> /diff_locallyP [dfc]; rewrite -addrA. +move=> /diff_locallyP; rewrite -addrA. rewrite (littleo_bigO_eqo (cst (1 : R))); last first. by apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1; near do by []. rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r. -by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0. +by apply/eqolim0P; apply: (cvg_trans (cts_fun 0)); rewrite linear0. Unshelve. all: by end_near. Qed. Section littleo_lemmas. @@ -398,10 +396,9 @@ Notation derivemxE := deriveEjacobian (only parsing). Section DifferentialR3. Variable R : numFieldType. -Fact dcst (V W : normedModType R) (a : W) (x : V) : continuous (0 : V -> W) /\ +Fact dcst (V W : normedModType R) (a : W) (x : V) : cst a \o shift x = cst (cst a x) + \0 +o_ 0 id. Proof. -split; first exact: cst_continuous. apply/eqaddoE; rewrite addr0 funeqE => ? /=; rewrite -[LHS]addr0; congr (_ + _). by rewrite littleoE; last exact: littleo0_subproof. Qed. @@ -410,20 +407,18 @@ Variables (V W : normedModType R). Fact dadd (f g : V -> W) x : differentiable f x -> differentiable g x -> - continuous ('d f x \+ 'd g x) /\ (f + g) \o shift x = cst ((f + g) x) + ('d f x \+ 'd g x) +o_ 0 id. Proof. -move=> df dg; split => [?|]; do ?exact: continuousD. +move=> df dg. apply/(@eqaddoE R); rewrite funeqE => y /=; rewrite -[(f + g) _]/(_ + _). by rewrite ![_ (_ + x)]diff_locallyx// addrACA addox addrACA. Qed. Fact dopp (f : V -> W) x : - differentiable f x -> continuous (- ('d f x : V -> W)) /\ + differentiable f x -> (- f) \o shift x = cst (- f x) \- 'd f x +o_ 0 id. Proof. -move=> df; split; first by move=> ?; apply: continuousN. -apply/eqaddoE; rewrite funeqE => y /=. +move=> df; apply/eqaddoE; rewrite funeqE => y /=. by rewrite -[(- f) _]/(- (_ _)) diff_locallyx// !opprD oppox. Qed. @@ -432,31 +427,27 @@ Lemma is_diff_eq (V' W' : normedModType R) (f f' g : V' -> W') (x : V') : Proof. by move=> ? <-. Qed. Fact dscale (f : V -> W) k x : - differentiable f x -> continuous (k \*: 'd f x) /\ + differentiable f x -> (k *: f) \o shift x = cst ((k *: f) x) + k \*: 'd f x +o_ 0 id. Proof. -move=> df; split; first by move=> ?; apply: continuousZl_tmp. -apply/eqaddoE; rewrite funeqE => y /=. +move=> df; apply/eqaddoE; rewrite funeqE => y /=. by rewrite -[(k *: f) _]/(_ *: _) diff_locallyx // !scalerDr scaleox. Qed. (* NB: could be generalized with K : absRingType instead of R; DONE? *) Fact dscalel (k : V -> R) (f : W) x : differentiable k x -> - continuous (fun z : V => 'd k x z *: f) /\ (fun z => k z *: f) \o shift x = cst (k x *: f) + (fun z => 'd k x z *: f) +o_ 0 id. Proof. -move=> df; split. - move=> ?; exact/continuousZr_tmp/diff_continuous. -apply/eqaddoE; rewrite funeqE => y /=. +move=> df; apply/eqaddoE; rewrite funeqE => y /=. by rewrite diff_locallyx //= !scalerDl scaleolx. Qed. -Fact dlin (V' W' : normedModType R) (f : {linear V' -> W'}) x : - continuous f -> f \o shift x = cst (f x) + f +o_ 0 id. +Fact dlin (V' W' : normedModType R) (f : c0linType V' W') x : + f \o shift x = cst (f x) + f +o_ 0 id. Proof. -move=> df; apply: eqaddoE; rewrite funeqE => y /=. +apply: eqaddoE; rewrite funeqE => y /=. rewrite linearD addrC -[LHS]addr0; congr (_ + _). by rewrite littleoE; last exact: littleo0_subproof. (*fixme*) Qed. @@ -520,11 +511,11 @@ by rewrite -mulrA mulVf ?lt0r_neq0 // mulr1 [ltRHS]splitr ltrDl. Qed. Lemma diff_unique (V W : normedModType R) (f : V -> W) - (df : {linear V -> W}) x : - continuous df -> f \o shift x = cst (f x) + df +o_ 0 id -> + (df : c0linType V W) x : + f \o shift x = cst (f x) + df +o_ 0 id -> 'd f x = df :> (V -> W). Proof. -move=> dfc dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _). +move=> dxf; apply/subr0_eq; rewrite -[LHS]/(_ \- _). apply/littleo_linear0/eqoP/eq_some_oP => /=; rewrite funeqE => y /=. have hdf h : (f \o shift x = cst (f x) + h +o_ 0 id) -> h = f \o shift x - cst (f x) +o_ 0 id. @@ -536,10 +527,10 @@ rewrite (hdf _ dxf). suff /diff_locally /hdf -> : differentiable f x. by rewrite opprD addrCA -(addrA (_ - _)) addKr oppox addox. apply/diffP => /=. -apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\ +apply: (@getPex _ (fun (df : c0linType V W) => forall y, f y = f (lim (nbhs x)) + df (y - lim (nbhs x)) +o_(y \near x) (y - lim (nbhs x)))). -exists df; split=> //; apply: eqaddoEx => z. +exists df; apply: eqaddoEx => z. rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK. rewrite -addrA -[LHS]addr0; congr (_ + _). apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP. @@ -547,8 +538,11 @@ rewrite [in LHS]littleo_center0 (comp_centerK x id). by rewrite -[- _ in RHS](comp_centerK x). Qed. -Lemma diff_cst (V W : normedModType R) a x : ('d (cst a) x : V -> W) = 0. -Proof. by apply/diff_unique; have [] := dcst a x. Qed. +Lemma diff_cst (V W : normedModType R) a x : 'd (cst a) x = 0 :> (V -> W). +Proof. +rewrite -[RHS]/((0 : c0linType V W) : V -> W). +by apply: diff_unique; have := dcst a x. +Qed. Variables (V W : normedModType R). @@ -584,11 +578,8 @@ by elim/big_ind : _ => // ? ? g h ?; apply: differentiableD; [exact:g|exact:h]. Qed. Lemma diffN (f : V -> W) x : - differentiable f x -> 'd (- f) x = - ('d f x : V -> W) :> (V -> W). -Proof. -move=> df; rewrite -[RHS]/(@GRing.opp _ \o _); apply/diff_unique; -by have [] := dopp df. -Qed. + differentiable f x -> 'd (- f) x = - 'd f x :> (V -> W). +Proof. by move=> df; apply/diff_unique; have := dopp df. Qed. Lemma differentiableN (f : V -> W) x : differentiable f x -> differentiable (- f) x. @@ -600,7 +591,7 @@ Global Instance is_diffN (f df : V -> W) x : is_diff x f df -> is_diff x (- f) (- df). Proof. move=> dfx; apply: DiffDef; first exact: differentiableN. -by rewrite diffN // diff_val. +by rewrite diffN //= diff_val. Qed. Global Instance is_diffB (f g df dg : V -> W) x : @@ -638,27 +629,33 @@ Qed. Lemma diffZl (k : V -> R) (f : W) x : differentiable k x -> 'd (fun z => k z *: f) x = (fun z => 'd k x z *: f) :> (_ -> _). Proof. -move=> df; set g := RHS; have glin : linear g. +move=> df; set g := RHS. +have glin : linear g. by move=> a u v; rewrite /g linearP /= scalerDl -scalerA. +have gc0 : continuous g. + move=> y. + apply: (@continuous_comp _ _ _ ('d k x) ( *:%R^~ f)); first exact: cts_fun. + exact: scalel_continuous. pose glM := GRing.isLinear.Build _ _ _ _ _ glin. -pose gL : {linear _ -> _} := HB.pack g glM. -by apply:(@diff_unique _ _ _ gL); have [] := dscalel f df. +pose glC := isContinuous.Build _ _ _ gc0. +pose gL : c0linType _ _ := HB.pack g glM glC. +by apply:(@diff_unique _ _ _ gL); have := dscalel f df. Qed. Lemma differentiableZl (k : V -> R) (f : W) x : differentiable k x -> differentiable (fun z => k z *: f) x. Proof. -by move=> df; apply/diff_locallyP; rewrite diffZl //; have [] := dscalel f df. +by move=> df; apply/diff_locallyP; rewrite diffZl //; have := dscalel f df. Qed. -Lemma diff_lin (V' W' : normedModType R) (f : {linear V' -> W'}) x : - continuous f -> 'd f x = f :> (V' -> W'). -Proof. by move=> fcont; apply/diff_unique => //; apply: dlin. Qed. +Lemma diff_lin (V' W' : normedModType R) (f : c0linType V' W') x : + 'd f x = f :> (V' -> W'). +Proof. by apply/diff_unique => //; apply: dlin. Qed. -Lemma linear_differentiable (V' W' : normedModType R) (f : {linear V' -> W'}) - x : continuous f -> differentiable f x. +Lemma linear_differentiable (V' W' : normedModType R) (f : c0linType V' W') x : + differentiable f x. Proof. -by move=> fcont; apply/diff_locallyP; rewrite diff_lin //; have := dlin x fcont. +by apply/diff_locallyP; rewrite diff_lin //; have := dlin f x. Qed. Global Instance is_diff_id (x : V) : is_diff x id id. @@ -670,8 +667,10 @@ Qed. Global Instance is_diff_scaler (k : R) (x : V) : is_diff x ( *:%R k) ( *:%R k). Proof. -apply: DiffDef; first exact/linear_differentiable/scaler_continuous. -by rewrite diff_lin //; apply: scaler_continuous. +have sc := isContinuous.Build _ _ _ (@scaler_continuous _ V k). +set slc : c0linType V V := HB.pack ( *:%R k) sc. +apply: DiffDef; first exact: (linear_differentiable slc). +by rewrite (diff_lin slc). Qed. Global Instance is_diff_scalel (k : R) (x : V) : @@ -680,25 +679,30 @@ Proof. have sx_lin : linear ( *:%R ^~ x : R -> _). by move=> u y z; rewrite scalerDl scalerA. pose sxlM := GRing.isLinear.Build _ _ _ _ _ sx_lin. -pose sxL : {linear _ -> _} := HB.pack ( *:%R ^~ x) sxlM. +have sxc0 : continuous ( *:%R ^~ x : R -> _) by exact: scalel_continuous. +pose sxc := isContinuous.Build _ _ _ sxc0. +pose sxL : c0linType _ _ := HB.pack ( *:%R ^~ x) sxlM sxc. have -> : *:%R ^~ x = sxL by rewrite funeqE. -apply: DiffDef; first exact/linear_differentiable/scalel_continuous. -by rewrite diff_lin //; apply: scalel_continuous. +apply: DiffDef; first exact: linear_differentiable. +by rewrite diff_lin. Qed. Lemma differentiable_coord m n (M : 'M[R]_(m.+1, n.+1)) i j : differentiable (fun N : 'M[R]_(m.+1, n.+1) => N i j : R ) M. Proof. -have @f : {linear 'M[R]_(m.+1, n.+1) -> R}. - by exists (fun N : 'M[R]_(_, _) => N i j); do 2![eexists]; do ?[constructor]; - rewrite ?mxE// => ? *; rewrite ?mxE//; move=> ?; rewrite !mxE. -rewrite (_ : (fun _ => _) = f) //; exact/linear_differentiable/coord_continuous. +have fM : linear (fun N : 'M[R]_(_, _) => N i j) by move=> ? ? ?; rewrite !mxE. +pose flin := GRing.isLinear.Build _ _ _ _ _ fM. +have fc0 : continuous (fun N : 'M[R]_(_, _) => N i j). + exact: coord_continuous. +pose fc := isContinuous.Build _ _ _ fc0. +exact: (linear_differentiable (HB.pack (fun N : 'M[R]_(_, _) => N i j) flin fc)). Qed. -Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : - continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. +Lemma linear_lipschitz (V' W' : normedModType R) (f : c0linType V' W') : + exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. Proof. -move=> /(_ 0); rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)). +move: (@cts_fun _ _ f) => /(_ 0). +rewrite /continuous_at linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. have [|xn0] := real_le0P (normr_real x). by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0. @@ -714,44 +718,43 @@ rewrite normfV ger0_norm /k // invfM/= -mulrA mulVf ?gt_eqF//. by rewrite mulr1 invf_div gtr_pMr// invf_lt1// ltr1n. Qed. -Lemma linear_eqO (V' W' : normedModType R) (f : {linear V' -> W'}) : - continuous f -> (f : V' -> W') =O_ 0 id. +Lemma linear_eqO (V' W' : normedModType R) (f : c0linType V' W') : + (f : V' -> W') =O_ 0 id. Proof. -move=> /linear_lipschitz [k kgt0 flip]; apply/eqO_exP; exists k => //. +case: (linear_lipschitz f) => k kgt0 flip; apply/eqO_exP; exists k => //. exact: filterE. Qed. Lemma diff_eqO (V' W' : normedModType R) (x : filter_on V') (f : V' -> W') : - differentiable f x -> ('d f x : V' -> W') =O_ 0 id. -Proof. by move=> /diff_continuous /linear_eqO; apply. Qed. + ('d f x : V' -> W') =O_ 0 id. +Proof. exact: linear_eqO. Qed. Lemma compOo_eqox (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : [O_ 0 id of g] ([o_ 0 id of f] x) =o_(x \near 0) x. Proof. by rewrite -[LHS]/((_ \o _) x) compOo_eqo. Qed. Fact dcomp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : - differentiable f x -> differentiable g (f x) -> - continuous ('d g (f x) \o 'd f x) /\ forall y, + differentiable f x -> differentiable g (f x) -> forall y, g (f (y + x)) = g (f x) + ('d g (f x) \o 'd f x) y +o_(y \near 0) y. Proof. -move=> df dg; split; first by move=> ?; apply: continuous_comp. +move=> df dg. apply: eqaddoEx => y; rewrite diff_locallyx// -addrA diff_locallyxC// linearD. rewrite addrA -[LHS]addrA; congr (_ + _ + _). -rewrite diff_eqO // ['d f x : _ -> _]diff_eqO //. +rewrite [X in X _ + _]diff_eqO ['d f x : _ -> _]diff_eqO //. by rewrite {2}eqoO addOx compOo_eqox compoO_eqox addox. Qed. Lemma diff_comp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : differentiable f x -> differentiable g (f x) -> 'd (g \o f) x = 'd g (f x) \o 'd f x :> (U -> W'). -Proof. by move=> df dg; apply/diff_unique; have [? /funext] := dcomp df dg. Qed. +Proof. by move=> df dg; apply/diff_unique; have /funext := dcomp df dg. Qed. Lemma differentiable_comp (U V' W' : normedModType R) (f : U -> V') (g : V' -> W') x : differentiable f x -> differentiable g (f x) -> differentiable (g \o f) x. Proof. -move=> df dg; apply/diff_locallyP; rewrite diff_comp //; -by have [? /funext]:= dcomp df dg. +move=> df dg; apply/diff_locallyP; rewrite diff_comp //. +by have /funext := dcomp df dg. Qed. Global Instance is_diff_comp (U V' W' : normedModType R) (f df : U -> V') @@ -824,20 +827,22 @@ Lemma diff_bilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> 'd (fun q => f q.1 q.2) p = (fun q => f p.1 q.2 + f q.1 p.2) :> (U * V' -> W'). Proof. -pose d q := f p.1 q.2 + f q.1 p.2. -move=> fc; have lind : linear d. +pose d q := f p.1 q.2 + f q.1 p.2 => fc. +have lind : linear d. by move=> ? ? ?; rewrite /d linearPr linearPl scalerDr addrACA. pose dlM := GRing.isLinear.Build _ _ _ _ _ lind. -pose dL : {linear _ -> _} := HB.pack d dlM. -rewrite -/d -[d]/(dL : _ -> _). -by apply/diff_unique; have [] := dbilin p fc. +have [lc0 ld] := dbilin p fc. +pose dlC := isContinuous.Build _ _ _ lc0. +pose dL : c0linType _ _ := HB.pack d dlM dlC. +by rewrite -/d -[d]/(dL : _ -> _); apply: diff_unique. Qed. Lemma differentiable_bilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p : continuous (fun p => f p.1 p.2) -> differentiable (fun p => f p.1 p.2) p. Proof. -by move=> fc; apply/diff_locallyP; rewrite diff_bilin //; apply: dbilin p fc. +move=> fc; apply/diff_locallyP; rewrite diff_bilin //. +by have [_] := dbilin p fc. Qed. Lemma mulr_is_bilinear : @@ -892,16 +897,18 @@ move=> df dg. pose d y := ('d f x y, 'd g x y). have lin_pair : linear d by move=> ???; rewrite /d !linearPZ. pose pairlM := GRing.isLinear.Build _ _ _ _ _ lin_pair. -pose pairL : {linear _ -> _} := HB.pack d pairlM. -rewrite -/d -[d]/(pairL : _ -> _). -by apply: diff_unique; have [] := dpair df dg. +have [pairC0 paird] := dpair df dg. +pose pairC := isContinuous.Build _ _ _ pairC0. +pose pairL : c0linType _ _ := HB.pack d pairlM pairC. +by rewrite -/d -[d]/(pairL : _ -> _); apply: diff_unique. Qed. Lemma differentiable_pair (U V' W' : normedModType R) (f : U -> V') (g : U -> W') x : differentiable f x -> differentiable g x -> differentiable (fun y => (f y, g y)) x. Proof. -by move=> df dg; apply/diff_locallyP; rewrite diff_pair //; apply: dpair. +move=> df dg; apply/diff_locallyP; rewrite diff_pair //. +by have [_] := dpair df dg. Qed. Global Instance is_diff_pair (U V' W' : normedModType R) (f df : U -> V') @@ -983,16 +990,24 @@ by rewrite normrM normfV (@ger0_norm _ 2) // addrK; apply/ltW. Unshelve. all: by end_near. Qed. Lemma diff_Rinv (x : R) : x != 0 -> - 'd GRing.inv x = (fun h : R => - x ^- 2 *: h) :> (R -> R). + 'd GRing.inv x = ( *:%R (- x ^- 2)) :> (R -> R). Proof. -move=> xn0; have -> : (fun h : R => - x ^- 2 *: h) = ( *:%R (- x ^- 2)) by []. -by apply: diff_unique; have [] := dinv xn0. +move=> xn0. +pose f := ( *:%R (- x ^- 2) : R -> R). +have fM : linear f. + by move=> ? ? ?; rewrite /f scalerDr scalerA mulrC -scalerA. +pose fl := GRing.isLinear.Build _ _ _ _ _ fM. +have [fc0] := dinv xn0. +pose fc := isContinuous.Build _ _ _ fc0. +set g : c0linType _ _ := HB.pack f fl fc. +exact: (@diff_unique _ _ _ g). Qed. Lemma differentiable_Rinv (x : R) : x != 0 -> differentiable (GRing.inv : R -> R) x. Proof. -by move=> xn0; apply/diff_locallyP; rewrite diff_Rinv //; apply: dinv. +move=> xn0; apply/diff_locallyP; rewrite diff_Rinv //. +by have [_] := dinv xn0. Qed. Lemma diffV (f : V -> R) x : differentiable f x -> f x != 0 -> @@ -1043,23 +1058,26 @@ Qed. Lemma deriv1E f x : derivable f x 1 -> 'd f x = ( *:%R^~ (f^`() x)) :> (R -> U). Proof. -pose d (h : R) := h *: (f^`() x)%classic. -move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. +pose d (h : R) := h *: (f^`() x)%classic => df. +have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. -pose scalL : {linear _ -> _} := HB.pack d scallM. -rewrite -/d -[d]/(scalL : _ -> _). -by apply: diff_unique; [apply: scalel_continuous|apply: der1]. +have scallC0 : continuous d by apply: scalel_continuous. +pose scallC := isContinuous.Build _ _ _ scallC0. +pose scalL : c0linType _ _ := HB.pack d scallM scallC. +by rewrite -/d -[d]/(scalL : _ -> _); apply/diff_unique/der1. Qed. Lemma diff1E f x : - differentiable f x -> 'd f x = (fun h => h *: f^`()%classic x) :> (R -> U). + differentiable f x -> 'd f x = ( *:%R^~ (f^`()%classic x)) :> (R -> U). Proof. -pose d (h : R) := h *: 'd f x 1. -move=> df; have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. +pose d (h : R) := h *: 'd f x 1 => df. +have lin_scal : linear d by move=> ? ? ?; rewrite /d scalerDl scalerA. pose scallM := GRing.isLinear.Build _ _ _ _ _ lin_scal. -pose scalL : {linear _ -> _} := HB.pack d scallM. -have -> : (fun h => h *: f^`()%classic x) = scalL by rewrite derive1E'. -apply: diff_unique; first exact: scalel_continuous. +have scallC0 : continuous d by apply: scalel_continuous. +pose scallC := isContinuous.Build _ _ _ scallC0. +pose scalL : c0linType _ _ := HB.pack d scallM scallC. +have -> : ( *:%R^~ (f^`()%classic x)) = scalL by rewrite derive1E'. +apply: diff_unique. apply/eqaddoE; have /diff_locally -> := df; congr (_ + _ + _). by rewrite funeqE => h /=; rewrite -{1}[h]mulr1 linearZ. Qed. @@ -1067,8 +1085,7 @@ Qed. Lemma derivable1_diffP f x : derivable f x 1 <-> differentiable f x. Proof. split=> dfx. - by apply/diff_locallyP; rewrite deriv1E //; split; - [apply: scalel_continuous|apply: der1]. + by apply/diff_locallyP; rewrite deriv1E //; apply: der1. apply/derivable_nbhsP/eqaddoE. have -> : (fun h => (f \o shift x) h%:A) = f \o shift x. by rewrite funeqE=> ?; rewrite [_%:A]mulr1. @@ -1255,8 +1272,7 @@ Proof. exact/diff_derivable. Qed. Global Instance is_derive_id (x v : V) : is_derive x v id v. Proof. apply: (DeriveDef (@derivable_id _ _)). -rewrite deriveE// (@diff_lin _ _ _ idfun)//=. -by rewrite /continuous_at. +by rewrite deriveE// (@diff_lin _ _ _ idfun). Qed. Global Instance is_deriveNid (x v : V) : is_derive x v -%R (- v). diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index 20cf27a6e3..dd758a1e74 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -241,5 +241,6 @@ Qed. HB.instance Definition _ := PseudoMetricNormedZmod_Lmodule_isNormedModule.Build K 'M[K]_(m.+1, n.+1) mx_normZ. +HB.instance Definition _ := Equality.on 'M[K]_(m.+1, n.+1). End matrix_NormedModule. diff --git a/theories/tvs.v b/theories/tvs.v index 193659a0b9..80f3087022 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -732,6 +732,7 @@ HB.instance Definition _ := TopologicalNmodule_isTopologicalLmodule.Build K (E * F)%type prod_scale_continuous. HB.instance Definition _ := Uniform_isTvs.Build K (E * F)%type prod_locally_convex. +HB.instance Definition _ := Choice.on (E * F)%type. End prod_Tvs. @@ -820,4 +821,6 @@ Qed. HB.instance Definition _ := GRing.SubChoice_isSubLmodule.Build K (continuousType M N) _ (c0linType M N) submod_closed. +HB.instance Definition _ := isPointed.Build (c0linType M N) 0. + End ContinuousLinear_sub_Continuous. From 5201b010b5f415ceaed9b371325163c7378eaf95 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 13 Nov 2025 11:13:43 +0100 Subject: [PATCH 4/9] wip derive.v ++ start tensor.v --- .nix/config.nix | 2 +- classical/tensor.v | 253 +++++++++++++++++++++ theories/derive.v | 250 +++++++++++++++++++- theories/normedtype_theory/normed_module.v | 10 + 4 files changed, 513 insertions(+), 2 deletions(-) create mode 100644 classical/tensor.v diff --git a/.nix/config.nix b/.nix/config.nix index 2b6bf88ff2..7048627f10 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -45,7 +45,7 @@ in { ## select an entry to build in the following `bundles` set ## defaults to "default" - default-bundle = "9.0"; + default-bundle = "9.1"; ## write one `bundles.name` attribute set per ## alternative configuration diff --git a/classical/tensor.v b/classical/tensor.v new file mode 100644 index 0000000000..3581d7eb90 --- /dev/null +++ b/classical/tensor.v @@ -0,0 +1,253 @@ +From HB Require Import structures. +From mathcomp Require Import all_ssreflect ssralg vector ring_quotient finmap boolp. + +Import GRing.Theory. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +(** Free module *) + +Section FreeLmod. +Variables (R : pzRingType) (T : choiceType). + +Definition free_lmod := {fsfun T -> R with 0}. + +HB.instance Definition _ := Choice.on free_lmod. + +Fact free_lmod_key : unit. Proof. exact: tt. Qed. + +Let zero : free_lmod := fsfun_of_fun free_lmod_key fset0 (fun=> 0) (fun=> 0). + +Let zeroE x : zero x = 0. +Proof. by rewrite fsfunE in_fset0. Qed. + +Let opp (f : free_lmod) := fsfun_of_fun free_lmod_key (finsupp f) (GRing.opp \o f) (fun=> 0). + +Let oppE (f : free_lmod) x : opp f x = - (f x). +Proof. +rewrite fsfunE mem_finsupp; case: ifPn => //; rewrite negbK => /eqP ->. +by rewrite oppr0. +Qed. + +Let add (f g : free_lmod) := fsfun_of_fun free_lmod_key (finsupp f `|` finsupp g)%fset (f \+ g) (fun=> 0). + +Let addE (f g : free_lmod) x : add f g x = f x + g x. +Proof. +rewrite fsfunE in_fsetU !mem_finsupp. +case: ifPn => //; rewrite negb_or !negbK => /andP[] /eqP -> /eqP ->. +by rewrite addr0. +Qed. + +Let addrA : associative add. +Proof. by move=> f g h; apply/fsfunP => x; rewrite !addE addrA. Qed. + +Let addrC : commutative add. +Proof. by move=> f g; apply/fsfunP => x; rewrite !addE addrC. Qed. + +Let add0r : left_id zero add. +Proof. by move=> f; apply/fsfunP => x; rewrite addE zeroE add0r. Qed. + +Let addNr : left_inverse zero opp add. +Proof. by move=> f; apply/fsfunP => x; rewrite addE oppE addNr. Qed. + +HB.instance Definition _ := + GRing.isZmodule.Build free_lmod addrA addrC add0r addNr. + +Let scale (a : R) (f : free_lmod) : free_lmod := + fsfun_of_fun free_lmod_key (finsupp f)%fset (fun x => a * f x) (fun=> 0). + +Let scaleE a f x : scale a f x = a * f x. +Proof. +rewrite fsfunE mem_finsupp. +by case: ifPn => //; rewrite negbK => /eqP ->; rewrite mulr0. +Qed. + +Let scalerA a b f : scale a (scale b f) = scale (a * b) f. +Proof. by apply/fsfunP => x; rewrite !scaleE mulrA. Qed. + +Let scale1r : left_id 1 scale. +Proof. by move=> f; apply/fsfunP => x; rewrite !scaleE mul1r. Qed. + +Let scalerDr : right_distributive scale +%R. +Proof. +by move=> a f g; apply/fsfunP => x; rewrite addE !scaleE addE mulrDr. +Qed. + +Let scalerDl f : {morph scale^~ f: a b / a + b}. +Proof. by move=> a b; apply/fsfunP => x; rewrite addE !scaleE mulrDl. Qed. + +HB.instance Definition _ := + GRing.Zmodule_isLmodule.Build R free_lmod scalerA scale1r scalerDr scalerDl. + +Lemma free_lmod0E : (0 : free_lmod) = (fun=> 0) :> (_ -> _). +Proof. exact/funext/zeroE. Qed. + +Lemma free_lmodNE (f : free_lmod) : - f = \- f :> (_ -> _). +Proof. exact/funext/oppE. Qed. + +Lemma free_lmodDE (f g : free_lmod) : f + g = f \+ g :> (_ -> _). +Proof. exact/funext/addE. Qed. + +Lemma free_lmodZE a (f : free_lmod) : a *: f = (fun x => a * f x) :> (_ -> _). +Proof. exact/funext/scaleE. Qed. + +End FreeLmod. + +HB.mixin Record ZmodQuotient_isLmodQuotient (R : pzRingType) T eqT + (zeroT : T) (oppT : T -> T) (addT : T -> T -> T) (scaleT : R -> T -> T) + (Q : Type) of ZmodQuotient T eqT zeroT oppT addT Q & GRing.Lmodule R Q := { + pi_scaler : forall a, {morph \pi_Q : x / scaleT a x >-> a *: x} +}. + +#[short(type="lmodQuotType")] +HB.structure Definition LmodQuotient R T eqT zeroT oppT addT scaleT := + {Q of ZmodQuotient_isLmodQuotient R T eqT zeroT oppT addT scaleT Q & + ZmodQuotient T eqT zeroT oppT addT Q & GRing.Lmodule R Q }. + +Section LModQuotient. + +Variable (R : pzRingType) (T : Type). +Variable eqT : rel T. +Variables (zeroT : T) (oppT : T -> T) (addT : T -> T -> T) (scaleT : R -> T -> T). +Implicit Type zqT : LmodQuotient.type eqT zeroT oppT addT scaleT. + +Canonical pi_scale_quot_morph zqT a := PiMorph1 (@pi_scaler _ _ _ _ _ _ _ zqT a). + +End LModQuotient. + +Section PiLinear. + +Variables (R : pzRingType) (L : lmodType R) (equivL : rel L) (zeroL : L). +Variable Q : @lmodQuotType R L equivL zeroL -%R +%R *:%R. + +Lemma pi_is_linear : linear \pi_Q. +Proof. by move=> a x y /=; rewrite !piE. Qed. + +HB.instance Definition _ := GRing.isLinear.Build R L Q _ \pi_Q pi_is_linear. + +End PiLinear. + +(* TODO: backport *) +HB.factory Record SubmodClosed_isZmodClosed + (R : pzRingType) (L : lmodType R) (P : {pred L}) of GRing.SubmodClosed R P := + {}. + +HB.builders Context R L P of SubmodClosed_isZmodClosed R L P. +Lemma submodClosedB : oppr_closed P. +Proof. by move=> x xP; rewrite -scaleN1r; apply: rpredZ. Qed. + +HB.instance Definition _ := GRing.isOppClosed.Build L P submodClosedB. +HB.end. + +Module Quotient. +Export Quotient. +Section LmodQuotient. +Variables (R : pzRingType) (L : lmodType R) (P : submodClosed L). + +Definition Pzmod : {pred _} := P. +HB.instance Definition _ := GRing.SubmodClosed.on Pzmod. +HB.instance Definition _ := @SubmodClosed_isZmodClosed.Build R L Pzmod. + +Notation quot := (quot Pzmod). + +Definition scale a := lift_op1 quot ( *:%R a). + +Lemma pi_scale a : {morph \pi : x / a *: x >-> scale a x}. +Proof. +move=> x; unlock scale; apply/eqP; rewrite piE equivE. +by rewrite -scalerBr rpredZ// idealrBE reprK. +Qed. + +Canonical pi_scale_morph a := PiMorph1 (pi_scale a). + +Let scalerA a b f : scale a (scale b f) = scale (a * b) f. +Proof. by rewrite -[f]reprK !piE scalerA. Qed. + +Let scale1r : left_id 1 scale. +Proof. by move=> f; rewrite -[f]reprK !piE scale1r. Qed. + +Let scalerDr : right_distributive scale +%R. +Proof. by move=> a f g; rewrite -[f]reprK -[g]reprK !piE scalerDr. Qed. + +Let scalerDl f : {morph scale^~ f: a b / a + b}. +Proof. by move=> a b; rewrite -[f]reprK !piE scalerDl. Qed. + +#[export] +HB.instance Definition _ := + GRing.Zmodule_isLmodule.Build R quot scalerA scale1r scalerDr scalerDl. +#[export] +HB.instance Definition _ := + ZmodQuotient_isLmodQuotient.Build R L (equiv Pzmod) 0 -%R +%R *:%R quot pi_scale. + +End LmodQuotient. +Module Exports. HB.reexport. End Exports. +End Quotient. + +Export Quotient.Exports. + + +Module Tensor. +Section fintensor. +Variables (R : fieldType) (U V : vectType R). + +Let nU := \dim (@fullv _ U). +Let nV := \dim (@fullv _ V). +Let bU := vbasis (@fullv _ U). +Let bV := vbasis (@fullv _ V). + +Definition fintensor := free_lmod R ('I_nU * 'I_nV)%type. + +Definition fintensor_proj (x : U * V) : fintensor := + fsfun_of_fun free_lmod_key (unpickle setT) (fun i => coord bU i.1 x.1 * coord bV i.2 x.2) (fun=> 0). + +End fintensor. + +Section span. +Variables (R : fieldType) (U : lmodType R) (X : {fset U}). + +Definition of_span_subdef (x : free_lmod R X) := + \sum_(i <- finsupp x) x i *: val i. + +Lemma of_span_subdef_linear : linear of_span_subdef. +Proof. +move=> a x y; rewrite /of_span_subdef scaler_sumr. +rewrite (big_fset_incl _ (fsubsetUr (finsupp x `|` finsupp y)%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. +apply: esym; rewrite (big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp y))%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r scaler0. +rewrite [X in _ + X](big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp x))%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. +rewrite fsetUAC -big_split/= -fsetUA fsetUC. +by apply: eq_bigr => i _; rewrite free_lmodDE/= scalerDl free_lmodZE scalerA. +Qed. + +HB.instance Definition _ := GRing.isLinear.Build _ _ _ _ of_span_subdef of_span_subdef_linear. + +Definition spanI0 (x : free_lmod R X) := of_span_subdef x == 0. + +Lemma spanI0_submod_closed : submod_closed spanI0. +Proof. +split=> [|a x y]; rewrite !unfold_in; first by rewrite linear0. +by rewrite linearPZ/= => /eqP -> /eqP ->; rewrite scaler0 addr0. +Qed. + +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ spanI0 spanI0_submod_closed. + +(* TODO: Why does the reverse coercion fail to apply? *) +Definition span := Quotient.quot Tensor_spanI0__canonical__GRing_SubmodClosed. + +Check span : zmodType . + +End span. + +Section tensor. +Variables (R : fieldType) (U V : lmodType R). + +Definition equiv (x y : free_lmod R (U * V)%type) := true. +End tensor. +End Tensor. diff --git a/theories/derive.v b/theories/derive.v index bee1c43882..be4347cb75 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly. From mathcomp Require Import sesquilinear. From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. From mathcomp Require Import functions reals interval_inference topology. -From mathcomp Require Import prodnormedzmodule tvs normedtype landau. +From mathcomp Require Import prodnormedzmodule tvs normedtype landau ereal. (**md**************************************************************************) (* # Differentiation *) @@ -2141,3 +2141,251 @@ exact/derivable1_diffP/derivable_horner. Qed. End derive_horner. + +Lemma deriveE1 (R : numFieldType) (V W : normedModType R) (f : V -> W) (x v : V) : + 'D_v f x = (fun h => f (h *: v + x))^`() 0. +Proof. +rewrite /derive /derive1/=; apply: esym. +by under [X in fmap X]funext do rewrite addr0 scale0r add0r. +Qed. + +Lemma is_derive_comp (R : numFieldType) (U V W : normedModType R) (f : V -> W) + (g : U -> V) (x u : U) (v : V) (w : W) : + differentiable f (g x) -> is_derive x u g v -> + is_derive x u (f \o g) ('d f (g x) v). +Proof. +move=> fgx gx. +have gx0: differentiable (fun h : R^o => g (h *: u + x)%E) 0. + exact/derivable1_diffP/(derivable1P _ _ u). +have fgx1: differentiable (fun h : R => (f \o g) (h *: u + x)%E) 0. + apply: (@differentiable_comp _ _ _ _ (fun h : R^o => g (h *: u + x)) f) => //. + by rewrite scale0r add0r. +apply: DeriveDef; first exact/derivable1P/diff_derivable. +rewrite deriveE1 derive1E'//. +rewrite (@diff_comp _ _ _ _ _ f)//; last by rewrite scale0r add0r/=. +by rewrite scale0r add0r/= -derive1E'// -deriveE1 derive_val. +Qed. +(* +Section MVI. + (* TODO: backport convex types *) +Theorem MVI (R : realType) (U V : normedModType R) (f : U -> V) (a b : U) : + (forall t : R, t \in `[0, 1]%R -> differentiable f (t *: a + (1 - t) *: b)) -> + (`|f b - f a|%:E <= ereal_sup [set `|'d f (t *: a + (1 - t) *: b)%R|%:E | t in `[0%R, 1%R]] * `|b - a|%:E)%E. +Proof. +have [-> _|ab] := eqVneq a b; first by rewrite !subrr !normr0 mule0. +suff: forall g : R -> V, (forall t, t \in `[0, 1]%R -> derivable g t 1) -> + (`|g 1 - g 0|%:E <= ereal_sup [set `|derive1 g t|%:E | t in `[0%R, 1%R]])%E. + pose g t := (t *: a + (1 - t) *: b). + move=> + fdiff. + have fgd (t : R) : t \in `[0, 1]%R -> is_derive t 1 (f \o g) ('d f (g t) (derive1 g t)). + move=> /fdiff ft. + apply: is_derive_comp. + Search is_derive . + + move=> t01; apply: differentiable_comp; last exact: fdiff. + by apply: differentiableD; apply: differentiableZl. + move=> /(_ (f \o g) _)/wrap[t /fgd/diff_derivable //|]. + rewrite /g/= subr0 subrr !scale1r !scale0r add0r addr0 -normrN opprB. + move=> /le_trans; apply; apply/ereal_supP => _/= [] t t01 <-. + have ab0: (0 < `|b - a|) by rewrite normr_gt0 subr_eq0 eq_sym. + rewrite -lee_pdivrMr//; apply: ereal_sup_ge. + exists (`|'d f ((t *: a + (1 - t) *: b)%E)|%:E); first by exists t. + rewrite lee_pdivrMr// derive1E'; last exact: fgd. + rewrite diff_comp. + + Search diff derive1. + Search (_ <= ereal_sup _ )%E. + Search (_ <= sup _ ). + apply: sup_le_ub. + + Search GRing.scale (differentiable _ _). + /wrap. +under [X in X @` _]funext => t. rewrite -/(g t). over. +have <- : g 0 = b by rewrite /g scale0r add0r subr0 scale1r. +have <- : g 1 = a by rewrite /g scale1r subrr scale0r addr0. +rewrite (@MVT R (f \o g) (fun t => d f (g t) (b - a))). +Search "MVT". +End MVI. + *) +Section ndiff. +Variables (R : realType) (U : normedModType R). +(* TODO: decide notations*) + +Fixpoint nlin (V : normedModType R) n := + match n with + | 0 => V + | n.+1 => c0linType U (nlin V n) + end. + +Definition ndiff (V : normedModType R) n (f : U -> V) : U -> nlin V n := + (fix F V f n := + match n as m return (forall (V : normedModType R), (U -> V) -> (U -> nlin V m)) with + | 0 => fun V f => f + | n.+1 => fun V f => F (c0linType U V) (fun x => 'd f x) n + end) V f. + +Definition ndifferentiable n := forall k, (k < n)%N -> forall x, differentiable (ndiff k) x. +Definition ncontinuous n := ndifferentiable n /\ continuous (ndiff n). + +Definition smooth := forall k x, differentiable (ndiff k) x. + +Lemma ndiff0 : ndiff 0 = f. Proof. by []. Qed. +Lemma ndiff1 : ndiff 1 = fun x => 'd f x. Proof. by []. Qed. +Lemma ndiffS n : ndiff n.+1 = fun x => 'd (ndiff n) x. Proof. by []. Qed. + +Lemma ndifferentiableW n m : (n <= m)%N -> ndifferentiable m -> ndifferentiable n. +Proof. by move=> nm d k /leq_trans/(_ nm) /d. Qed. + +Lemma ncontinuousW n m : (n <= m)%N -> ncontinuous m -> ncontinuous n. +Proof. +move=> nm [] d c. +split; first exact: (ndifferentiableW nm). +move: nm; rewrite leq_eqVlt => /orP[/eqP -> //|] /d dd x. +exact: differentiable_continuous. +Qed. + +Lemma ndifferentiable_smooth n : smooth -> ndifferentiable n. +Proof. by move=> s k _. Qed. + +Lemma ncontinuous_smooth n : smooth -> ncontinuous n. +Proof. +move=> s; split=> [|x]; first exact: ndifferentiable_smooth. +exact/differentiable_continuous/ndifferentiable_smooth. +Qed. + +Lemma eqo_c0lin (V' W : normedModType R) (F : filter_on U) (g : U -> c0linType V' W) (v : V') : + (fun t : U => [o_F id of g] t v) =o_F id. +Proof. +apply/eqoP => _/posnumP[e]. +case: (ltP 0 `|v|) => [v0|]; last first. + rewrite normr_le0 => /eqP ->. + by near=> x; rewrite linear0 normr0. +near=> x. +apply: (le_trans (norm_c0lin_le _ _)). +rewrite -ler_pdivlMr// mulrAC. +by near: x; apply: littleoP; apply: divr_gt0. +Unshelve. all: end_near. +Qed. + +Fact dderive (u x : U) : ndifferentiable 2 -> + continuous (fun h : U => 'D_h (fun x => 'd f x) x u) /\ ('D_u f) \o shift x = cst ('D_u f x) + (fun h : U => 'D_h (fun x => 'd f x) x u) +o_ 0 id. +Proof. +move=> /[dup] /(_ 0 erefl) fd /(_ 1 erefl) dfd. +split=> [h|]. + under [X in _ _ X]funext do rewrite deriveE//. + (* TODO: Why does this fail? + rewrite -[forall t, _]/(@continuous_at _ _). *) + set g := 'd _ x. + case: (ltP 0 `|u|) => [u0|]; last first. + rewrite normr_le0 => /eqP ->. + rewrite linear0. + under [X in fmap X]funext do rewrite linear0. + exact: cvg_cst. + case: (ltP 0 `|g|) => [g0|]; last first. + rewrite normr_le0 => /eqP ->; apply: cvg_cst. + apply/cvg_ballP => e e0. + near=> b; rewrite -ball_normE/=. + apply: (le_lt_trans (norm_c0lin_le (g h - g b) u)). + rewrite -ltr_pdivlMr// -raddfB. + apply: (le_lt_trans (norm_c0lin_le g _)). + rewrite -ltr_pdivlMl//. + suff: ball h (`|g|^-1 * (e / `|u|)) b by rewrite -ball_normE. + near: b; apply: near_ball. + rewrite mulrC !divr_gt0//. +apply/eqaddoE; rewrite funeqE => h /=. +rewrite !addrfctE !deriveE//. +move: dfd; rewrite /ndiff/= => /(_ x)/diff_locallyx/(_ h) ->. +rewrite /= /cst/=; congr (_ + _ + _). +rewrite -[LHS]/((fun t : U => (ContinuousLinear.sort (the_littleo _ _ _ _ _ t)) u) h). +by rewrite eqo_c0lin. +Unshelve. all: end_near. +Qed. + +Lemma diff_derive u x : ndifferentiable 2 -> + 'd ('D_u f) x = (fun h : U => 'D_h (fun x => 'd f x) x u) :> (U -> V). +Proof. +move=> /[dup] df2 /(_ 1 erefl) dfd. +pose d h := ('D_h (fun x0 : U => 'd f x0) x) u. +have lind : linear d by move=> ???; rewrite /d !deriveE// linearPZ. +pose dlM := GRing.isLinear.Build _ _ _ _ _ lind. +have [dC0 dd] := dderive u x df2. +pose dC := isContinuous.Build _ _ _ dC0. +pose dL : c0linType _ _ := HB.pack d dlM dC. +by rewrite -/d -[d]/(dL : _ -> _); apply: diff_unique. +Qed. + +Lemma differentiable_derive u x : ndifferentiable 2 -> + differentiable ('D_u f) x. +Proof. +move=> df2; apply/diff_locallyP; rewrite diff_derive//. +by have [_] := dderive u x df2. +Qed. + +Global Instance is_diff_derive (u x : U) : ndifferentiable 2 -> is_diff x ('D_u f) (fun h : U => ('D_h (fun x0 : U => 'd f x0) x) u). +Proof. +move=> df2; apply: DiffDef; first exact: differentiable_derive. +by rewrite diff_derive. +Qed. + +End ndiff. + +Lemma ndiffSn [R : realType] [U V : normedModType R] (f : U -> V) (n : nat) : + ndiff f n.+1 = ndiff (fun x => 'd f x) n. + +Lemma ndifferentiable_derive [R : realType] [U V : normedModType R] (f : U -> V)(u : U) (n : nat) : ndifferentiable f n.+1 -> + ndifferentiable ('D_u f) n. +Proof. +elim: n f => // n IHn f. + +(* With this definition of `ndiff` this lemma is very ugly and probably unusable, + things will be better when we have tensor products. *) +Lemma derive1nE [R : realType] [V : normedModType R] (f : R -> V) (n : nat) : + f^`(n) = (fix F n : nlin R V n -> V := + match n as m return nlin R V m -> V with + | 0 => id + | n.+1 => fun f : nlin R V n.+1 => F n (f 1%R : nlin R V n) + end) n \o (ndiff f n). +Proof. +elim: n f => // n IHn f. +rewrite derive1Sn/=. +IHn. + +Lemma ncontinuous1_derivP : + ncontinuous 1 <-> forall a, (forall x, derivable f a x) /\ continuous ('D_a f). +Proof. +split=> [[] /(_ 0 erefl) d c a|]. + split=> x; first exact: diff_derivable. + case: (ltP 0 `|a|) => [a0|]; last first. + rewrite normr_le0 => /eqP ->. + suff ->: 'D_0 f = cst 0 by apply: cts_fun. + by apply: funext => y; rewrite deriveE// linear0. + apply/cvg_ballP => e e0. + set e' := e / `|a|. + have e'0 : 0 < e' by apply: divr_gt0. + move: c => /(_ x)/cvg_ballP/(_ e' e'0) c. + near=> y. + rewrite -ball_normE/= deriveE// deriveE//. + have: ball (ndiff 1 x) e' (ndiff 1 y). + near: y; exact: c. + rewrite /ndiff/= -ball_normE/= ltr_pdivlMr//. + by move=> /(le_lt_trans (norm_c0lin_le _ _)). +move=> c. +split. + move=> k; rewrite [(_ < _)%N]leqn0 => /eqP -> {k} x. + Search (differentiable _ _) derivable. + +admit. +Unshelve. all: end_near. + Search (\forall _ \near _, _). + Search cvg_to Order.lt. + Search lipschitz_on . +Check lipschitz_on. _). + + + +Lemma ndifferentiable_deriv n a : ndifferentiable n.+1 -> ndifferentiable n ('D_a f). + + + + +End ndiff. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 2ba27fb01f..58b67d2d19 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2142,4 +2142,14 @@ Qed. HB.instance Definition _ := Lmodule_isNormed.Build R (c0linType M N) ler_normD normrZ normr0_eq0. +Lemma norm_c0lin_le (f : c0linType M N) (x : M) : `|f x| <= `|f| * `|x|. +Proof. +case: (ltP 0 `|x|) => [x0|]; last first. + by rewrite normr_le0 => /eqP ->; rewrite linear0 !normr0 mulr0. +have x0': 0 <= `|x|^-1 by rewrite invr_ge0; apply: ltW. +rewrite -ler_pdivrMr// mulrC -[_^-1]ger0_norm// -normed_module.normrZ -linearZ. +apply: (sup_upper_bound (normP f)); exists (`|x|^-1 *: x) => //=. +by rewrite normed_module.normrZ ger0_norm// mulVf// lt0r_neq0. +Qed. + End LinearContinuous. From 11d0d4740f98cc9c28cdfab44d1cbfa28d5faf8c Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 14 Nov 2025 12:18:30 +0100 Subject: [PATCH 5/9] Small repairs and tentative improvements --- classical/tensor.v | 196 +++++++++++++++++++++++++++++++++------------ 1 file changed, 146 insertions(+), 50 deletions(-) diff --git a/classical/tensor.v b/classical/tensor.v index 3581d7eb90..14fd4b478b 100644 --- a/classical/tensor.v +++ b/classical/tensor.v @@ -1,5 +1,7 @@ From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg vector ring_quotient finmap boolp. +From elpi Require Import elpi. +From mathcomp Require Import all_ssreflect ssralg vector ring_quotient finmap. +From mathcomp Require Import boolp functions classical_sets. Import GRing.Theory. @@ -7,40 +9,48 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Local Open Scope fset_scope. Local Open Scope ring_scope. Local Open Scope quotient_scope. (** Free module *) Section FreeLmod. -Variables (R : pzRingType) (T : choiceType). +Context {R : pzRingType} {T : choiceType}. Definition free_lmod := {fsfun T -> R with 0}. HB.instance Definition _ := Choice.on free_lmod. -Fact free_lmod_key : unit. Proof. exact: tt. Qed. +Section lmodType. -Let zero : free_lmod := fsfun_of_fun free_lmod_key fset0 (fun=> 0) (fun=> 0). +(* This is the unit of the monad *) +Elpi lock Definition free_lmod_unit (x : T) : free_lmod := + [fsfun [fsfun] with x |-> 1]. + +Elpi lock Definition zero_subdef : free_lmod := [fsfun]. +Local Notation zero := zero_subdef. Let zeroE x : zero x = 0. -Proof. by rewrite fsfunE in_fset0. Qed. +Proof. by rewrite [zero]unlock fsfunE. Qed. -Let opp (f : free_lmod) := fsfun_of_fun free_lmod_key (finsupp f) (GRing.opp \o f) (fun=> 0). +Elpi lock Definition opp_subdef (f : free_lmod) : free_lmod := + [fsfun x in finsupp f => - (f x)]. +Local Notation opp := opp_subdef. -Let oppE (f : free_lmod) x : opp f x = - (f x). +Lemma oppE (f : free_lmod) x : opp f x = - (f x). Proof. -rewrite fsfunE mem_finsupp; case: ifPn => //; rewrite negbK => /eqP ->. -by rewrite oppr0. +by rewrite [opp]unlock fsfunE mem_finsupp; case: eqP => //= ->; rewrite oppr0. Qed. -Let add (f g : free_lmod) := fsfun_of_fun free_lmod_key (finsupp f `|` finsupp g)%fset (f \+ g) (fun=> 0). +Elpi lock Definition add_subdef (f g : free_lmod) : free_lmod := + [fsfun x in finsupp f `|` finsupp g => f x + g x]. +Local Notation add := add_subdef. Let addE (f g : free_lmod) x : add f g x = f x + g x. Proof. -rewrite fsfunE in_fsetU !mem_finsupp. -case: ifPn => //; rewrite negb_or !negbK => /andP[] /eqP -> /eqP ->. -by rewrite addr0. +rewrite [add]unlock fsfunE in_fsetU !mem_finsupp. +by do 2!case: eqP => //= ->; rewrite addr0. Qed. Let addrA : associative add. @@ -58,13 +68,14 @@ Proof. by move=> f; apply/fsfunP => x; rewrite addE oppE addNr. Qed. HB.instance Definition _ := GRing.isZmodule.Build free_lmod addrA addrC add0r addNr. -Let scale (a : R) (f : free_lmod) : free_lmod := - fsfun_of_fun free_lmod_key (finsupp f)%fset (fun x => a * f x) (fun=> 0). +Elpi lock Definition scale_subdef (a : R) (f : free_lmod) : free_lmod := + [fsfun x in finsupp f => a * f x]. +Local Notation scale := scale_subdef. Let scaleE a f x : scale a f x = a * f x. Proof. -rewrite fsfunE mem_finsupp. -by case: ifPn => //; rewrite negbK => /eqP ->; rewrite mulr0. +rewrite [scale]unlock fsfunE mem_finsupp. +by case: eqP => //= ->; rewrite mulr0. Qed. Let scalerA a b f : scale a (scale b f) = scale (a * b) f. @@ -93,10 +104,81 @@ Proof. exact/funext/oppE. Qed. Lemma free_lmodDE (f g : free_lmod) : f + g = f \+ g :> (_ -> _). Proof. exact/funext/addE. Qed. +Lemma free_lmod_sumE I r P (F : I -> free_lmod) : + \sum_(i <- r | P i) F i = (fun x => \sum_(i <- r | P i) F i x) :> (_ -> _). +Proof. +apply/funext => t; elim/big_ind2: _ => //= x u y v. +by rewrite free_lmodDE/= => -> ->. +Qed. + Lemma free_lmodZE a (f : free_lmod) : a *: f = (fun x => a * f x) :> (_ -> _). Proof. exact/funext/scaleE. Qed. +Lemma free_lmod_unitE t t' : free_lmod_unit t t' = (t == t')%:R. +Proof. +by rewrite [free_lmod_unit]unlock fsfunE/= !inE/= orbF; case: eqVneq. +Qed. + +End lmodType. + +Section eval. +Context {U : lmodType R} (f : T -> U). + +Elpi lock Definition free_lmod_eval (x : free_lmod) : U := + \sum_(t <- finsupp x) x t *: f t. + +Lemma free_lmod_eval_linear : linear free_lmod_eval. +Proof. +move=> a x y; rewrite [free_lmod_eval]unlock scaler_sumr. +rewrite (big_fset_incl _ (fsubsetUr (finsupp x `|` finsupp y)%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. +apply: esym; rewrite (big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp y))%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r scaler0. +rewrite [X in _ + X](big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp x))%fset _))/=; last first. + by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. +rewrite fsetUAC -big_split/= -fsetUA fsetUC. +by apply: eq_bigr => i _; rewrite free_lmodDE/= scalerDl free_lmodZE scalerA. +Qed. + +HB.instance Definition _ := GRing.isLinear.Build _ _ _ _ free_lmod_eval free_lmod_eval_linear. + +End eval. + End FreeLmod. +Arguments free_lmod : clear implicits. +Notation "x %:lmod" := (free_lmod_unit x). + + +Section free_lmod_map. +Context {R : comRingType}. +Implicit Types X Y Z : choiceType. + +Definition free_lmod_map {X Y} + (f : X -> Y) (u : free_lmod R X) : free_lmod R Y := + free_lmod_eval (free_lmod_unit \o f) u. + +Definition free_lmod_map_id {X} : free_lmod_map (@id X) =1 id. +Proof. +move=> u /=; rewrite /free_lmod_map; apply/fsfunP => x /=. +rewrite unlock /= free_lmod_sumE. +case: (finsuppP u x) => [xNu|xu]. + rewrite big1// => i _; rewrite free_lmodZE free_lmod_unitE. + by case: eqVneq; rewrite (mulr1,mulr0)// => ->; rewrite fsfun_dflt. +rewrite (bigD1_seq x)//= free_lmodZE ?free_lmod_unitE eqxx mulr1 big1 ?addr0//. +by move=> y nyx; rewrite free_lmodZE free_lmod_unitE (negPf nyx) mulr0. +Qed. + + +Definition free_lmod_map_comp {X Y Z} (f : X -> Y) (g : Y -> Z) : + free_lmod_map (g \o f) =1 free_lmod_map g \o free_lmod_map f. +Proof. +move=> u /=; rewrite /free_lmod_map/=. +rewrite ![@free_lmod_eval _ _ _ _]unlock. +Admitted. + +End free_lmod_map. + + HB.mixin Record ZmodQuotient_isLmodQuotient (R : pzRingType) T eqT (zeroT : T) (oppT : T -> T) (addT : T -> T -> T) (scaleT : R -> T -> T) @@ -153,9 +235,9 @@ Definition Pzmod : {pred _} := P. HB.instance Definition _ := GRing.SubmodClosed.on Pzmod. HB.instance Definition _ := @SubmodClosed_isZmodClosed.Build R L Pzmod. -Notation quot := (quot Pzmod). +Definition zmodquot := (quot Pzmod). -Definition scale a := lift_op1 quot ( *:%R a). +Definition scale a := lift_op1 zmodquot ( *:%R a). Lemma pi_scale a : {morph \pi : x / a *: x >-> scale a x}. Proof. @@ -177,12 +259,14 @@ Proof. by move=> a f g; rewrite -[f]reprK -[g]reprK !piE scalerDr. Qed. Let scalerDl f : {morph scale^~ f: a b / a + b}. Proof. by move=> a b; rewrite -[f]reprK !piE scalerDl. Qed. +#[export] +HB.instance Definition _ := ZmodQuotient.on zmodquot. #[export] HB.instance Definition _ := - GRing.Zmodule_isLmodule.Build R quot scalerA scale1r scalerDr scalerDl. + GRing.Zmodule_isLmodule.Build R zmodquot scalerA scale1r scalerDr scalerDl. #[export] HB.instance Definition _ := - ZmodQuotient_isLmodQuotient.Build R L (equiv Pzmod) 0 -%R +%R *:%R quot pi_scale. + ZmodQuotient_isLmodQuotient.Build R L (equiv Pzmod) 0 -%R +%R *:%R zmodquot pi_scale. End LmodQuotient. Module Exports. HB.reexport. End Exports. @@ -202,52 +286,64 @@ Let bV := vbasis (@fullv _ V). Definition fintensor := free_lmod R ('I_nU * 'I_nV)%type. -Definition fintensor_proj (x : U * V) : fintensor := - fsfun_of_fun free_lmod_key (unpickle setT) (fun i => coord bU i.1 x.1 * coord bV i.2 x.2) (fun=> 0). +Elpi lock Definition fintensor_proj (x : U * V) : fintensor := + [fsfun i in [fset i in 'I_nU] `*` [fset i in 'I_nV] + => coord bU i.1 x.1 * coord bV i.2 x.2]. End fintensor. Section span. -Variables (R : fieldType) (U : lmodType R) (X : {fset U}). - -Definition of_span_subdef (x : free_lmod R X) := - \sum_(i <- finsupp x) x i *: val i. - -Lemma of_span_subdef_linear : linear of_span_subdef. -Proof. -move=> a x y; rewrite /of_span_subdef scaler_sumr. -rewrite (big_fset_incl _ (fsubsetUr (finsupp x `|` finsupp y)%fset _))/=; last first. - by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. -apply: esym; rewrite (big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp y))%fset _))/=; last first. - by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r scaler0. -rewrite [X in _ + X](big_fset_incl _ (fsubsetUr (finsupp (a *: x + y)%R `|` (finsupp x))%fset _))/=; last first. - by move=> i _; rewrite mem_finsupp negbK => /eqP ->; rewrite scale0r. -rewrite fsetUAC -big_split/= -fsetUA fsetUC. -by apply: eq_bigr => i _; rewrite free_lmodDE/= scalerDl free_lmodZE scalerA. -Qed. - -HB.instance Definition _ := GRing.isLinear.Build _ _ _ _ of_span_subdef of_span_subdef_linear. +Variables (R : comRingType) (U : lmodType R) (X : {fset U}). -Definition spanI0 (x : free_lmod R X) := of_span_subdef x == 0. +Definition span_ideal : {pred free_lmod R X} := + [pred x | free_lmod_eval (val : X -> U) x == 0]. -Lemma spanI0_submod_closed : submod_closed spanI0. +Lemma span_ideal_submod_closed : submod_closed span_ideal. Proof. split=> [|a x y]; rewrite !unfold_in; first by rewrite linear0. by rewrite linearPZ/= => /eqP -> /eqP ->; rewrite scaler0 addr0. Qed. -HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ spanI0 spanI0_submod_closed. +HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ span_ideal span_ideal_submod_closed. -(* TODO: Why does the reverse coercion fail to apply? *) -Definition span := Quotient.quot Tensor_spanI0__canonical__GRing_SubmodClosed. - -Check span : zmodType . +Definition span := Quotient.zmodquot span_ideal. End span. Section tensor. Variables (R : fieldType) (U V : lmodType R). -Definition equiv (x y : free_lmod R (U * V)%type) := true. +Let tensor_ideal_left_generators : set (free_lmod R (U * V)%type) := + [set (x.1.1 *: x.1.2 + x.2.1, x.2.2)%:lmod + - x.1.1 *: (x.1.2, x.2.2)%:lmod - (x.2.1, x.2.2)%:lmod + | x in @setT ((R * U) * (U * V))%type]. + +Let tensor_ideal_right_generators : set (free_lmod R (U * V)%type) := + [set (x.2.2, x.1.1 *: x.1.2 + x.2.1)%:lmod + - x.1.1 *: (x.2.2, x.1.2)%:lmod - (x.2.2, x.2.1)%:lmod + | x in @setT ((R * V) * (V * U))%type]. + +Let tensor_ideal_generators := + (tensor_ideal_left_generators `|` tensor_ideal_right_generators)%classic. + +Definition tensor_ideal_set : set (free_lmod R (U * V)%type) := + smallest (fun X => submod_closed [pred x in X]) tensor_ideal_generators. +Definition tensor_ideal := [pred x in tensor_ideal_set]. + +Lemma tensor_ideal_submod_closed : submod_closed tensor_ideal. +Proof. +constructor; first by rewrite inE/=; move => /= A [[/[!inE]]]. +move=> /= x u v /[!inE] ut vt. +move=> /= A [/[dup] Asubmod [_ /(_ x u v)] /[!inE] /[swap] inA]; apply. + by apply: ut; split. +by apply: vt; split. +Qed. + +HB.instance Definition _ := + GRing.isSubmodClosed.Build _ _ tensor_ideal tensor_ideal_submod_closed. + +Definition tensor := Quotient.zmodquot tensor_ideal. +HB.instance Definition _ := LmodQuotient.on tensor. + End tensor. End Tensor. From 4a19ddf214047ce9bd5d7bf8de2189f67237cfa7 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 14 Nov 2025 20:20:40 +0100 Subject: [PATCH 6/9] Finished binary tensor --- classical/tensor.v | 159 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 137 insertions(+), 22 deletions(-) diff --git a/classical/tensor.v b/classical/tensor.v index 14fd4b478b..4f77e4fe14 100644 --- a/classical/tensor.v +++ b/classical/tensor.v @@ -1,7 +1,8 @@ From HB Require Import structures. From elpi Require Import elpi. -From mathcomp Require Import all_ssreflect ssralg vector ring_quotient finmap. -From mathcomp Require Import boolp functions classical_sets. +From mathcomp Require Import all_ssreflect ssralg vector ring_quotient. +From mathcomp Require Import sesquilinear. +From mathcomp Require Import finmap boolp functions classical_sets. Import GRing.Theory. @@ -27,6 +28,7 @@ Section lmodType. (* This is the unit of the monad *) Elpi lock Definition free_lmod_unit (x : T) : free_lmod := [fsfun [fsfun] with x |-> 1]. +Local Notation "x %:lmod" := (free_lmod_unit x). Elpi lock Definition zero_subdef : free_lmod := [fsfun]. Local Notation zero := zero_subdef. @@ -119,7 +121,9 @@ Proof. by rewrite [free_lmod_unit]unlock fsfunE/= !inE/= orbF; case: eqVneq. Qed. + End lmodType. +Notation "x %:lmod" := (free_lmod_unit x). Section eval. Context {U : lmodType R} (f : T -> U). @@ -145,9 +149,35 @@ HB.instance Definition _ := GRing.isLinear.Build _ _ _ _ free_lmod_eval free_lmo End eval. End FreeLmod. -Arguments free_lmod : clear implicits. +Arguments free_lmod R T%_type : clear implicits. Notation "x %:lmod" := (free_lmod_unit x). +Lemma finsupp_free_lmod_unit {R : nzRingType} {T : choiceType} (t : T) : + finsupp (t%:lmod : free_lmod R T) = [fset t]. +Proof. +apply/fsetP=> i; rewrite inE mem_finsupp free_lmod_unitE. +by case: (eqVneq i t); rewrite ?eqxx// oner_eq0. +Qed. + +Lemma free_lmod_eval_unit {R : nzRingType} {T : choiceType} + {U : lmodType R} (f : T -> U) (t : T) : free_lmod_eval f t%:lmod = f t. +Proof. +rewrite [free_lmod_eval _]unlock finsupp_free_lmod_unit. +by rewrite big_seq_fset1 free_lmod_unitE eqxx scale1r. +Qed. + +Section general_kernel. +Context {R : nzRingType} {U V : lmodType R}. +Definition ker_set (f : U -> V) : set U := + [set u | f u = 0]. + +Lemma ker_submod_closed (f : {linear U -> V}) : submod_closed [pred x in ker_set f]. +Proof. +split => [|x u v] /[!inE]; rewrite /ker_set/=; first exact: linear0. +by move=> + + /[!linearP] => -> ->; rewrite scaler0 addr0. +Qed. + +End general_kernel. Section free_lmod_map. Context {R : comRingType}. @@ -276,7 +306,7 @@ Export Quotient.Exports. Module Tensor. -Section fintensor. +Section fiptensor. Variables (R : fieldType) (U V : vectType R). Let nU := \dim (@fullv _ U). @@ -284,49 +314,48 @@ Let nV := \dim (@fullv _ V). Let bU := vbasis (@fullv _ U). Let bV := vbasis (@fullv _ V). -Definition fintensor := free_lmod R ('I_nU * 'I_nV)%type. +Definition fiptensor := free_lmod R ('I_nU * 'I_nV). -Elpi lock Definition fintensor_proj (x : U * V) : fintensor := +Elpi lock Definition fiptensor_proj (x : U * V) : fiptensor := [fsfun i in [fset i in 'I_nU] `*` [fset i in 'I_nV] => coord bU i.1 x.1 * coord bV i.2 x.2]. -End fintensor. +End fiptensor. Section span. Variables (R : comRingType) (U : lmodType R) (X : {fset U}). Definition span_ideal : {pred free_lmod R X} := - [pred x | free_lmod_eval (val : X -> U) x == 0]. + [pred x in ker_set (free_lmod_eval (val : X -> U))]. Lemma span_ideal_submod_closed : submod_closed span_ideal. -Proof. -split=> [|a x y]; rewrite !unfold_in; first by rewrite linear0. -by rewrite linearPZ/= => /eqP -> /eqP ->; rewrite scaler0 addr0. -Qed. +Proof. exact: ker_submod_closed. Qed. -HB.instance Definition _ := GRing.isSubmodClosed.Build _ _ span_ideal span_ideal_submod_closed. +HB.instance Definition _ := + GRing.isSubmodClosed.Build _ _ span_ideal span_ideal_submod_closed. Definition span := Quotient.zmodquot span_ideal. End span. +End Tensor. -Section tensor. -Variables (R : fieldType) (U V : lmodType R). +Section Biptensor. +Variables (R : comRingType) (U V : lmodType R). -Let tensor_ideal_left_generators : set (free_lmod R (U * V)%type) := +Let tensor_ideal_left_generators : set (free_lmod R (U * V)) := [set (x.1.1 *: x.1.2 + x.2.1, x.2.2)%:lmod - - x.1.1 *: (x.1.2, x.2.2)%:lmod - (x.2.1, x.2.2)%:lmod + - (x.1.1 *: (x.1.2, x.2.2)%:lmod + (x.2.1, x.2.2)%:lmod) | x in @setT ((R * U) * (U * V))%type]. -Let tensor_ideal_right_generators : set (free_lmod R (U * V)%type) := +Let tensor_ideal_right_generators : set (free_lmod R (U * V)) := [set (x.2.2, x.1.1 *: x.1.2 + x.2.1)%:lmod - - x.1.1 *: (x.2.2, x.1.2)%:lmod - (x.2.2, x.2.1)%:lmod + - (x.1.1 *: (x.2.2, x.1.2)%:lmod + (x.2.2, x.2.1)%:lmod) | x in @setT ((R * V) * (V * U))%type]. Let tensor_ideal_generators := (tensor_ideal_left_generators `|` tensor_ideal_right_generators)%classic. -Definition tensor_ideal_set : set (free_lmod R (U * V)%type) := +Definition tensor_ideal_set : set (free_lmod R _) := smallest (fun X => submod_closed [pred x in X]) tensor_ideal_generators. Definition tensor_ideal := [pred x in tensor_ideal_set]. @@ -345,5 +374,91 @@ HB.instance Definition _ := Definition tensor := Quotient.zmodquot tensor_ideal. HB.instance Definition _ := LmodQuotient.on tensor. -End tensor. -End Tensor. +Definition to_tensor (u : U) (v : V) := \pi_tensor ((u, v)%:lmod). +Notation "u *t v" := (to_tensor u v) (at level 40) : ring_scope. + +Variable (W : lmodType R). + +Definition tensor_umap (f : U -> V -> W) (t : tensor) : W := + free_lmod_eval (uncurry f) (repr t). + +Lemma eq_free_lmod_eval (f : {bilinear U -> V -> W}) (a b : free_lmod R (U * V)) : + a = b %[mod tensor] -> free_lmod_eval (uncurry f) a = free_lmod_eval (uncurry f) b. +Proof. +move=> /eqquotP; rewrite Quotient.equivE !inE /= => ab0. +(* rewrite [free_lmod_eval _]unlock. *) +apply/eqP; rewrite -subr_eq0 -raddfB/=; apply/eqP. +suff: ker_set (free_lmod_eval (uncurry f)) (a - b) by []. +apply: ab0; split; first exact: ker_submod_closed. +by move=> g [[x _ <-]|[x _ <-]]; rewrite /ker_set/= !(linearZ, linearB, linearD)/=; + rewrite !free_lmod_eval_unit/= ?linearPr ?linearPl ?scalerN; + rewrite addrACA !subrr addr0. +Qed. + +Lemma tensor_umap_is_linear (f : {bilinear U -> V -> W}) : linear (tensor_umap f). +Proof. +move=> x t1 t2; rewrite /tensor_umap/=. +have: repr (x *: t1 + t2) = x *: repr t1 + repr t2 %[mod tensor]. + by rewrite linearP/= !reprK. +move=> /eq_free_lmod_eval ->. +rewrite [free_lmod_eval _]unlock. +set A := finsupp _; set B := finsupp _; set C := finsupp _. +rewrite (big_fset_incl _ (fsubsetUl _ (B `|` C)%fset))/=; last first. + by move=> uv _ /fsfun_dflt->; rewrite scale0r. +rewrite [in RHS](big_fset_incl _ (fsubsetUl _ (A `|` C)%fset))/=; last first. + by move=> uv _ /fsfun_dflt->; rewrite scale0r. +rewrite [in X in _ = _ + X](big_fset_incl _ (fsubsetUr (A `|` B)%fset _))/=; last first. + by move=> uv _ /fsfun_dflt->; rewrite scale0r. +rewrite [in RHS]fsetUCA !fsetUA. +rewrite scaler_sumr -big_split/=; apply/eq_bigr => -[u v] _ /=. +rewrite scalerA -scalerDl; apply/eqP; rewrite -subr_eq0 -scalerBl. +by rewrite free_lmodDE/= free_lmodZE/= subrr scale0r. +Qed. +HB.instance Definition _ (f : {bilinear U -> V -> W}) := + GRing.isLinear.Build _ _ _ _ (tensor_umap f) (tensor_umap_is_linear f). + +Definition tensor_universal_mapP (f : {bilinear U -> V -> W}) (u : U) (v : V) : + tensor_umap f (u *t v) = f u v. +Proof. +rewrite /tensor_umap /to_tensor. +have : repr (\pi_tensor (u, v)%:lmod) = (u, v)%:lmod %[mod tensor]. + by rewrite reprK. +move=> /eq_free_lmod_eval->. +rewrite [free_lmod_eval _]unlock/= finsupp_free_lmod_unit. +by rewrite big_seq_fset1 free_lmod_unitE eqxx scale1r. +Qed. + +End Biptensor. + +Section ProdTensor. +Variables (R : fieldType) (I : eqType) (U_ : I -> lmodType R). + +Let ptensor_ideal_generators : set (free_lmod R (forall i, U_ i)) := + [set + (fun i => (if tag (x.1.1) =P i is ReflectT xi then x.1.2 *: etagged xi else 0) + x.2 i)%:lmod + - (x.1.2 *: (fun i => if tag (x.1.1) =P i is ReflectT xi then etagged xi else x.2 i)%:lmod + x.2%:lmod) + | x in @setT (({i : I & U_ i} * R) * (forall i, U_ i))%type]. + +Definition ptensor_ideal_set : set (free_lmod R _) := + smallest (fun X => submod_closed [pred x in X]) ptensor_ideal_generators. +Definition ptensor_ideal : {pred _} := [pred x in ptensor_ideal_set]. + +Lemma ptensor_ideal_submod_closed : submod_closed ptensor_ideal. +Proof. +constructor; first by rewrite inE/=; move => /= A [[/[!inE]]]. +move=> /= x u v /[!inE] ut vt. +move=> /= A [/[dup] Asubmod [_ /(_ x u v)] /[!inE] /[swap] inA]; apply. + by apply: ut; split. +by apply: vt; split. +Qed. + +HB.instance Definition _ := + GRing.isSubmodClosed.Build _ _ ptensor_ideal ptensor_ideal_submod_closed. + +Definition ptensor := Quotient.zmodquot ptensor_ideal. +HB.instance Definition _ := LmodQuotient.on ptensor. + +Definition to_ptensor (u_ : forall i, U_ i) := \pi_ptensor (u_%:lmod). +Notation "u %:tensor" := (to_ptensor u) : ring_scope. + +End ProdTensor. From 1444ed1a7ece26f2929fefab9ba1db686f0c4377 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 17 Nov 2025 14:49:51 +0100 Subject: [PATCH 7/9] proof --- classical/tensor.v | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/classical/tensor.v b/classical/tensor.v index 4f77e4fe14..1dd5217d6c 100644 --- a/classical/tensor.v +++ b/classical/tensor.v @@ -204,7 +204,20 @@ Definition free_lmod_map_comp {X Y Z} (f : X -> Y) (g : Y -> Z) : Proof. move=> u /=; rewrite /free_lmod_map/=. rewrite ![@free_lmod_eval _ _ _ _]unlock. -Admitted. +rewrite (@big_fset_incl _ _ _ _ _ [fset f x | x in finsupp u])/=; first last. +- move=> _ /imfsetP[] x/= xu ->; rewrite mem_finsupp negbK => /eqP ->. + exact: scale0r. +- apply/fsubsetP => y; rewrite mem_finsupp => /eqP; apply: contra_notT => yf. + rewrite free_lmod_sumE big_seq; apply: big1 => x xu. + rewrite free_lmodZE/= free_lmod_unitE. + case: eqP => yE; last by rewrite mulr0. + by elim: (negP yf); apply/imfsetP; exists x. +rewrite (partition_big_imfset _ f)/=; apply: eq_bigr => y _. +rewrite big_mkcond/= free_lmod_sumE scaler_suml; apply: eq_bigr => x _. +rewrite free_lmodZE free_lmod_unitE. +case: eqP => [<-|]; first by rewrite mulr1. +by rewrite mulr0 scale0r. +Qed. End free_lmod_map. From 03b373e3de698bd935addecd0ae57b597eaa3eba Mon Sep 17 00:00:00 2001 From: Gabriella Clemente Date: Tue, 18 Nov 2025 14:31:09 +0100 Subject: [PATCH 8/9] commit --- classical/multilinear.v | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 classical/multilinear.v diff --git a/classical/multilinear.v b/classical/multilinear.v new file mode 100644 index 0000000000..49f775c771 --- /dev/null +++ b/classical/multilinear.v @@ -0,0 +1,22 @@ +From HB Require Import structures. +From elpi Require Import elpi. +From mathcomp Require Import all_ssreflect ssralg vector ring_quotient. +From mathcomp Require Import sesquilinear. +From mathcomp Require Import finmap boolp functions classical_sets. + +Import GRing.Theory. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +Local Open Scope fset_scope. +Local Open Scope ring_scope. +Local Open Scope quotient_scope. + +HB.mixin Record isMultilinear (I : eqType) (R : pzSemiRingType) + (V : I -> lSemiModType R) (W : lSemiModType R) + (f : (forall i, V i) -> W) := { + ilinear : forall i : I, forall v :(forall i, V i), + linear (f \o (fun x : V i => dfwith v x)) +}. From 1d50b759add361d32f82cedf1cb7cb0525525ea1 Mon Sep 17 00:00:00 2001 From: Gabriella Clemente Date: Tue, 18 Nov 2025 15:47:36 +0100 Subject: [PATCH 9/9] multilinear --- classical/multilinear.v | 51 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/classical/multilinear.v b/classical/multilinear.v index 49f775c771..d42ae87d76 100644 --- a/classical/multilinear.v +++ b/classical/multilinear.v @@ -14,9 +14,60 @@ Local Open Scope fset_scope. Local Open Scope ring_scope. Local Open Scope quotient_scope. +Definition is_multilinear (I : eqType) (R : pzSemiRingType) + (V : I -> lSemiModType R) (W : lSemiModType R) + (f : (forall i, V i) -> W):=forall i : I, forall v :(forall i, V i), + linear (f \o (fun x : V i => dfwith v x)). + HB.mixin Record isMultilinear (I : eqType) (R : pzSemiRingType) (V : I -> lSemiModType R) (W : lSemiModType R) (f : (forall i, V i) -> W) := { ilinear : forall i : I, forall v :(forall i, V i), linear (f \o (fun x : V i => dfwith v x)) }. + +#[short(type="multilinearType")] +HB.structure Definition Multilinear (I : eqType) (R : pzSemiRingType) + (V : I -> lSemiModType R) (W : lSemiModType R):= + {f of @isMultilinear I R V W f}. + +Lemma multilinearEP (I : eqType) (R : pzSemiRingType) + (V : I -> lSemiModType R) (W : lSemiModType R) (f g : multilinearType V W): + f = g <-> f =1 g. +Proof. +case: f g => [f [[ffun]]] [g [[gfun]]]/= ; split=> [[->//]|/funext eqfg]. +rewrite eqfg in ffun *; congr {| Multilinear.sort := _; Multilinear.class := {| + Multilinear.multilinear_isMultilinear_mixin := + {| isMultilinear.ilinear := _|}|}|}. +exact: Prop_irrelevance. +Qed. + +Section TopologicalNmoduleTheory. +Variables (R : pzSemiRingType) (I : eqType) (V : I -> lSemiModType R) + (W : lSemiModType R). + +Let addfun_multilinear (f g : multilinearType V W) : is_multilinear (f \+ g). +Proof. +move=> i v. +admit. + +Admitted. + +HB.instance Definition _ (f g : continuousType M N) := + isContinuous.Build M N (f \+ g) (@addfun_continuous f g). + +Let addrA : associative (fun f g : continuousType M N => f \+ g). +Proof. by move=> f g h; apply/continuousEP => x; apply: addrA. Qed. + +Let addrC : @commutative _ (continuousType M N) + (fun f g : continuousType M N => f \+ g). +Proof. by move=> f g; apply/continuousEP => x; apply: addrC. Qed. + +Let add0r : @left_id (continuousType M N) _ (cst 0) + (fun f g : continuousType M N => f \+ g). +Proof. by move=> f; apply/continuousEP => x; apply: add0r. Qed. + +HB.instance Definition _ := + GRing.isNmodule.Build (continuousType M N) addrA addrC add0r. + +End TopologicalNmoduleTheory.