Skip to content

Commit 994f950

Browse files
TragicusTragicus
committed
norm interface
1 parent a279568 commit 994f950

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
@@ -9,12 +9,18 @@
99
- in `tvs.v`
1010
+ lemmas `cvg_sum`, `sum_continuous`
1111

12+
- in `unstable.v`:
13+
+ structure `Norm`
14+
+ lemmas `normMn`, `normN`, `ler_norm_sum`
15+
+ definitions `max_norm`, `max_space`
16+
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `max_norm0`, `ler_max_normD`,
17+
`max_norm0_eq0`, `max_normZ`, `max_normMn`, `max_normN`
18+
1219
- in `normed_module.v`:
1320
+ structure `NormedVector`
14-
+ definitions `normedVectType`, `max_norm`, `max_space`
15-
+ lemmas `max_norm_ge0`, `le_coord_max_norm`, `ler_max_normD`, `max_norm0_eq0`,
16-
`max_normZ`, `max_normMn`, `max_normN`, `sup_closed_ball_compact`,
17-
`equivalence_norms`, `linear_findim_continuous`
21+
+ definition `normedVectType`
22+
+ lemmas `sup_closed_ball_compact`, `equivalence_norms`,
23+
`linear_findim_continuous`
1824

1925
### Changed
2026
- 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 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**************************************************************************)
@@ -553,3 +554,114 @@ End ProperNotations.
553554

554555
Lemma sqrtK {K : rcfType} : {in Num.nneg, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
555556
Proof. by move=> r r0; rewrite sqr_sqrtr. Qed.
557+
558+
Module Norm.
559+
560+
HB.mixin Record isNorm (K : numDomainType) (L : lmodType K) (norm : L -> K) := {
561+
norm0 : norm 0 = 0;
562+
norm_ge0 : forall x, 0 <= norm x;
563+
norm0_eq0 : forall x, norm x = 0 -> x = 0;
564+
ler_normD : forall x y, norm (x + y) <= norm x + norm y;
565+
normZ : forall r x, norm (r *: x) = `|r| * norm x;
566+
}.
567+
568+
#[export]
569+
HB.structure Definition Norm K L := { norm of @isNorm K L norm }.
570+
571+
Module Import Theory.
572+
Section Theory.
573+
Variables (K : numDomainType) (L : lmodType K) (norm : Norm.type L).
574+
575+
Lemma normMn x n : norm (x *+ n) = norm x *+ n.
576+
Proof. by rewrite -scaler_nat normZ normr_nat mulr_natl. Qed.
577+
578+
Lemma normN x : norm (- x) = norm x.
579+
Proof. by rewrite -scaleN1r normZ normrN1 mul1r. Qed.
580+
581+
Lemma ler_norm_sum (I : Type) (r : seq I) (F : I -> L) :
582+
norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i).
583+
Proof.
584+
by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD.
585+
Qed.
586+
587+
End Theory.
588+
End Theory.
589+
590+
Module Import Exports. HB.reexport. End Exports.
591+
End Norm.
592+
Export Norm.Exports.
593+
594+
Section InfiniteNorm.
595+
Variables (K : numFieldType) (V : vectType K).
596+
Let V' := @fullv _ V.
597+
Variable B : (\dim V').-tuple V.
598+
Hypothesis Bbasis : basis_of V' B.
599+
600+
Definition max_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|.
601+
602+
Definition max_space : Type := (fun=> V) Bbasis.
603+
604+
HB.instance Definition _ := Vector.on max_space.
605+
606+
Lemma max_norm_ge0 x : 0 <= max_norm x.
607+
Proof.
608+
rewrite /max_norm.
609+
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
610+
Qed.
611+
612+
Lemma le_coord_max_norm x i : `|coord B i x| <= max_norm x.
613+
Proof.
614+
rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
615+
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
616+
case: ifP => [/ltW|]// /negbT.
617+
set b := (X in _ < X).
618+
have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real.
619+
have /comparable_leNgt <- := real_comparable bR (normr_real (coord B j x)).
620+
by move=> /(le_trans IHl).
621+
Qed.
622+
623+
Lemma max_norm0 : max_norm 0 = 0.
624+
Proof.
625+
apply: le_anti; rewrite max_norm_ge0 andbT.
626+
apply: bigmax_le => // i _.
627+
have <-: \sum_(i < \dim V') 0 *: B`_i = 0.
628+
under eq_bigr do rewrite scale0r.
629+
by rewrite sumr_const mul0rn.
630+
by rewrite coord_sum_free ?normr0// (basis_free Bbasis).
631+
Qed.
632+
633+
Lemma ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y.
634+
Proof.
635+
apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
636+
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
637+
Qed.
638+
639+
Lemma max_norm0_eq0 x : max_norm x = 0 -> x = 0.
640+
Proof.
641+
move=> x0; rewrite (coord_basis Bbasis (memvf x)).
642+
suff: forall i, coord B i x = 0.
643+
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
644+
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
645+
Qed.
646+
647+
Lemma max_normZ r x : max_norm (r *: x) = `|r| * max_norm x.
648+
Proof.
649+
rewrite /max_norm.
650+
under eq_bigr do rewrite linearZ/= normrM.
651+
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
652+
by rewrite !big_cons IHl maxr_pMr.
653+
Qed.
654+
655+
HB.instance Definition _ := Norm.isNorm.Build K V max_norm
656+
max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ.
657+
658+
Lemma max_normMn x n : max_norm (x *+ n) = max_norm x *+ n.
659+
Proof. exact: Norm.Theory.normMn. Qed.
660+
661+
Lemma max_normN x : max_norm (- x) = max_norm x.
662+
Proof. exact: Norm.Theory.normN. Qed.
663+
664+
HB.instance Definition _ := Num.Zmodule_isNormed.Build K
665+
max_space ler_max_normD max_norm0_eq0 max_normMn max_normN.
666+
667+
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 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.
@@ -381,6 +381,9 @@ Unshelve. all: by end_near. Qed.
381381
Lemma ball_open_nbhs (x : V) (r : K) : 0 < r -> open_nbhs x (ball x r).
382382
Proof. by move=> e0; split; [exact: ball_open|exact: ballxx]. Qed.
383383

384+
HB.instance Definition _ := Norm.isNorm.Build K V (@Num.norm K V) (normr0 V)
385+
(@normr_ge0 _ V) (@normr0_eq0 _ V) (@ler_normD _ V) (@normrZ _ V).
386+
384387
End NormedModule_numDomainType.
385388

386389
Definition self_sub (K : numDomainType) (V W : normedModType K)
@@ -2477,68 +2480,15 @@ Let V' := @fullv _ V.
24772480
Variable B : (\dim V').-tuple V.
24782481
Hypothesis Bbasis : basis_of V' B.
24792482

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

25352485
HB.instance Definition _ :=
2536-
PseudoMetric.copy max_space (pseudoMetric_normed max_space).
2486+
PseudoMetric.copy (max_space Bbasis) (pseudoMetric_normed (max_space Bbasis)).
25372487

2538-
HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R max_space erefl.
2488+
HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space Bbasis) erefl.
25392489

25402490
HB.instance Definition _ :=
2541-
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R max_space max_normZ.
2491+
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space Bbasis) (max_normZ B).
25422492

25432493
End InfiniteNorm.
25442494

@@ -2570,23 +2520,16 @@ apply: (@continuous_compact _ _ f).
25702520
exact: segment_compact.
25712521
Qed.
25722522

2573-
Lemma equivalence_norms (N : V -> R) :
2574-
N 0 = 0 -> (forall x, 0 <= N x) -> (forall x, N x = 0 -> x = 0) ->
2575-
(forall x y, N (x + y) <= N x + N y) ->
2576-
(forall r x, N (r *: x) = `|r| * N x) ->
2523+
Lemma equivalence_norms (N : Norm.Norm.type V) :
25772524
exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|.
25782525
Proof.
2579-
move=> N0 N_ge0 N0_eq0 ND NZ.
25802526
set M0 := 1 + \sum_(i < \dim V') N (vbasis V')`_i.
2581-
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0.
2582-
have N_sum (I : Type) (r : seq I) (F : I -> V) :
2583-
N (\sum_(i <- r) F i) <= \sum_(i <- r) N (F i).
2584-
by elim/big_ind2 : _ => *; rewrite ?N0// (le_trans (ND _ _))// lerD.
2527+
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0.
25852528
have leNoo (x : Voo) : N x <= M0 * `|x|.
2586-
rewrite [in leLHS](coord_vbasis (memvf (x : V))) (le_trans (N_sum _ _ _))//.
2529+
rewrite [in leLHS](coord_vbasis (memvf (x : V))).
2530+
rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//.
25872531
rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _.
2588-
by rewrite NZ mulrC ler_pM// le_coord_max_norm.
2589-
have NZN a : N (- a) = N a by rewrite -scaleN1r NZ normrN1 mul1r.
2532+
by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0.
25902533
have NC0 : continuous (N : Voo -> R).
25912534
move=> /= x; rewrite /continuous_at.
25922535
apply: cvg_zero; first exact: nbhs_filter.
@@ -2596,8 +2539,8 @@ have NC0 : continuous (N : Voo -> R).
25962539
rewrite -[_ y]/(N y - N x) (@le_trans _ _ (N (y - x)))//.
25972540
apply/ler_normlP.
25982541
have NB a b : N a <= N b + N (a - b).
2599-
by rewrite (le_trans _ (ND _ _)) ?subrKC.
2600-
by rewrite opprB !lerBlDl NB -opprB NZN NB.
2542+
by rewrite (le_trans _ (Norm.ler_normD _ _))// subrKC.
2543+
by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB.
26012544
rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN.
26022545
by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
26032546
have: compact [set x : Voo | `|x| = 1].
@@ -2613,20 +2556,23 @@ move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
26132556
[set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)).
26142557
move=> /= r /set_mem/= [y y1 <-].
26152558
apply: inv_continuous.
2616-
by apply: contra_eq_neq y1 => /N0_eq0 ->; rewrite normr0 eq_sym oner_eq0.
2559+
apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->.
2560+
by rewrite normr0 eq_sym oner_eq0.
26172561
move=> /compact_bounded[M1 [M1R /(_ (1 + M1))]] /(_ (ltr_pwDl ltr01 (lexx _))).
26182562
rewrite /globally/= => M1N.
26192563
exists (maxr M0 (1 + M1)) => [|x]; first by rewrite lt_max M00.
26202564
split; last by rewrite (le_trans (leNoo x))// ler_wpM2r// le_max lexx.
2621-
have [->|x0] := eqVneq x 0; first by rewrite normr0 N0 mulr0.
2565+
have [->|x0] := eqVneq x 0; first by rewrite normr0 Norm.norm0 mulr0.
26222566
have Nx0 : 0 < N x.
2623-
by rewrite lt0r N_ge0 andbT; move: x0; apply: contra_neq => /N0_eq0.
2567+
rewrite lt0r Norm.norm_ge0 andbT.
2568+
by move: x0; apply: contra_neq => /Norm.norm0_eq0.
26242569
have normx0 : 0 < `|x| by rewrite normr_gt0.
26252570
move: M1N => /(_ (`|x| / N x)) -/(_ _)/wrap[].
26262571
exists (N x / `|x|); last by rewrite invf_div.
2627-
exists (`|x|^-1 *: x); last by rewrite NZ mulrC ger0_norm.
2572+
exists (`|x|^-1 *: x); last by rewrite Norm.normZ mulrC ger0_norm.
26282573
by rewrite normrZ normfV normr_id mulVf// gt_eqF.
2629-
rewrite ger0_norm ?divr_ge0// ler_pdivrMr// => /le_trans; apply.
2574+
rewrite ger0_norm; last by rewrite divr_ge0// Norm.norm_ge0.
2575+
rewrite ler_pdivrMr// => /le_trans; apply.
26302576
by rewrite ler_pM2r// le_max lexx orbT.
26312577
Unshelve. all: by end_near. Qed.
26322578

@@ -2649,8 +2595,7 @@ apply: cvg_sum => i _.
26492595
rewrite [X in _ --> X]linearZ/= -/B.
26502596
apply: cvgZr_tmp.
26512597
move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
2652-
have [M M0 MP] := @equivalence_norms R V (@normr R V) (@normr0 _ _)
2653-
(@normr_ge0 _ _) (@normr0_eq0 _ _) (@ler_normD _ _) (@normrZ _ _).
2598+
have [M M0 MP] := equivalence_norms (@Num.norm _ V).
26542599
exists (M * r) => x.
26552600
move: MP => /(_ x) [Mx _] xr.
26562601
by rewrite (le_trans (le_coord_max_norm _ _ _))// (le_trans Mx) ?ler_wpM2l// ltW.

0 commit comments

Comments
 (0)