Skip to content

Commit ea91b3d

Browse files
TragicusTragicus
committed
norm interface
1 parent 006af99 commit ea91b3d

3 files changed

Lines changed: 147 additions & 85 deletions

File tree

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -72,12 +72,18 @@
7272
- in `tvs.v`
7373
+ lemmas `cvg_sum`, `sum_continuous`
7474

75+
- in `unstable.v`:
76+
+ structure `Norm`
77+
+ lemmas `normMn`, `normN`, `ler_norm_sum`
78+
+ definitions `max_norm`, `max_space`
79+
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `max_norm0`, `ler_max_normD`,
80+
`max_norm0_eq0`, `max_normZ`, `max_normMn`, `max_normN`
81+
7582
- in `normed_module.v`:
7683
+ structure `NormedVector`
77-
+ definitions `normedVectType`, `max_norm`, `max_space`
78-
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `ler_max_normD`, `max_norm0_eq0`,
79-
`max_normZ`, `max_normMn`, `max_normN`, `sup_closed_ball_compact`,
80-
`equivalence_norms`, `linear_findim_continuous`
84+
+ definition `normedVectType`
85+
+ lemmas `sup_closed_ball_compact`, `equivalence_norms`,
86+
`linear_findim_continuous`
8187

8288
### Changed
8389

‎classical/unstable.v‎

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

56
(**md**************************************************************************)
67
(* # MathComp extra *)
@@ -592,3 +593,114 @@ Proof. exact: real_ltr_bound. Qed.
592593

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

‎theories/normedtype_theory/normed_module.v‎

Lines changed: 24 additions & 80 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
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 interval_inference fieldext falgebra.
65
#[warning="-warn-library-file-internal-analysis"]
7-
From mathcomp Require Import unstable.
6+
From mathcomp Require Import mathcomp_extra unstable.
87
From mathcomp Require Import boolp classical_sets filter functions cardinality.
98
From mathcomp Require Import set_interval ereal reals topology real_interval.
109
From mathcomp Require Import prodnormedzmodule tvs num_normedtype.
@@ -396,6 +395,9 @@ Unshelve. all: by end_near. Qed.
396395
Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
397396
Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
398397

398+
HB.instance Definition _ := Norm.isNorm.Build K V (@Num.norm K V) (normr0 V)
399+
(@normr_ge0 _ V) (@normr0_eq0 _ V) (@ler_normD _ V) (@normrZ _ V).
400+
399401
End NormedModule_numDomainType.
400402

401403
Definition self_sub (K : numDomainType) (V W : normedModType K)
@@ -2494,68 +2496,15 @@ Let V' := @fullv _ V.
24942496
Variable B : (\dim V').-tuple V.
24952497
Hypothesis Bbasis : basis_of V' B.
24962498

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

25522501
HB.instance Definition _ :=
2553-
PseudoMetric.copy max_space (pseudoMetric_normed max_space).
2502+
PseudoMetric.copy (max_space Bbasis) (pseudoMetric_normed (max_space Bbasis)).
25542503

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

25572506
HB.instance Definition _ :=
2558-
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R max_space max_normZ.
2507+
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) (max_normZ B).
25592508

25602509
End InfiniteNorm.
25612510

@@ -2587,23 +2536,16 @@ apply: (@continuous_compact _ _ f).
25872536
exact: segment_compact.
25882537
Qed.
25892538

2590-
Lemma equivalence_norms (N : V -> R) :
2591-
N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) ->
2592-
(forall x y, N (x + y) <= N x + N y) ->
2593-
(forall r x, N (r *: x) = `|r| * N x) ->
2539+
Lemma equivalence_norms (N : Norm.Norm.type V) :
25942540
exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|.
25952541
Proof.
2596-
move=> N0 N_ge0 N0_eq0 ND NZ.
25972542
set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i.
2598-
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0.
2599-
have N_sum (I : Type) (r : seq I) (F : I -> V) :
2600-
N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i).
2601-
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.
26022544
have leNoo (x : Voo) : N x <= M0 * `|x|.
2603-
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 _ _ _))//.
26042547
rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _.
2605-
by rewrite NZ mulrC ler_pM// le_coord_max_norm.
2606-
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.
26072549
have NC0 : continuous (N : Voo -> R).
26082550
move=> /= x; rewrite /continuous_at.
26092551
apply: cvg_zero; first exact: nbhs_filter.
@@ -2613,8 +2555,8 @@ have NC0 : continuous (N : Voo -> R).
26132555
rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//.
26142556
apply/ler_normlP.
26152557
have NB a b : N a <= N b + N (a - b).
2616-
by rewrite (le_trans _ (ND _ _)) ?subrKC.
2617-
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.
26182560
rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN.
26192561
by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
26202562
have: compact [set x : Voo | `|x| = 1].
@@ -2630,20 +2572,23 @@ move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
26302572
[set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)).
26312573
move=> /= r /set_mem/= [y y1 <-].
26322574
apply: inv_continuous.
2633-
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.
26342577
move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))).
26352578
rewrite /globally/= => M1N.
26362579
exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00.
26372580
split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx.
2638-
have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0.
2581+
have [->|x0] := eqVneq x 0; first by rewrite normr0 Norm.norm0 mulr0.
26392582
have Nx0 : 0 < N x.
2640-
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.
26412585
have normx0 : 0 < `|x| by rewrite normr_gt0.
26422586
move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[].
26432587
exists (N x / `|x|); last by rewrite invf_div.
2644-
exists (`|x|^-1 *: x); last by rewrite NZ mulrC ger0_norm.
2588+
exists (`|x|^-1 *: x); last by rewrite Norm.normZ mulrC ger0_norm.
26452589
by rewrite normrZ normfV normr_id mulVf// gt_eqF.
2646-
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.
26472592
by rewrite ler_pM2r// le_max lexx orbT.
26482593
Unshelve. all: by end_near. Qed.
26492594

@@ -2666,8 +2611,7 @@ apply: cvg_sum => i _.
26662611
rewrite [X in _ --> X]linearZ/= -/B.
26672612
apply: cvgZr_tmp.
26682613
move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
2669-
have [M M0 MP] := @equivalence_norms R V (@normr R V) (@normr0 _ _)
2670-
(@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _).
2614+
have [M M0 MP] := equivalence_norms (@Num.norm _ V).
26712615
exists (M * r) => x.
26722616
move: MP => /(_ x) [Mx _] xr.
26732617
by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW.

0 commit comments

Comments
 (0)