From 48fdcb71225747b16e87ee128933ef6985f7c43b Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Sun, 24 Aug 2025 11:39:14 +0200 Subject: [PATCH 1/7] normed vector types, infinite norm, norm equivalence thm, continuity of linear functions in finite dimension --- CHANGELOG_UNRELEASED.md | 9 + theories/normedtype_theory/normed_module.v | 244 +++++++++++++++++++++ theories/normedtype_theory/tvs.v | 19 ++ 3 files changed, 272 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0366d7f63..817da044b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -71,6 +71,15 @@ - in `derive.v`: + lemmas `compact_EVT_max`, `compact_EVT_min`, `EVT_max_rV`, `EVT_min_rV` +- in `tvs.v` + + lemmas `cvg_sum`, `sum_continuous` + +- in `normed_module.v`: + + structure `NormedVector` + + definitions `normedVectType`, `max_norm`, `max_space` + + lemmas `max_norm_ge0`, `le_coord_max_norm`, `ler_max_normD`, `max_norm0_eq0`, + `max_normZ`, `max_normMn`, `max_normN`, `sup_closed_ball_compact`, + `equivalence_norms`, `linear_findim_continuous` ### Changed diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 9ccf4583a..59ca03812 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -20,6 +20,9 @@ From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. (* normedModType K == interface type for a normed module *) (* structure over the numDomainType K *) (* The HB class is NormedModule. *) +(* normedVectType K == interface type for a normed vectType *) +(* structure over the numDomainType K *) +(* The HB class is NormedVector. *) (* `|x| == the norm of x (notation from ssrnum.v) *) (* ``` *) (* *) @@ -141,6 +144,10 @@ HB.instance Definition _ := HB.end. +#[short(type="normedVectType")] +HB.structure Definition NormedVector (K : numDomainType) := + {T of NormedModule K T & Vector K T}. + (**md see also `Section standard_topology_pseudoMetricNormedZmod` in `pseudometric_normed_Zmodule.v` *) Section standard_topology_normedMod. @@ -2447,3 +2454,240 @@ Lemma open_disjoint_itv_bigcup : U = \bigcup_q open_disjoint_itv q. Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. + +Section InfiniteNorm. +Variables (R : numFieldType) (V : vectType R) (B : (\dim (@fullv _ V)).-tuple V). +Let V' := @fullv _ V. +Hypothesis (Bbasis : basis_of V' B). + +Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. + +Definition max_space : Type := (fun=> V) Bbasis. + +HB.instance Definition _ := Vector.on max_space. + +HB.instance Definition _ := Pointed.copy max_space V^o. + +Lemma max_norm_ge0 x : 0 <= max_norm x. +Proof. +rewrite /max_norm. +elim: (index_enum _) => /=; first by rewrite big_nil. +by move=> i l IHl; rewrite big_cons /Order.max/=; case: ifP. +Qed. + +Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x. +Proof. +rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. +rewrite inE big_cons /Order.max/= => /orP[/eqP <-|/IHl {}IHl]; + case: ifP => [/ltW|]//. +move=> /negP/negP. +have bR: \big[Order.max/0]_(i <- l) `|coord B i x| \is Num.real. + exact: bigmax_real. +move: (real_comparable bR (normr_real (coord B j x))). +by move=> /comparable_leNgt <- /(le_trans IHl). +Qed. + +Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. +Proof. +apply: bigmax_le => [|/= i _]. + by apply: addr_ge0; apply: max_norm_ge0. +rewrite raddfD/=. +by apply/(le_trans (ler_normD _ _))/lerD; apply: le_coord_max_norm. +Qed. + +Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0. +Proof. +move=> x0. +rewrite (coord_basis Bbasis (memvf x)). +suff: forall i, coord B i x = 0. + move=> {}x0. + under eq_bigr do rewrite x0. + by rewrite -scaler_sumr scale0r. +move=> i; apply/normr0_eq0/le_anti/andP; split; last exact: normr_ge0. +by rewrite -x0; apply: le_coord_max_norm. +Qed. + +Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. +Proof. +rewrite /max_norm. +under eq_bigr do rewrite linearZ normrZ/=. +elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. +by rewrite !big_cons IHl maxr_pMr. +Qed. + +Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. +Proof. by rewrite -scaler_nat max_normZ normr_nat mulr_natl. Qed. + +Lemma max_normN x : max_norm (- x) = max_norm x. +Proof. by rewrite -scaleN1r max_normZ normrN1 mul1r. Qed. + +HB.instance Definition _ := Num.Zmodule_isNormed.Build R + max_space ler_max_normD max_norm0_eq0 max_normMn max_normN. + +HB.instance Definition _ := + PseudoMetric.copy max_space (pseudoMetric_normed max_space). + +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R max_space erefl. + +HB.instance Definition _ := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R max_space max_normZ. + +End InfiniteNorm. + +Section EquivalenceNorms. +Variables (R : realType) (V : vectType R). +Let V' := @fullv _ V. +Let Voo := max_space (vbasisP (@fullv _ V)). + +(* N.B. Get Trocq to prove the continuity part automatically. *) +Lemma sup_closed_ball_compact : compact (closed_ball (0 : Voo) 1). +Proof. +rewrite closed_ballE/closed_ball_//=. +under eq_set do rewrite sub0r normrN. +rewrite -[forall x, _]/(compact _). +pose f (X : {ptws 'I_(\dim V') -> R^o}) : Voo := + \sum_(i < \dim V') (X i) *: (vbasis V')`_i. +have -> : + [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. + apply/seteqP; split=> x/=. + move=> x1; exists (fun i => coord (vbasis V') i x); last first. + exact/esym/(@coord_vbasis _ _ (x : V))/memvf. + move=> i; rewrite in_itv/= -ler_norml. + apply: (le_trans _ x1). + exact: le_coord_max_norm. + move=> [X] X1 <-. + rewrite /normr/=/max_norm. + apply: bigmax_le => //= i _. + rewrite coord_sum_free; last exact/basis_free/vbasisP. + rewrite ler_norml. + exact: X1. +apply: (@continuous_compact _ _ f); last first. + apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1 : R^o]%classic)). + move=> _. + exact: segment_compact. +apply/continuous_subspaceT/sum_continuous => i _/= x. +exact/continuousZl/proj_continuous. +Qed. + +Lemma equivalence_norms (N : V -> R) : + N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> + (forall x y, N (x + y) <= N x + N y) -> + (forall r x, N (r *: x) = `|r| * N x) -> + exists M, 0 < M /\ forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. +Proof. +move=> N0 N_ge0 N0_eq0 ND NZ. +set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. +have N_sum (I : Type) (r : seq I) (F : I -> V): + N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). + elim: r => [|x r IHr]; first by rewrite !big_nil N0. + by rewrite !big_cons; apply/(le_trans (ND _ _))/lerD. +have leNoo: forall x : Voo, N x <= M0 * `|x|. + move=> x. + rewrite [in leLHS](coord_vbasis (memvf (x : V))). + apply: (le_trans (N_sum _ _ _)). + rewrite mulrDl mul1r mulr_suml -[leLHS]add0r. + apply: lerD => //. + apply: ler_sum => /= i _. + rewrite NZ mulrC; apply: ler_pM => //. + exact: le_coord_max_norm. +have M00 : 0 < M0. + rewrite -[ltLHS]addr0. + by apply: ltr_leD => //; apply: sumr_ge0. +have NC0 : continuous (N : Voo -> R). + move=> /= x. + rewrite /continuous_at. + apply: cvg_zero; first exact: nbhs_filter. + apply/cvgr0Pnorm_le; first exact: nbhs_filter. + move=> /= e e0. + near=> y. + rewrite -[_ y]/(N y - N x). + apply: (@le_trans _ _ (N (y - x))). + apply/real_ler_normlP. + by apply: realB; apply: ger0_real. + have NB a b : N a <= N b + N (a - b). + by rewrite -[a in N a]addr0 -(subrr b) addrCA ND. + rewrite opprB !lerBlDl; split; last exact: NB. + by rewrite -opprB -scaleN1r NZ normrN1 mul1r NB. + apply: (le_trans (leNoo _)). + rewrite mulrC -ler_pdivlMr// -opprB normrN. + near: y; apply: cvgr_dist_le; first exact: cvg_id. + exact: divr_gt0. +have: compact [set x : Voo | `|x| = 1]. + apply: (subclosed_compact _ sup_closed_ball_compact); last first. + apply/subsetP => x. + rewrite closed_ballE// !inE/=. + by rewrite /closed_ball_/= sub0r normrN => ->. + apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. + by rewrite /prop_in1 => + _; apply: norm_continuous. +move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[]. + exact: continuous_subspaceT. +move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. + move=> /= x. + rewrite /continuous_at. + apply: (@continuous_in_subspaceT _ _ + [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). + move=> r /set_mem/=[] y y1 <-. + apply: inv_continuous. + apply/negP => /eqP/N0_eq0 y0. + move: y1; rewrite y0 normr0 => /esym. + by move: (@oner_neq0 R) => /eqP. +move=> /compact_bounded[] M1 [] M1R /(_ (1 + M1)). +rewrite -subr_gt0 -addrA subrr addr0 => /(_ ltr01). +rewrite /globally/= => M1N. +exists (maxr M0 (1 + M1)). +split=> [|x]; first by apply: (lt_le_trans M00); rewrite le_max lexx. +split; last first. + apply/(le_trans (leNoo x))/ler_pM => //; first exact/ltW. + by rewrite /maxr; case: ifP => // /ltW. +have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0. +have Nx0: 0 < N x. + rewrite lt0r N_ge0 andbT. + by move: x0; apply: contra => /eqP/N0_eq0/eqP. +have normx0 : 0 < `|x|. + move: (lt_le_trans Nx0 (leNoo x)). + by rewrite pmulr_rgt0. +move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[]. + exists (N x / `|x|); last by rewrite invf_div. + exists (`|x|^-1 *: x); last first. + by rewrite NZ mulrC ger0_norm. + rewrite normrZ mulrC ger0_norm. + by rewrite divrr//; apply: unitf_gt0. + by rewrite invr_ge0; apply: ltW. +rewrite ger0_norm; last exact: divr_ge0. +rewrite ler_pdivrMr// => xle. +apply: (le_trans xle). +rewrite -subr_ge0 -mulrBl pmulr_lge0// subr_ge0. +by rewrite le_max lexx orbT. +Unshelve. all: by end_near. +Qed. + +End EquivalenceNorms. + +Section LinearContinuous. +Variables (R : realType) (V : normedVectType R) (W : normedModType R). + +Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f. +Proof. +set V' := @fullv _ V. +set B := vbasis V' => /= x. +rewrite /continuous_at. +rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum. +rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); + last first. + move=> y; rewrite [y in LHS](coord_vbasis (memvf y)) raddf_sum. + by apply: eq_big => // i _; apply: linearZ. +apply: cvg_sum => i _. +rewrite [X in _ --> X]linearZ/= -/B. +apply: cvgZl. +move: x; apply/linear_bounded_continuous/bounded_funP => r/=. +have := @equivalence_norms R V (@normr R V) (@normr0 _ _) (@normr_ge0 _ _) + (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). +move=> [] M [] M0 MP. +exists (M * r) => x. +move: MP => /(_ x)[] Mx Mx' xr. +apply/(le_trans (le_coord_max_norm _ _ _))/(le_trans Mx). +rewrite -subr_ge0 -mulrBr; apply: mulr_ge0; first exact: ltW. +by rewrite subr_ge0. +Qed. + +End LinearContinuous. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index c67224749..181d0108f 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -85,6 +85,25 @@ HB.mixin Record PreTopologicalNmodule_isTopologicalNmodule M HB.structure Definition TopologicalNmodule := {M of PreTopologicalNmodule M & PreTopologicalNmodule_isTopologicalNmodule M}. +Section TopologicalNmodule_Theory. + +Lemma cvg_sum (T : Type) (U : TopologicalNmodule.type) (F : set_system T) + (I : Type) (r : seq I) (P : pred I) (Ff : I -> T -> U) (Fa : I -> U) : + Filter F -> (forall i, P i -> Ff i x @[x --> F] --> Fa i) -> + \sum_(i <- r | P i) Ff i x @[x --> F] --> \sum_(i <- r| P i) Fa i. +Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. + +Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) + (I : Type) (r : seq I) (P : pred I) (F : I -> T -> M) : + (forall i : I, P i -> continuous (F i)) -> + continuous (fun x1 : T => \sum_(i <- r | P i) F i x1). +Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. + +End TopologicalNmodule_Theory. + +HB.structure Definition PreTopologicalZmodule := + {M of Topological M & GRing.Zmodule M}. + HB.mixin Record TopologicalNmodule_isTopologicalZmodule M & Topological M & GRing.Zmodule M := { opp_continuous : continuous (-%R : M -> M) ; From d25ddef16964ab22f9f677fc4dcbe62d976d4c5c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 8 Dec 2025 10:15:16 +0900 Subject: [PATCH 2/7] linting --- theories/normedtype_theory/normed_module.v | 192 ++++++++------------- 1 file changed, 71 insertions(+), 121 deletions(-) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 59ca03812..c7974b476 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2456,9 +2456,10 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. Section InfiniteNorm. -Variables (R : numFieldType) (V : vectType R) (B : (\dim (@fullv _ V)).-tuple V). +Variables (R : numFieldType) (V : vectType R). Let V' := @fullv _ V. -Hypothesis (Bbasis : basis_of V' B). +Variable B : (\dim V').-tuple V. +Hypothesis Bbasis : basis_of V' B. Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. @@ -2471,40 +2472,31 @@ HB.instance Definition _ := Pointed.copy max_space V^o. Lemma max_norm_ge0 x : 0 <= max_norm x. Proof. rewrite /max_norm. -elim: (index_enum _) => /=; first by rewrite big_nil. -by move=> i l IHl; rewrite big_cons /Order.max/=; case: ifP. +by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. Qed. Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x. Proof. rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. -rewrite inE big_cons /Order.max/= => /orP[/eqP <-|/IHl {}IHl]; - case: ifP => [/ltW|]//. -move=> /negP/negP. -have bR: \big[Order.max/0]_(i <- l) `|coord B i x| \is Num.real. - exact: bigmax_real. -move: (real_comparable bR (normr_real (coord B j x))). -by move=> /comparable_leNgt <- /(le_trans IHl). +rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; + case: ifP => [/ltW|]// /negbT. +set b := (X in _ < X); have bR : b \is Num.real by exact: bigmax_real. +have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)). +by move=> /(le_trans IHl). Qed. Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. Proof. -apply: bigmax_le => [|/= i _]. - by apply: addr_ge0; apply: max_norm_ge0. -rewrite raddfD/=. -by apply/(le_trans (ler_normD _ _))/lerD; apply: le_coord_max_norm. +apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. +by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. Qed. Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0. Proof. -move=> x0. -rewrite (coord_basis Bbasis (memvf x)). +move=> x0; rewrite (coord_basis Bbasis (memvf x)). suff: forall i, coord B i x = 0. - move=> {}x0. - under eq_bigr do rewrite x0. - by rewrite -scaler_sumr scale0r. -move=> i; apply/normr0_eq0/le_anti/andP; split; last exact: normr_ge0. -by rewrite -x0; apply: le_coord_max_norm. + by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. +by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. Qed. Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. @@ -2542,124 +2534,85 @@ Let Voo := max_space (vbasisP (@fullv _ V)). (* N.B. Get Trocq to prove the continuity part automatically. *) Lemma sup_closed_ball_compact : compact (closed_ball (0 : Voo) 1). Proof. -rewrite closed_ballE/closed_ball_//=. +rewrite closed_ballE// /closed_ball_. under eq_set do rewrite sub0r normrN. rewrite -[forall x, _]/(compact _). -pose f (X : {ptws 'I_(\dim V') -> R^o}) : Voo := - \sum_(i < \dim V') (X i) *: (vbasis V')`_i. -have -> : - [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. - apply/seteqP; split=> x/=. - move=> x1; exists (fun i => coord (vbasis V') i x); last first. +pose f (X : {ptws 'I_(\dim V') -> R}) : Voo := + \sum_(i < \dim V') X i *: (vbasis V')`_i. +have -> : [set x : Voo | `|x| <= 1] = + f @` [set X | forall i, `[-1, 1]%classic (X i)]. + apply/seteqP; split=> [x/= x1|x/= [X X1 <-]]. + - exists (coord (vbasis V') ^~ x); last first. exact/esym/(@coord_vbasis _ _ (x : V))/memvf. - move=> i; rewrite in_itv/= -ler_norml. - apply: (le_trans _ x1). - exact: le_coord_max_norm. - move=> [X] X1 <-. - rewrite /normr/=/max_norm. - apply: bigmax_le => //= i _. - rewrite coord_sum_free; last exact/basis_free/vbasisP. - rewrite ler_norml. - exact: X1. -apply: (@continuous_compact _ _ f); last first. - apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1 : R^o]%classic)). - move=> _. + by move=> i; rewrite in_itv/= -ler_norml (le_trans _ x1)// le_coord_max_norm. + - rewrite /normr/= /max_norm bigmax_le => //= i _. + by rewrite coord_sum_free ?ler_norml; [exact: X1|exact/basis_free/vbasisP]. +apply: (@continuous_compact _ _ f). +- apply/continuous_subspaceT/sum_continuous => /= i _ x. + exact/continuousZr_tmp/proj_continuous. +- apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1]%classic)) => _. exact: segment_compact. -apply/continuous_subspaceT/sum_continuous => i _/= x. -exact/continuousZl/proj_continuous. Qed. Lemma equivalence_norms (N : V -> R) : N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> (forall x y, N (x + y) <= N x + N y) -> (forall r x, N (r *: x) = `|r| * N x) -> - exists M, 0 < M /\ forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. + exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. Proof. move=> N0 N_ge0 N0_eq0 ND NZ. set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. -have N_sum (I : Type) (r : seq I) (F : I -> V): - N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). - elim: r => [|x r IHr]; first by rewrite !big_nil N0. - by rewrite !big_cons; apply/(le_trans (ND _ _))/lerD. -have leNoo: forall x : Voo, N x <= M0 * `|x|. - move=> x. - rewrite [in leLHS](coord_vbasis (memvf (x : V))). - apply: (le_trans (N_sum _ _ _)). - rewrite mulrDl mul1r mulr_suml -[leLHS]add0r. - apply: lerD => //. - apply: ler_sum => /= i _. - rewrite NZ mulrC; apply: ler_pM => //. - exact: le_coord_max_norm. -have M00 : 0 < M0. - rewrite -[ltLHS]addr0. - by apply: ltr_leD => //; apply: sumr_ge0. +have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0. +have N_sum (I : Type) (r : seq I) (F : I -> V) : + N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). + by elim/big_ind2 : _ => *; rewrite ?N0// (le_trans (ND _ _))// lerD. +have leNoo (x : Voo) : N x <= M0 * `|x|. + rewrite [in leLHS](coord_vbasis (memvf (x : V))) (le_trans (N_sum _ _ _))//. + rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _. + by rewrite NZ mulrC ler_pM// le_coord_max_norm. +have NZN a : N (- a) = N a by rewrite -scaleN1r NZ normrN1 mul1r. have NC0 : continuous (N : Voo -> R). - move=> /= x. - rewrite /continuous_at. + move=> /= x; rewrite /continuous_at. apply: cvg_zero; first exact: nbhs_filter. apply/cvgr0Pnorm_le; first exact: nbhs_filter. move=> /= e e0. near=> y. - rewrite -[_ y]/(N y - N x). - apply: (@le_trans _ _ (N (y - x))). - apply/real_ler_normlP. - by apply: realB; apply: ger0_real. - have NB a b : N a <= N b + N (a - b). - by rewrite -[a in N a]addr0 -(subrr b) addrCA ND. - rewrite opprB !lerBlDl; split; last exact: NB. - by rewrite -opprB -scaleN1r NZ normrN1 mul1r NB. - apply: (le_trans (leNoo _)). - rewrite mulrC -ler_pdivlMr// -opprB normrN. - near: y; apply: cvgr_dist_le; first exact: cvg_id. - exact: divr_gt0. + rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//. + apply/ler_normlP. + have NB a b : N a <= N b + N (a - b). + by rewrite (le_trans _ (ND _ _)) ?subrKC. + by rewrite opprB !lerBlDl NB -opprB NZN NB. + rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN. + by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0]. have: compact [set x : Voo | `|x| = 1]. - apply: (subclosed_compact _ sup_closed_ball_compact); last first. - apply/subsetP => x. - rewrite closed_ballE// !inE/=. - by rewrite /closed_ball_/= sub0r normrN => ->. - apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. - by rewrite /prop_in1 => + _; apply: norm_continuous. + apply: (subclosed_compact _ sup_closed_ball_compact). + - apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. + by move=> *; exact: norm_continuous. + - by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->. move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[]. exact: continuous_subspaceT. move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. - move=> /= x. - rewrite /continuous_at. + move=> /= x; rewrite /continuous_at. apply: (@continuous_in_subspaceT _ _ [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). - move=> r /set_mem/=[] y y1 <-. + move=> /= r /set_mem/= [y y1 <-]. apply: inv_continuous. - apply/negP => /eqP/N0_eq0 y0. - move: y1; rewrite y0 normr0 => /esym. - by move: (@oner_neq0 R) => /eqP. -move=> /compact_bounded[] M1 [] M1R /(_ (1 + M1)). -rewrite -subr_gt0 -addrA subrr addr0 => /(_ ltr01). + by apply: contra_eq_neq y1 => /N0_eq0 ->; rewrite normr0 eq_sym oner_eq0. +move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))). rewrite /globally/= => M1N. -exists (maxr M0 (1 + M1)). -split=> [|x]; first by apply: (lt_le_trans M00); rewrite le_max lexx. -split; last first. - apply/(le_trans (leNoo x))/ler_pM => //; first exact/ltW. - by rewrite /maxr; case: ifP => // /ltW. +exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00. +split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx. have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0. -have Nx0: 0 < N x. - rewrite lt0r N_ge0 andbT. - by move: x0; apply: contra => /eqP/N0_eq0/eqP. -have normx0 : 0 < `|x|. - move: (lt_le_trans Nx0 (leNoo x)). - by rewrite pmulr_rgt0. +have Nx0 : 0 < N x. + by rewrite lt0r N_ge0 andbT; move: x0; apply: contra_neq => /N0_eq0. +have normx0 : 0 < `|x| by rewrite normr_gt0. move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[]. exists (N x / `|x|); last by rewrite invf_div. - exists (`|x|^-1 *: x); last first. - by rewrite NZ mulrC ger0_norm. - rewrite normrZ mulrC ger0_norm. - by rewrite divrr//; apply: unitf_gt0. - by rewrite invr_ge0; apply: ltW. -rewrite ger0_norm; last exact: divr_ge0. -rewrite ler_pdivrMr// => xle. -apply: (le_trans xle). -rewrite -subr_ge0 -mulrBl pmulr_lge0// subr_ge0. -by rewrite le_max lexx orbT. -Unshelve. all: by end_near. -Qed. + exists (`|x|^-1 *: x); last by rewrite NZ mulrC ger0_norm. + by rewrite normrZ normfV normr_id mulVf// gt_eqF. +rewrite ger0_norm ?divr_ge0// ler_pdivrMr// => /le_trans; apply. +by rewrite ler_pM2r// le_max lexx orbT. +Unshelve. all: by end_near. Qed. End EquivalenceNorms. @@ -2669,8 +2622,8 @@ Variables (R : realType) (V : normedVectType R) (W : normedModType R). Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f. Proof. set V' := @fullv _ V. -set B := vbasis V' => /= x. -rewrite /continuous_at. +set B := vbasis V'. +move=> /= x; rewrite /continuous_at. rewrite [x in f x](coord_vbasis (memvf x)) raddf_sum. rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); last first. @@ -2678,16 +2631,13 @@ rewrite (@eq_cvg _ _ _ _ (fun y => \sum_(i < \dim V') coord B i y *: f B`_i)); by apply: eq_big => // i _; apply: linearZ. apply: cvg_sum => i _. rewrite [X in _ --> X]linearZ/= -/B. -apply: cvgZl. +apply: cvgZr_tmp. move: x; apply/linear_bounded_continuous/bounded_funP => r/=. -have := @equivalence_norms R V (@normr R V) (@normr0 _ _) (@normr_ge0 _ _) - (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). -move=> [] M [] M0 MP. +have [M M0 MP] := @equivalence_norms R V (@normr R V) (@normr0 _ _) + (@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). exists (M * r) => x. -move: MP => /(_ x)[] Mx Mx' xr. -apply/(le_trans (le_coord_max_norm _ _ _))/(le_trans Mx). -rewrite -subr_ge0 -mulrBr; apply: mulr_ge0; first exact: ltW. -by rewrite subr_ge0. +move: MP => /(_ x) [Mx _] xr. +by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW. Qed. End LinearContinuous. From e820463ec5f0d847464b820362fdd99825e37249 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 20 Jan 2026 14:30:01 +0100 Subject: [PATCH 3/7] norm interface --- CHANGELOG_UNRELEASED.md | 14 ++- classical/unstable.v | 114 +++++++++++++++++- .../complete_normed_module.v | 5 +- theories/normedtype_theory/normed_module.v | 105 ++++------------ theories/normedtype_theory/tvs.v | 5 +- 5 files changed, 152 insertions(+), 91 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 817da044b..c21ed28b5 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -74,12 +74,18 @@ - in `tvs.v` + lemmas `cvg_sum`, `sum_continuous` +- in `unstable.v`: + + structure `Norm` + + lemmas `normMn`, `normN`, `ler_norm_sum` + + definitions `max_norm`, `max_space` + + lemmas `max_norm_ge0`, `le_coord_max_norm`, `max_norm0`, `ler_max_normD`, + `max_norm0_eq0`, `max_normZ`, `max_normMn`, `max_normN` + - in `normed_module.v`: + structure `NormedVector` - + definitions `normedVectType`, `max_norm`, `max_space` - + lemmas `max_norm_ge0`, `le_coord_max_norm`, `ler_max_normD`, `max_norm0_eq0`, - `max_normZ`, `max_normMn`, `max_normN`, `sup_closed_ball_compact`, - `equivalence_norms`, `linear_findim_continuous` + + definition `normedVectType` + + lemmas `sup_closed_ball_compact`, `equivalence_norms`, + `linear_findim_continuous` ### Changed diff --git a/classical/unstable.v b/classical/unstable.v index 617dbc9ae..4a653a76c 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -1,6 +1,7 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) +From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. -From mathcomp Require Import archimedean interval. +From mathcomp Require Import vector archimedean interval. (**md**************************************************************************) (* # MathComp extra *) @@ -592,3 +593,114 @@ Proof. exact: real_ltr_bound. Qed. Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R. Proof. exact: real_ltrNbound. Qed. + +Module Norm. + +HB.mixin Record isNorm (K : numDomainType) (L : lmodType K) (norm : L -> K) := { + norm0 : norm 0 = 0; + norm_ge0 : forall x, 0 <= norm x; + norm0_eq0 : forall x, norm x = 0 -> x = 0; + ler_normD : forall x y, norm (x + y) <= norm x + norm y; + normZ : forall r x, norm (r *: x) = `|r| * norm x; +}. + +#[export] +HB.structure Definition Norm K L := { norm of @isNorm K L norm }. + +Module Import Theory. +Section Theory. +Variables (K : numDomainType) (L : lmodType K) (norm : Norm.type L). + +Lemma normMn x n : norm (x *+ n) = norm x *+ n. +Proof. by rewrite -scaler_nat normZ normr_nat mulr_natl. Qed. + +Lemma normN x : norm (- x) = norm x. +Proof. by rewrite -scaleN1r normZ normrN1 mul1r. Qed. + +Lemma ler_norm_sum (I : Type) (r : seq I) (F : I -> L) : + norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i). +Proof. +by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD. +Qed. + +End Theory. +End Theory. + +Module Import Exports. HB.reexport. End Exports. +End Norm. +Export Norm.Exports. + +Section InfiniteNorm. +Variables (K : numFieldType) (V : vectType K). +Let V' := @fullv _ V. +Variable B : (\dim V').-tuple V. +Hypothesis Bbasis : basis_of V' B. + +Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. + +Definition max_space : Type := (fun=> V) Bbasis. + +HB.instance Definition _ := Vector.on max_space. + +Lemma max_norm_ge0 x : 0 <= max_norm x. +Proof. +rewrite /max_norm. +by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. +Qed. + +Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x. +Proof. +rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. +rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; + case: ifP => [/ltW|]// /negbT. +set b := (X in _ < X). +have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real. +have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)). +by move=> /(le_trans IHl). +Qed. + +Lemma max_norm0 : max_norm 0 = 0. +Proof. +apply: le_anti; rewrite max_norm_ge0 andbT. +apply: bigmax_le => // i _. +have <-: \sum_(i < \dim V') 0 *: B`_i = 0. + under eq_bigr do rewrite scale0r. + by rewrite sumr_const mul0rn. +by rewrite coord_sum_free ?normr0// (basis_free Bbasis). +Qed. + +Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. +Proof. +apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. +by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. +Qed. + +Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0. +Proof. +move=> x0; rewrite (coord_basis Bbasis (memvf x)). +suff: forall i, coord B i x = 0. + by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. +by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. +Qed. + +Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. +Proof. +rewrite /max_norm. +under eq_bigr do rewrite linearZ/= normrM. +elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. +by rewrite !big_cons IHl maxr_pMr. +Qed. + +HB.instance Definition _ := Norm.isNorm.Build K V max_norm + max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ. + +Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. +Proof. exact: Norm.Theory.normMn. Qed. + +Lemma max_normN x : max_norm (- x) = max_norm x. +Proof. exact: Norm.Theory.normN. Qed. + +HB.instance Definition _ := Num.Zmodule_isNormed.Build K + max_space ler_max_normD max_norm0_eq0 max_normMn max_normN. + +End InfiniteNorm. diff --git a/theories/normedtype_theory/complete_normed_module.v b/theories/normedtype_theory/complete_normed_module.v index cb95c2de8..12e52d0b4 100644 --- a/theories/normedtype_theory/complete_normed_module.v +++ b/theories/normedtype_theory/complete_normed_module.v @@ -1,7 +1,8 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum. -From mathcomp Require Import boolp classical_sets interval_inference reals. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. +From mathcomp Require Import interval_inference. +From mathcomp Require Import boolp classical_sets reals. From mathcomp Require Import topology tvs pseudometric_normed_Zmodule. From mathcomp Require Import normed_module. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index c7974b476..7c320f4d8 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2,9 +2,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean rat interval zmodp vector. -From mathcomp Require Import interval_inference fieldext falgebra. #[warning="-warn-library-file-internal-analysis"] -From mathcomp Require Import unstable. +From mathcomp Require Import mathcomp_extra unstable. From mathcomp Require Import boolp classical_sets filter functions cardinality. From mathcomp Require Import set_interval ereal reals topology real_interval. From mathcomp Require Import prodnormedzmodule tvs num_normedtype. @@ -365,6 +364,10 @@ Lemma normrZV (K : numDomainType) (V : normedModType K) (x : V) : `|x| \in GRing.unit -> `| `| x |^-1 *: x | = 1. Proof. by move=> nxu; rewrite normrZ normrV// normr_id mulVr. Qed. +HB.instance Definition _ (K : numDomainType) (V : normedModType K) := + Norm.isNorm.Build K V (@Num.norm K V) (normr0 V) + (@normr_ge0 _ V) (@normr0_eq0 _ V) (@ler_normD _ V) (@normrZ _ V). + Definition self_sub (K : numDomainType) (V W : normedModType K) (f : V -> W) (x : V * V) : W := f x.1 - f x.2. Arguments self_sub {K V W} f x /. @@ -2461,68 +2464,15 @@ Let V' := @fullv _ V. Variable B : (\dim V').-tuple V. Hypothesis Bbasis : basis_of V' B. -Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. - -Definition max_space : Type := (fun=> V) Bbasis. - -HB.instance Definition _ := Vector.on max_space. - -HB.instance Definition _ := Pointed.copy max_space V^o. - -Lemma max_norm_ge0 x : 0 <= max_norm x. -Proof. -rewrite /max_norm. -by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. -Qed. - -Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x. -Proof. -rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. -rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; - case: ifP => [/ltW|]// /negbT. -set b := (X in _ < X); have bR : b \is Num.real by exact: bigmax_real. -have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)). -by move=> /(le_trans IHl). -Qed. - -Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. -Proof. -apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. -by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. -Qed. - -Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0. -Proof. -move=> x0; rewrite (coord_basis Bbasis (memvf x)). -suff: forall i, coord B i x = 0. - by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. -by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. -Qed. - -Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. -Proof. -rewrite /max_norm. -under eq_bigr do rewrite linearZ normrZ/=. -elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. -by rewrite !big_cons IHl maxr_pMr. -Qed. - -Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. -Proof. by rewrite -scaler_nat max_normZ normr_nat mulr_natl. Qed. - -Lemma max_normN x : max_norm (- x) = max_norm x. -Proof. by rewrite -scaleN1r max_normZ normrN1 mul1r. Qed. - -HB.instance Definition _ := Num.Zmodule_isNormed.Build R - max_space ler_max_normD max_norm0_eq0 max_normMn max_normN. +HB.instance Definition _ := Pointed.copy (max_space Bbasis) V^o. HB.instance Definition _ := - PseudoMetric.copy max_space (pseudoMetric_normed max_space). + PseudoMetric.copy (max_space Bbasis) (pseudoMetric_normed (max_space Bbasis)). -HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R max_space erefl. +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space Bbasis) erefl. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R max_space max_normZ. + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) (max_normZ B). End InfiniteNorm. @@ -2554,23 +2504,16 @@ apply: (@continuous_compact _ _ f). exact: segment_compact. Qed. -Lemma equivalence_norms (N : V -> R) : - N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) -> - (forall x y, N (x + y) <= N x + N y) -> - (forall r x, N (r *: x) = `|r| * N x) -> +Lemma equivalence_norms (N : Norm.Norm.type V) : exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. Proof. -move=> N0 N_ge0 N0_eq0 ND NZ. set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. -have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0. -have N_sum (I : Type) (r : seq I) (F : I -> V) : - N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i). - by elim/big_ind2 : _ => *; rewrite ?N0// (le_trans (ND _ _))// lerD. +have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0. have leNoo (x : Voo) : N x <= M0 * `|x|. - rewrite [in leLHS](coord_vbasis (memvf (x : V))) (le_trans (N_sum _ _ _))//. + rewrite [in leLHS](coord_vbasis (memvf (x : V))). + rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//. rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _. - by rewrite NZ mulrC ler_pM// le_coord_max_norm. -have NZN a : N (- a) = N a by rewrite -scaleN1r NZ normrN1 mul1r. + by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0. have NC0 : continuous (N : Voo -> R). move=> /= x; rewrite /continuous_at. apply: cvg_zero; first exact: nbhs_filter. @@ -2580,8 +2523,8 @@ have NC0 : continuous (N : Voo -> R). rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//. apply/ler_normlP. have NB a b : N a <= N b + N (a - b). - by rewrite (le_trans _ (ND _ _)) ?subrKC. - by rewrite opprB !lerBlDl NB -opprB NZN NB. + by rewrite (le_trans _ (Norm.ler_normD _ _))// subrKC. + by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB. rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN. by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0]. have: compact [set x : Voo | `|x| = 1]. @@ -2597,20 +2540,23 @@ move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). move=> /= r /set_mem/= [y y1 <-]. apply: inv_continuous. - by apply: contra_eq_neq y1 => /N0_eq0 ->; rewrite normr0 eq_sym oner_eq0. + apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->. + by rewrite normr0 eq_sym oner_eq0. move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))). rewrite /globally/= => M1N. exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00. split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx. -have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0. +have [->|x0] := eqVneq x 0; first by rewrite normr0 Norm.norm0 mulr0. have Nx0 : 0 < N x. - by rewrite lt0r N_ge0 andbT; move: x0; apply: contra_neq => /N0_eq0. + rewrite lt0r Norm.norm_ge0 andbT. + by move: x0; apply: contra_neq => /Norm.norm0_eq0. have normx0 : 0 < `|x| by rewrite normr_gt0. move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[]. exists (N x / `|x|); last by rewrite invf_div. - exists (`|x|^-1 *: x); last by rewrite NZ mulrC ger0_norm. + exists (`|x|^-1 *: x); last by rewrite Norm.normZ mulrC ger0_norm. by rewrite normrZ normfV normr_id mulVf// gt_eqF. -rewrite ger0_norm ?divr_ge0// ler_pdivrMr// => /le_trans; apply. +rewrite ger0_norm; last by rewrite divr_ge0// Norm.norm_ge0. +rewrite ler_pdivrMr// => /le_trans; apply. by rewrite ler_pM2r// le_max lexx orbT. Unshelve. all: by end_near. Qed. @@ -2633,8 +2579,7 @@ apply: cvg_sum => i _. rewrite [X in _ --> X]linearZ/= -/B. apply: cvgZr_tmp. move: x; apply/linear_bounded_continuous/bounded_funP => r/=. -have [M M0 MP] := @equivalence_norms R V (@normr R V) (@normr0 _ _) - (@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _). +have [M M0 MP] := equivalence_norms (@Num.norm _ V). exists (M * r) => x. move: MP => /(_ x) [Mx _] xr. by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW. diff --git a/theories/normedtype_theory/tvs.v b/theories/normedtype_theory/tvs.v index 181d0108f..e5e0800b7 100644 --- a/theories/normedtype_theory/tvs.v +++ b/theories/normedtype_theory/tvs.v @@ -93,7 +93,7 @@ Lemma cvg_sum (T : Type) (U : TopologicalNmodule.type) (F : set_system T) \sum_(i <- r | P i) Ff i x @[x --> F] --> \sum_(i <- r| P i) Fa i. Proof. by move=> FF Ffa; apply: cvg_big => //; apply: add_continuous. Qed. -Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) +Lemma sum_continuous (T : topologicalType) (M : TopologicalNmodule.type) (I : Type) (r : seq I) (P : pred I) (F : I -> T -> M) : (forall i : I, P i -> continuous (F i)) -> continuous (fun x1 : T => \sum_(i <- r | P i) F i x1). @@ -101,9 +101,6 @@ Proof. by move=> FC0; apply: continuous_big => //; apply: add_continuous. Qed. End TopologicalNmodule_Theory. -HB.structure Definition PreTopologicalZmodule := - {M of Topological M & GRing.Zmodule M}. - HB.mixin Record TopologicalNmodule_isTopologicalZmodule M & Topological M & GRing.Zmodule M := { opp_continuous : continuous (-%R : M -> M) ; From 58ea15c54938cb845aa2a4b3a3d12c69e3d9914d Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Fri, 6 Mar 2026 14:20:41 +0100 Subject: [PATCH 4/7] review --- CHANGELOG_UNRELEASED.md | 3 +-- classical/unstable.v | 24 ++++++++++++++-------- theories/normedtype_theory/normed_module.v | 3 ++- 3 files changed, 19 insertions(+), 11 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c21ed28b5..9ffb6fc04 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -78,8 +78,7 @@ + structure `Norm` + lemmas `normMn`, `normN`, `ler_norm_sum` + definitions `max_norm`, `max_space` - + lemmas `max_norm_ge0`, `le_coord_max_norm`, `max_norm0`, `ler_max_normD`, - `max_norm0_eq0`, `max_normZ`, `max_normMn`, `max_normN` + + lemma `le_coord_max_norm` - in `normed_module.v`: + structure `NormedVector` diff --git a/classical/unstable.v b/classical/unstable.v index 4a653a76c..4b564e623 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -24,6 +24,11 @@ From mathcomp Require Import vector archimedean interval. (* the dependent sum *) (* prodA x := sends (X * Y) * Z to X * (Y * Z) *) (* prodAr x := sends X * (Y * Z) to (X * Y) * Z *) +(* max_norm x := maximum of the norms of the coordinates of the *) +(* vector x in a given basis. *) +(* max_space V := alias of the vectType V equipped with a *) +(* structure of normed Z-module, where the norm is *) +(* max_norm. *) (* ``` *) (* *) (******************************************************************************) @@ -594,6 +599,9 @@ Proof. exact: real_ltr_bound. Qed. Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R. Proof. exact: real_ltrNbound. Qed. +(* normedZmodType provide norms but the subject is not the norm. We define here + a structure of norm where the subject is the function from the left-module to + its scalar field. *) Module Norm. HB.mixin Record isNorm (K : numDomainType) (L : lmodType K) (norm : L -> K) := { @@ -618,7 +626,7 @@ Lemma normN x : norm (- x) = norm x. Proof. by rewrite -scaleN1r normZ normrN1 mul1r. Qed. Lemma ler_norm_sum (I : Type) (r : seq I) (F : I -> L) : - norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i). + norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i). Proof. by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD. Qed. @@ -642,7 +650,7 @@ Definition max_space : Type := (fun=> V) Bbasis. HB.instance Definition _ := Vector.on max_space. -Lemma max_norm_ge0 x : 0 <= max_norm x. +Let max_norm_ge0 x : 0 <= max_norm x. Proof. rewrite /max_norm. by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. @@ -659,7 +667,7 @@ have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)). by move=> /(le_trans IHl). Qed. -Lemma max_norm0 : max_norm 0 = 0. +Let max_norm0 : max_norm 0 = 0. Proof. apply: le_anti; rewrite max_norm_ge0 andbT. apply: bigmax_le => // i _. @@ -669,13 +677,13 @@ have <-: \sum_(i < \dim V') 0 *: B`_i = 0. by rewrite coord_sum_free ?normr0// (basis_free Bbasis). Qed. -Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. +Let ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. Proof. apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. Qed. -Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0. +Let max_norm0_eq0 x : max_norm x = 0 -> x = 0. Proof. move=> x0; rewrite (coord_basis Bbasis (memvf x)). suff: forall i, coord B i x = 0. @@ -683,7 +691,7 @@ suff: forall i, coord B i x = 0. by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. Qed. -Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. +Let max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. Proof. rewrite /max_norm. under eq_bigr do rewrite linearZ/= normrM. @@ -694,10 +702,10 @@ Qed. HB.instance Definition _ := Norm.isNorm.Build K V max_norm max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ. -Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. +Let max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. Proof. exact: Norm.Theory.normMn. Qed. -Lemma max_normN x : max_norm (- x) = max_norm x. +Let max_normN x : max_norm (- x) = max_norm x. Proof. exact: Norm.Theory.normN. Qed. HB.instance Definition _ := Num.Zmodule_isNormed.Build K diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 7c320f4d8..12a4584fb 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2472,7 +2472,8 @@ HB.instance Definition _ := HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space Bbasis) erefl. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) (max_normZ B). + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) + (@Norm.normZ _ _ (unstable_max_norm__canonical__Norm_Norm Bbasis)). End InfiniteNorm. From bb7ab144c7412a8a7f47e1a279eed93dc8660741 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Mon, 16 Mar 2026 16:58:18 +0100 Subject: [PATCH 5/7] optimize max_norm --- classical/unstable.v | 23 ++++++++------- theories/normedtype_theory/normed_module.v | 34 ++++++++++------------ 2 files changed, 28 insertions(+), 29 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 4b564e623..71e8909d8 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -640,30 +640,29 @@ Export Norm.Exports. Section InfiniteNorm. Variables (K : numFieldType) (V : vectType K). -Let V' := @fullv _ V. -Variable B : (\dim V').-tuple V. -Hypothesis Bbasis : basis_of V' B. -Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. +Definition max_norm x : K := \big[Order.max/0]_(i < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|. -Definition max_space : Type := (fun=> V) Bbasis. +Definition max_space : Type := V. HB.instance Definition _ := Vector.on max_space. +Check erefl: (max_space : vectType _) = V. + Let max_norm_ge0 x : 0 <= max_norm x. Proof. rewrite /max_norm. by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. Qed. -Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x. +Lemma le_coord_max_norm x i : `|coord (vbasis fullv) i x| <= max_norm x :> K. Proof. rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; case: ifP => [/ltW|]// /negbT. set b := (X in _ < X). have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real. -have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)). +have /comparable_leNgt <- := real_comparable bR (normr_real (coord (vbasis fullv) j x)). by move=> /(le_trans IHl). Qed. @@ -671,10 +670,10 @@ Let max_norm0 : max_norm 0 = 0. Proof. apply: le_anti; rewrite max_norm_ge0 andbT. apply: bigmax_le => // i _. -have <-: \sum_(i < \dim V') 0 *: B`_i = 0. +have <-: \sum_(i < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0. under eq_bigr do rewrite scale0r. by rewrite sumr_const mul0rn. -by rewrite coord_sum_free ?normr0// (basis_free Bbasis). +by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)). Qed. Let ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. @@ -685,8 +684,8 @@ Qed. Let max_norm0_eq0 x : max_norm x = 0 -> x = 0. Proof. -move=> x0; rewrite (coord_basis Bbasis (memvf x)). -suff: forall i, coord B i x = 0. +move=> x0; rewrite (coord_vbasis (memvf x)). +suff: forall i, coord (vbasis fullv) i x = 0. by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. Qed. @@ -712,3 +711,5 @@ HB.instance Definition _ := Num.Zmodule_isNormed.Build K max_space ler_max_normD max_norm0_eq0 max_normMn max_normN. End InfiniteNorm. + +Set Printing All. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 12a4584fb..fbca3c94c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2460,27 +2460,23 @@ End open_set_disjoint_real_intervals. Section InfiniteNorm. Variables (R : numFieldType) (V : vectType R). -Let V' := @fullv _ V. -Variable B : (\dim V').-tuple V. -Hypothesis Bbasis : basis_of V' B. -HB.instance Definition _ := Pointed.copy (max_space Bbasis) V^o. +HB.instance Definition _ := Pointed.copy (max_space V) V^o. HB.instance Definition _ := - PseudoMetric.copy (max_space Bbasis) (pseudoMetric_normed (max_space Bbasis)). + PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)). -HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space Bbasis) erefl. +HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl. HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) - (@Norm.normZ _ _ (unstable_max_norm__canonical__Norm_Norm Bbasis)). + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) + (@Norm.normZ _ _ (@max_norm _ V)). End InfiniteNorm. Section EquivalenceNorms. Variables (R : realType) (V : vectType R). -Let V' := @fullv _ V. -Let Voo := max_space (vbasisP (@fullv _ V)). +Let Voo := max_space V. (* N.B. Get Trocq to prove the continuity part automatically. *) Lemma sup_closed_ball_compact : compact (closed_ball (0 : Voo) 1). @@ -2488,27 +2484,29 @@ Proof. rewrite closed_ballE// /closed_ball_. under eq_set do rewrite sub0r normrN. rewrite -[forall x, _]/(compact _). -pose f (X : {ptws 'I_(\dim V') -> R}) : Voo := - \sum_(i < \dim V') X i *: (vbasis V')`_i. +pose f (X : {ptws 'I_(\dim (@fullv _ V)) -> R}) : V := + \sum_(i < \dim (@fullv _ V)) X i *: (vbasis fullv)`_i. have -> : [set x : Voo | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. apply/seteqP; split=> [x/= x1|x/= [X X1 <-]]. - - exists (coord (vbasis V') ^~ x); last first. - exact/esym/(@coord_vbasis _ _ (x : V))/memvf. + (* FIXME: The type annotation on x is mandatory, otherwise we try to unify V + with its eta-expansion. *) + - exists (coord (vbasis fullv) ^~ (x : V)); last first. + exact/esym/coord_vbasis/memvf. by move=> i; rewrite in_itv/= -ler_norml (le_trans _ x1)// le_coord_max_norm. - rewrite /normr/= /max_norm bigmax_le => //= i _. by rewrite coord_sum_free ?ler_norml; [exact: X1|exact/basis_free/vbasisP]. -apply: (@continuous_compact _ _ f). +apply (@continuous_compact _ _ (f : _ -> Voo)). - apply/continuous_subspaceT/sum_continuous => /= i _ x. exact/continuousZr_tmp/proj_continuous. -- apply: (@tychonoff 'I_(\dim V') (fun=> R^o) (fun=> `[-1, 1]%classic)) => _. +- apply: (@tychonoff 'I_(\dim (@fullv _ V)) (fun=> R^o) (fun=> `[-1, 1]%classic)) => _. exact: segment_compact. Qed. Lemma equivalence_norms (N : Norm.Norm.type V) : exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. Proof. -set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i. +set M0 := 1 + \sum_(i < \dim (@fullv _ V)) N (vbasis fullv)`_i. have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0. have leNoo (x : Voo) : N x <= M0 * `|x|. rewrite [in leLHS](coord_vbasis (memvf (x : V))). @@ -2583,7 +2581,7 @@ move: x; apply/linear_bounded_continuous/bounded_funP => r/=. have [M M0 MP] := equivalence_norms (@Num.norm _ V). exists (M * r) => x. move: MP => /(_ x) [Mx _] xr. -by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW. +by rewrite (le_trans (le_coord_max_norm _ _))// (le_trans Mx) ?ler_wpM2l// ltW. Qed. End LinearContinuous. From e75500a6f41aab64fcacc2daea650bfd9e5e8a30 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 19 Mar 2026 16:06:07 +0100 Subject: [PATCH 6/7] stop exposing max_space and max_norm --- CHANGELOG_UNRELEASED.md | 2 - classical/unstable.v | 76 ------------ theories/normedtype_theory/normed_module.v | 132 ++++++++++++++++----- 3 files changed, 100 insertions(+), 110 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9ffb6fc04..acf2f0642 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,8 +77,6 @@ - in `unstable.v`: + structure `Norm` + lemmas `normMn`, `normN`, `ler_norm_sum` - + definitions `max_norm`, `max_space` - + lemma `le_coord_max_norm` - in `normed_module.v`: + structure `NormedVector` diff --git a/classical/unstable.v b/classical/unstable.v index 71e8909d8..66601ea7c 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -637,79 +637,3 @@ End Theory. Module Import Exports. HB.reexport. End Exports. End Norm. Export Norm.Exports. - -Section InfiniteNorm. -Variables (K : numFieldType) (V : vectType K). - -Definition max_norm x : K := \big[Order.max/0]_(i < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|. - -Definition max_space : Type := V. - -HB.instance Definition _ := Vector.on max_space. - -Check erefl: (max_space : vectType _) = V. - -Let max_norm_ge0 x : 0 <= max_norm x. -Proof. -rewrite /max_norm. -by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. -Qed. - -Lemma le_coord_max_norm x i : `|coord (vbasis fullv) i x| <= max_norm x :> K. -Proof. -rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. -rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; - case: ifP => [/ltW|]// /negbT. -set b := (X in _ < X). -have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real. -have /comparable_leNgt <- := real_comparable bR (normr_real (coord (vbasis fullv) j x)). -by move=> /(le_trans IHl). -Qed. - -Let max_norm0 : max_norm 0 = 0. -Proof. -apply: le_anti; rewrite max_norm_ge0 andbT. -apply: bigmax_le => // i _. -have <-: \sum_(i < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0. - under eq_bigr do rewrite scale0r. - by rewrite sumr_const mul0rn. -by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)). -Qed. - -Let ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y. -Proof. -apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. -by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. -Qed. - -Let max_norm0_eq0 x : max_norm x = 0 -> x = 0. -Proof. -move=> x0; rewrite (coord_vbasis (memvf x)). -suff: forall i, coord (vbasis fullv) i x = 0. - by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. -by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. -Qed. - -Let max_normZ r x : max_norm (r *: x) = `|r| * max_norm x. -Proof. -rewrite /max_norm. -under eq_bigr do rewrite linearZ/= normrM. -elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. -by rewrite !big_cons IHl maxr_pMr. -Qed. - -HB.instance Definition _ := Norm.isNorm.Build K V max_norm - max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ. - -Let max_normMn x n : max_norm (x *+ n) = max_norm x *+ n. -Proof. exact: Norm.Theory.normMn. Qed. - -Let max_normN x : max_norm (- x) = max_norm x. -Proof. exact: Norm.Theory.normN. Qed. - -HB.instance Definition _ := Num.Zmodule_isNormed.Build K - max_space ler_max_normD max_norm0_eq0 max_normMn max_normN. - -End InfiniteNorm. - -Set Printing All. diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index fbca3c94c..50a171b3c 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2458,35 +2458,100 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed. End open_set_disjoint_real_intervals. -Section InfiniteNorm. -Variables (R : numFieldType) (V : vectType R). +Section EquivalenceNorms. +Variables (R : realType). -HB.instance Definition _ := Pointed.copy (max_space V) V^o. +(* FIXME: Specialize to vector space with basis and expose this definition + (see https://github.com/math-comp/analysis/issues/1911). + It will also be possible to generalize to `numFieldType`. *) +Let max_norm (V : vectType R) x : R := \big[Order.max/0]_(i < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|. -HB.instance Definition _ := - PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)). +Definition max_space (V : vectType R) : Type := V. -HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl. +HB.instance Definition _ (V : vectType R) := Vector.on (max_space V). -HB.instance Definition _ := - PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) - (@Norm.normZ _ _ (@max_norm _ V)). +HB.instance Definition _ (V : vectType R) := Pointed.copy (max_space V) V^o. -End InfiniteNorm. +Let max_norm_ge0 (V : vectType R) (x : V) : 0 <= max_norm x. +Proof. +rewrite /max_norm. +by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP. +Qed. -Section EquivalenceNorms. -Variables (R : realType) (V : vectType R). -Let Voo := max_space V. +(* FIXME: expose. *) +Let le_coord_max_norm (V : vectType R) (x : V) i : `|coord (vbasis fullv) i x| <= max_norm x :> R. +Proof. +rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl. +rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl]; + case: ifP => [/ltW|]// /negbT. +set b := (X in _ < X). +have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real. +have /comparable_leNgt <- := real_comparable bR (normr_real (coord (vbasis fullv) j x)). +by move=> /(le_trans IHl). +Qed. + +Let max_norm0 (V : vectType R) : @max_norm V 0 = 0. +Proof. +apply: le_anti; rewrite max_norm_ge0 andbT. +apply: bigmax_le => // i _. +have <-: \sum_(i < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0. + under eq_bigr do rewrite scale0r. + by rewrite sumr_const mul0rn. +by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)). +Qed. + +Let ler_max_normD (V : vectType R) (x y : V) : max_norm (x + y) <= max_norm x + max_norm y. +Proof. +apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0. +by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm. +Qed. + +Let max_norm0_eq0 (V : vectType R) (x : V) : max_norm x = 0 -> x = 0. +Proof. +move=> x0; rewrite (coord_vbasis (memvf x)). +suff: forall i, coord (vbasis fullv) i x = 0. + by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r. +by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm. +Qed. + +Let max_normZ (V : vectType R) r (x : V) : max_norm (r *: x) = `|r| * max_norm x. +Proof. +rewrite /max_norm. +under eq_bigr do rewrite linearZ/= normrM. +elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0. +by rewrite !big_cons IHl maxr_pMr. +Qed. + +HB.instance Definition _ (V : vectType R) := Norm.isNorm.Build R V (@max_norm V) + (max_norm0 V) (@max_norm_ge0 V) (@max_norm0_eq0 V) (@ler_max_normD V) (@max_normZ V). + +Let max_normMn (V : vectType R) (x : V) n : max_norm (x *+ n) = max_norm x *+ n. +Proof. exact: (Norm.Theory.normMn (@normed_module_max_norm__canonical__Norm_Norm V)). Qed. + +Let max_normN (V : vectType R) (x : V) : max_norm (- x) = max_norm x. +Proof. exact: (Norm.Theory.normN (@normed_module_max_norm__canonical__Norm_Norm V)). Qed. + +HB.instance Definition _ (V : vectType R) := Num.Zmodule_isNormed.Build R + (max_space V) (@ler_max_normD V) (@max_norm0_eq0 V) (@max_normMn V) (@max_normN V). + +HB.instance Definition _ (V : vectType R) := + PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)). + +HB.instance Definition _ (V : vectType R) := NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl. + +HB.instance Definition _ (V : vectType R) := + PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V) + (@Norm.normZ _ _ (@max_norm V)). (* N.B. Get Trocq to prove the continuity part automatically. *) -Lemma sup_closed_ball_compact : compact (closed_ball (0 : Voo) 1). +Lemma sup_closed_ball_compact (V : vectType R) : compact (closed_ball (0 : max_space V) 1). Proof. rewrite closed_ballE// /closed_ball_. under eq_set do rewrite sub0r normrN. rewrite -[forall x, _]/(compact _). pose f (X : {ptws 'I_(\dim (@fullv _ V)) -> R}) : V := \sum_(i < \dim (@fullv _ V)) X i *: (vbasis fullv)`_i. -have -> : [set x : Voo | `|x| <= 1] = +have -> : [set x : max_space V | `|x| <= 1] = f @` [set X | forall i, `[-1, 1]%classic (X i)]. apply/seteqP; split=> [x/= x1|x/= [X X1 <-]]. (* FIXME: The type annotation on x is mandatory, otherwise we try to unify V @@ -2496,24 +2561,32 @@ have -> : [set x : Voo | `|x| <= 1] = by move=> i; rewrite in_itv/= -ler_norml (le_trans _ x1)// le_coord_max_norm. - rewrite /normr/= /max_norm bigmax_le => //= i _. by rewrite coord_sum_free ?ler_norml; [exact: X1|exact/basis_free/vbasisP]. -apply (@continuous_compact _ _ (f : _ -> Voo)). +apply (@continuous_compact _ _ (f : _ -> max_space V)). - apply/continuous_subspaceT/sum_continuous => /= i _ x. exact/continuousZr_tmp/proj_continuous. - apply: (@tychonoff 'I_(\dim (@fullv _ V)) (fun=> R^o) (fun=> `[-1, 1]%classic)) => _. exact: segment_compact. Qed. -Lemma equivalence_norms (N : Norm.Norm.type V) : - exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|. +Lemma equivalence_norms (V : vectType R) (N N' : Norm.Norm.type V) : + exists2 M, 0 < M & forall x : max_space V, N' x <= M * N x /\ N x <= M * N' x. Proof. +suff: forall (N : Norm.Norm.type V), + exists2 M, 0 < M & forall x : max_space V, `|x| <= M * N x /\ N x <= M * `|x|. + move=> /[dup] /(_ N) []/= M M0 Noo /(_ N') []/= M' M'0 N'oo. + exists (M * M') => [|x]; first exact: mulr_gt0. + move: Noo N'oo => /(_ x) [] Nge Nle /(_ x) [] N'ge N'le. + split; first by apply: (le_trans N'le); rewrite mulrAC mulrC ler_pM2r. + by apply: (le_trans Nle); rewrite -mulrA ler_pM2l. +move=> {N'}N. set M0 := 1 + \sum_(i < \dim (@fullv _ V)) N (vbasis fullv)`_i. have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0. -have leNoo (x : Voo) : N x <= M0 * `|x|. +have leNoo (x : max_space V) : N x <= M0 * `|x|. rewrite [in leLHS](coord_vbasis (memvf (x : V))). rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//. rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _. by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0. -have NC0 : continuous (N : Voo -> R). +have NC0 : continuous (N : max_space V -> R). move=> /= x; rewrite /continuous_at. apply: cvg_zero; first exact: nbhs_filter. apply/cvgr0Pnorm_le; first exact: nbhs_filter. @@ -2526,17 +2599,17 @@ have NC0 : continuous (N : Voo -> R). by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB. rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN. by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0]. -have: compact [set x : Voo | `|x| = 1]. - apply: (subclosed_compact _ sup_closed_ball_compact). +have: compact [set x : max_space V | `|x| = 1]. + apply: (subclosed_compact _ (@sup_closed_ball_compact V)). - apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq. by move=> *; exact: norm_continuous. - by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->. -move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[]. +move=> /(@continuous_compact _ _ (N : max_space V -> R)) -/(_ _)/wrap[]. exact: continuous_subspaceT. move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[]. move=> /= x; rewrite /continuous_at. apply: (@continuous_in_subspaceT _ _ - [set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)). + [set N x | x in [set x : max_space V | `|x| = 1]] (@GRing.inv R)). move=> /= r /set_mem/= [y y1 <-]. apply: inv_continuous. apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->. @@ -2559,12 +2632,7 @@ rewrite ler_pdivrMr// => /le_trans; apply. by rewrite ler_pM2r// le_max lexx orbT. Unshelve. all: by end_near. Qed. -End EquivalenceNorms. - -Section LinearContinuous. -Variables (R : realType) (V : normedVectType R) (W : normedModType R). - -Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f. +Lemma linear_findim_continuous (V : normedVectType R) (W : normedModType R) (f : {linear V -> W}) : continuous f. Proof. set V' := @fullv _ V. set B := vbasis V'. @@ -2578,10 +2646,10 @@ apply: cvg_sum => i _. rewrite [X in _ --> X]linearZ/= -/B. apply: cvgZr_tmp. move: x; apply/linear_bounded_continuous/bounded_funP => r/=. -have [M M0 MP] := equivalence_norms (@Num.norm _ V). +have [M M0 MP] := equivalence_norms (@Num.norm _ V) (@max_norm V). exists (M * r) => x. move: MP => /(_ x) [Mx _] xr. by rewrite (le_trans (le_coord_max_norm _ _))// (le_trans Mx) ?ler_wpM2l// ltW. Qed. -End LinearContinuous. +End EquivalenceNorms. From f46d3ba71dfa6d84c96ea89b2c4a07c9706f5036 Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 19 Mar 2026 16:13:30 +0100 Subject: [PATCH 7/7] fix header comment --- classical/unstable.v | 5 ----- 1 file changed, 5 deletions(-) diff --git a/classical/unstable.v b/classical/unstable.v index 66601ea7c..3a3fe719c 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -24,11 +24,6 @@ From mathcomp Require Import vector archimedean interval. (* the dependent sum *) (* prodA x := sends (X * Y) * Z to X * (Y * Z) *) (* prodAr x := sends X * (Y * Z) to (X * Y) * Z *) -(* max_norm x := maximum of the norms of the coordinates of the *) -(* vector x in a given basis. *) -(* max_space V := alias of the vectType V equipped with a *) -(* structure of normed Z-module, where the norm is *) -(* max_norm. *) (* ``` *) (* *) (******************************************************************************)