Skip to content

Commit 7e2ec42

Browse files
TragicusCohenCyril
Tragicus
authored and
CohenCyril
committed
norm interface
1 parent e373441 commit 7e2ec42

3 files changed

Lines changed: 147 additions & 84 deletions

File tree

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -63,12 +63,18 @@
6363
- in `tvs.v`
6464
+ lemmas `cvg_sum`, `sum_continuous`
6565

66+
- in `unstable.v`:
67+
+ structure `Norm`
68+
+ lemmas `normMn`, `normN`, `ler_norm_sum`
69+
+ definitions `max_norm`, `max_space`
70+
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `max_norm0`, `ler_max_normD`,
71+
`max_norm0_eq0`, `max_normZ`, `max_normMn`, `max_normN`
72+
6673
- in `normed_module.v`:
6774
+ structure `NormedVector`
68-
+ definitions `normedVectType`, `max_norm`, `max_space`
69-
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `ler_max_normD`, `max_norm0_eq0`,
70-
`max_normZ`, `max_normMn`, `max_normN`, `sup_closed_ball_compact`,
71-
`equivalence_norms`, `linear_findim_continuous`
75+
+ definition `normedVectType`
76+
+ lemmas `sup_closed_ball_compact`, `equivalence_norms`,
77+
`linear_findim_continuous`
7278

7379
### Changed
7480
- in `set_interval.v`

‎classical/unstable.v‎

Lines changed: 113 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *)
2-
From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
2+
From HB Require Import structures.
3+
From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint vector.
34
From mathcomp Require Import archimedean interval.
45

56
(**md**************************************************************************)
@@ -591,3 +592,114 @@ Proof. exact: real_ltr_bound. Qed.
591592

592593
Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R.
593594
Proof. exact: real_ltrNbound. Qed.
595+
596+
Module Norm.
597+
598+
HB.mixin Record isNorm (K : numDomainType) (L : lmodType K) (norm : L -> K) := {
599+
norm0 : norm 0 = 0;
600+
norm_ge0 : forall x, 0 <= norm x;
601+
norm0_eq0 : forall x, norm x = 0 -> x = 0;
602+
ler_normD : forall x y, norm (x + y) <= norm x + norm y;
603+
normZ : forall r x, norm (r *: x) = `|r| * norm x;
604+
}.
605+
606+
#[export]
607+
HB.structure Definition Norm K L := { norm of @isNorm K L norm }.
608+
609+
Module Import Theory.
610+
Section Theory.
611+
Variables (K : numDomainType) (L : lmodType K) (norm : Norm.type L).
612+
613+
Lemma normMn x n : norm (x *+ n) = norm x *+ n.
614+
Proof. by rewrite -scaler_nat normZ normr_nat mulr_natl. Qed.
615+
616+
Lemma normN x : norm (- x) = norm x.
617+
Proof. by rewrite -scaleN1r normZ normrN1 mul1r. Qed.
618+
619+
Lemma ler_norm_sum (I : Type) (r : seq I) (F : I -> L) :
620+
norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i).
621+
Proof.
622+
by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD.
623+
Qed.
624+
625+
End Theory.
626+
End Theory.
627+
628+
Module Import Exports. HB.reexport. End Exports.
629+
End Norm.
630+
Export Norm.Exports.
631+
632+
Section InfiniteNorm.
633+
Variables (K : numFieldType) (V : vectType K).
634+
Let V' := @fullv _ V.
635+
Variable B : (\dim V').-tuple V.
636+
Hypothesis Bbasis : basis_of V' B.
637+
638+
Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|.
639+
640+
Definition max_space : Type := (fun=> V) Bbasis.
641+
642+
HB.instance Definition _ := Vector.on max_space.
643+
644+
Lemma max_norm_ge0 x : 0 <= max_norm x.
645+
Proof.
646+
rewrite /max_norm.
647+
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
648+
Qed.
649+
650+
Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x.
651+
Proof.
652+
rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
653+
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
654+
case: ifP => [/ltW|]// /negbT.
655+
set b := (X in _ < X).
656+
have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real.
657+
have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)).
658+
by move=> /(le_trans IHl).
659+
Qed.
660+
661+
Lemma max_norm0 : max_norm 0 = 0.
662+
Proof.
663+
apply: le_anti; rewrite max_norm_ge0 andbT.
664+
apply: bigmax_le => // i _.
665+
have <-: \sum_(i < \dim V') 0 *: B`_i = 0.
666+
under eq_bigr do rewrite scale0r.
667+
by rewrite sumr_const mul0rn.
668+
by rewrite coord_sum_free ?normr0// (basis_free Bbasis).
669+
Qed.
670+
671+
Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y.
672+
Proof.
673+
apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
674+
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
675+
Qed.
676+
677+
Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0.
678+
Proof.
679+
move=> x0; rewrite (coord_basis Bbasis (memvf x)).
680+
suff: forall i, coord B i x = 0.
681+
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
682+
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
683+
Qed.
684+
685+
Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x.
686+
Proof.
687+
rewrite /max_norm.
688+
under eq_bigr do rewrite linearZ/= normrM.
689+
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
690+
by rewrite !big_cons IHl maxr_pMr.
691+
Qed.
692+
693+
HB.instance Definition _ := Norm.isNorm.Build K V max_norm
694+
max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ.
695+
696+
Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n.
697+
Proof. exact: Norm.Theory.normMn. Qed.
698+
699+
Lemma max_normN x : max_norm (- x) = max_norm x.
700+
Proof. exact: Norm.Theory.normN. Qed.
701+
702+
HB.instance Definition _ := Num.Zmodule_isNormed.Build K
703+
max_space ler_max_normD max_norm0_eq0 max_normMn max_normN.
704+
705+
End InfiniteNorm.

‎theories/normedtype_theory/normed_module.v‎

Lines changed: 24 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
From HB Require Import structures.
33
From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint.
44
From mathcomp Require Import archimedean rat interval zmodp vector.
5-
From mathcomp Require Import fieldext falgebra.
5+
From mathcomp Require Import fieldext falgebra mathcomp_extra.
66
#[warning="-warn-library-file-internal-analysis"]
77
From mathcomp Require Import unstable.
88
From mathcomp Require Import boolp classical_sets filter functions cardinality.
@@ -397,6 +397,9 @@ Unshelve. all: by end_near. Qed.
397397
Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
398398
Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
399399

400+
HB.instance Definition _ := Norm.isNorm.Build K V (@Num.norm K V) (normr0 V)
401+
(@normr_ge0 _ V) (@normr0_eq0 _ V) (@ler_normD _ V) (@normrZ _ V).
402+
400403
End NormedModule_numDomainType.
401404

402405
Definition self_sub (K : numDomainType) (V W : normedModType K)
@@ -2493,68 +2496,15 @@ Let V' := @fullv _ V.
24932496
Variable B : (\dim V').-tuple V.
24942497
Hypothesis Bbasis : basis_of V' B.
24952498

2496-
Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|.
2497-
2498-
Definition max_space : Type := (fun=> V) Bbasis.
2499-
2500-
HB.instance Definition _ := Vector.on max_space.
2501-
2502-
HB.instance Definition _ := Pointed.copy max_space V^o.
2503-
2504-
Lemma max_norm_ge0 x : 0 <= max_norm x.
2505-
Proof.
2506-
rewrite /max_norm.
2507-
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
2508-
Qed.
2509-
2510-
Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x.
2511-
Proof.
2512-
rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
2513-
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
2514-
case: ifP => [/ltW|]// /negbT.
2515-
set b := (X in _ < X); have bR : b \is Num.real by exact: bigmax_real.
2516-
have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)).
2517-
by move=> /(le_trans IHl).
2518-
Qed.
2519-
2520-
Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y.
2521-
Proof.
2522-
apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
2523-
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
2524-
Qed.
2525-
2526-
Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0.
2527-
Proof.
2528-
move=> x0; rewrite (coord_basis Bbasis (memvf x)).
2529-
suff: forall i, coord B i x = 0.
2530-
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
2531-
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
2532-
Qed.
2533-
2534-
Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x.
2535-
Proof.
2536-
rewrite /max_norm.
2537-
under eq_bigr do rewrite linearZ normrZ/=.
2538-
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
2539-
by rewrite !big_cons IHl maxr_pMr.
2540-
Qed.
2541-
2542-
Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n.
2543-
Proof. by rewrite -scaler_nat max_normZ normr_nat mulr_natl. Qed.
2544-
2545-
Lemma max_normN x : max_norm (- x) = max_norm x.
2546-
Proof. by rewrite -scaleN1r max_normZ normrN1 mul1r. Qed.
2547-
2548-
HB.instance Definition _ := Num.Zmodule_isNormed.Build R
2549-
max_space ler_max_normD max_norm0_eq0 max_normMn max_normN.
2499+
HB.instance Definition _ := Pointed.copy (max_space Bbasis) V^o.
25502500

25512501
HB.instance Definition _ :=
2552-
PseudoMetric.copy max_space (pseudoMetric_normed max_space).
2502+
PseudoMetric.copy (max_space Bbasis) (pseudoMetric_normed (max_space Bbasis)).
25532503

2554-
HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R max_space erefl.
2504+
HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space Bbasis) erefl.
25552505

25562506
HB.instance Definition _ :=
2557-
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R max_space max_normZ.
2507+
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) (max_normZ B).
25582508

25592509
End InfiniteNorm.
25602510

@@ -2586,23 +2536,16 @@ apply: (@continuous_compact _ _ f).
25862536
exact: segment_compact.
25872537
Qed.
25882538

2589-
Lemma equivalence_norms (N : V -> R) :
2590-
N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) ->
2591-
(forall x y, N (x + y) <= N x + N y) ->
2592-
(forall r x, N (r *: x) = `|r| * N x) ->
2539+
Lemma equivalence_norms (N : Norm.Norm.type V) :
25932540
exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|.
25942541
Proof.
2595-
move=> N0 N_ge0 N0_eq0 ND NZ.
25962542
set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i.
2597-
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0.
2598-
have N_sum (I : Type) (r : seq I) (F : I -> V) :
2599-
N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i).
2600-
by elim/big_ind2 : _ => *; rewrite ?N0// (le_trans (ND _ _))// lerD.
2543+
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0.
26012544
have leNoo (x : Voo) : N x <= M0 * `|x|.
2602-
rewrite [in leLHS](coord_vbasis (memvf (x : V))) (le_trans (N_sum _ _ _))//.
2545+
rewrite [in leLHS](coord_vbasis (memvf (x : V))).
2546+
rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//.
26032547
rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _.
2604-
by rewrite NZ mulrC ler_pM// le_coord_max_norm.
2605-
have NZN a : N (- a) = N a by rewrite -scaleN1r NZ normrN1 mul1r.
2548+
by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0.
26062549
have NC0 : continuous (N : Voo -> R).
26072550
move=> /= x; rewrite /continuous_at.
26082551
apply: cvg_zero; first exact: nbhs_filter.
@@ -2612,8 +2555,8 @@ have NC0 : continuous (N : Voo -> R).
26122555
rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//.
26132556
apply/ler_normlP.
26142557
have NB a b : N a <= N b + N (a - b).
2615-
by rewrite (le_trans _ (ND _ _)) ?subrKC.
2616-
by rewrite opprB !lerBlDl NB -opprB NZN NB.
2558+
by rewrite (le_trans _ (Norm.ler_normD _ _))// subrKC.
2559+
by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB.
26172560
rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN.
26182561
by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
26192562
have: compact [set x : Voo | `|x| = 1].
@@ -2629,20 +2572,23 @@ move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
26292572
[set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)).
26302573
move=> /= r /set_mem/= [y y1 <-].
26312574
apply: inv_continuous.
2632-
by apply: contra_eq_neq y1 => /N0_eq0 ->; rewrite normr0 eq_sym oner_eq0.
2575+
apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->.
2576+
by rewrite normr0 eq_sym oner_eq0.
26332577
move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))).
26342578
rewrite /globally/= => M1N.
26352579
exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00.
26362580
split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx.
2637-
have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0.
2581+
have [->|x0] := eqVneq x 0; first by rewrite normr0 Norm.norm0 mulr0.
26382582
have Nx0 : 0 < N x.
2639-
by rewrite lt0r N_ge0 andbT; move: x0; apply: contra_neq => /N0_eq0.
2583+
rewrite lt0r Norm.norm_ge0 andbT.
2584+
by move: x0; apply: contra_neq => /Norm.norm0_eq0.
26402585
have normx0 : 0 < `|x| by rewrite normr_gt0.
26412586
move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[].
26422587
exists (N x / `|x|); last by rewrite invf_div.
2643-
exists (`|x|^-1 *: x); last by rewrite NZ mulrC ger0_norm.
2588+
exists (`|x|^-1 *: x); last by rewrite Norm.normZ mulrC ger0_norm.
26442589
by rewrite normrZ normfV normr_id mulVf// gt_eqF.
2645-
rewrite ger0_norm ?divr_ge0// ler_pdivrMr// => /le_trans; apply.
2590+
rewrite ger0_norm; last by rewrite divr_ge0// Norm.norm_ge0.
2591+
rewrite ler_pdivrMr// => /le_trans; apply.
26462592
by rewrite ler_pM2r// le_max lexx orbT.
26472593
Unshelve. all: by end_near. Qed.
26482594

@@ -2665,8 +2611,7 @@ apply: cvg_sum => i _.
26652611
rewrite [X in _ --> X]linearZ/= -/B.
26662612
apply: cvgZr_tmp.
26672613
move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
2668-
have [M M0 MP] := @equivalence_norms R V (@normr R V) (@normr0 _ _)
2669-
(@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _).
2614+
have [M M0 MP] := equivalence_norms (@Num.norm _ V).
26702615
exists (M * r) => x.
26712616
move: MP => /(_ x) [Mx _] xr.
26722617
by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW.

0 commit comments

Comments
 (0)