Skip to content

Commit e75500a

Browse files
TragicusTragicus
committed
stop exposing max_space and max_norm
1 parent bb7ab14 commit e75500a

3 files changed

Lines changed: 100 additions & 110 deletions

File tree

‎CHANGELOG_UNRELEASED.md‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -77,8 +77,6 @@
7777
- in `unstable.v`:
7878
+ structure `Norm`
7979
+ lemmas `normMn`, `normN`, `ler_norm_sum`
80-
+ definitions `max_norm`, `max_space`
81-
+ lemma `le_coord_max_norm`
8280

8381
- in `normed_module.v`:
8482
+ structure `NormedVector`

‎classical/unstable.v‎

Lines changed: 0 additions & 76 deletions
Original file line numberDiff line numberDiff line change
@@ -637,79 +637,3 @@ End Theory.
637637
Module Import Exports. HB.reexport. End Exports.
638638
End Norm.
639639
Export Norm.Exports.
640-
641-
Section InfiniteNorm.
642-
Variables (K : numFieldType) (V : vectType K).
643-
644-
Definition max_norm x : K := \big[Order.max/0]_(i < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|.
645-
646-
Definition max_space : Type := V.
647-
648-
HB.instance Definition _ := Vector.on max_space.
649-
650-
Check erefl: (max_space : vectType _) = V.
651-
652-
Let max_norm_ge0 x : 0 <= max_norm x.
653-
Proof.
654-
rewrite /max_norm.
655-
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
656-
Qed.
657-
658-
Lemma le_coord_max_norm x i : `|coord (vbasis fullv) i x| <= max_norm x :> K.
659-
Proof.
660-
rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
661-
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
662-
case: ifP => [/ltW|]// /negbT.
663-
set b := (X in _ < X).
664-
have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real.
665-
have /comparable_leNgt <- := real_comparable bR (normr_real (coord (vbasis fullv) j x)).
666-
by move=> /(le_trans IHl).
667-
Qed.
668-
669-
Let max_norm0 : max_norm 0 = 0.
670-
Proof.
671-
apply: le_anti; rewrite max_norm_ge0 andbT.
672-
apply: bigmax_le => // i _.
673-
have <-: \sum_(i < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0.
674-
under eq_bigr do rewrite scale0r.
675-
by rewrite sumr_const mul0rn.
676-
by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)).
677-
Qed.
678-
679-
Let ler_max_normD x y : max_norm (x + y) <= max_norm x + max_norm y.
680-
Proof.
681-
apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
682-
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
683-
Qed.
684-
685-
Let max_norm0_eq0 x : max_norm x = 0 -> x = 0.
686-
Proof.
687-
move=> x0; rewrite (coord_vbasis (memvf x)).
688-
suff: forall i, coord (vbasis fullv) i x = 0.
689-
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
690-
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
691-
Qed.
692-
693-
Let max_normZ r x : max_norm (r *: x) = `|r| * max_norm x.
694-
Proof.
695-
rewrite /max_norm.
696-
under eq_bigr do rewrite linearZ/= normrM.
697-
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
698-
by rewrite !big_cons IHl maxr_pMr.
699-
Qed.
700-
701-
HB.instance Definition _ := Norm.isNorm.Build K V max_norm
702-
max_norm0 max_norm_ge0 max_norm0_eq0 ler_max_normD max_normZ.
703-
704-
Let max_normMn x n : max_norm (x *+ n) = max_norm x *+ n.
705-
Proof. exact: Norm.Theory.normMn. Qed.
706-
707-
Let max_normN x : max_norm (- x) = max_norm x.
708-
Proof. exact: Norm.Theory.normN. Qed.
709-
710-
HB.instance Definition _ := Num.Zmodule_isNormed.Build K
711-
max_space ler_max_normD max_norm0_eq0 max_normMn max_normN.
712-
713-
End InfiniteNorm.
714-
715-
Set Printing All.

‎theories/normedtype_theory/normed_module.v‎

Lines changed: 100 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -2458,35 +2458,100 @@ Proof. by rewrite /open_disjoint_itv; case: cid => //= I [_]. Qed.
24582458

24592459
End open_set_disjoint_real_intervals.
24602460

2461-
Section InfiniteNorm.
2462-
Variables (R : numFieldType) (V : vectType R).
2461+
Section EquivalenceNorms.
2462+
Variables (R : realType).
24632463

2464-
HB.instance Definition _ := Pointed.copy (max_space V) V^o.
2464+
(* FIXME: Specialize to vector space with basis and expose this definition
2465+
(see https://github.com/math-comp/analysis/issues/1911).
2466+
It will also be possible to generalize to `numFieldType`. *)
2467+
Let max_norm (V : vectType R) x : R := \big[Order.max/0]_(i < \dim (@fullv _ V)) `|coord (vbasis fullv) i x|.
24652468

2466-
HB.instance Definition _ :=
2467-
PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)).
2469+
Definition max_space (V : vectType R) : Type := V.
24682470

2469-
HB.instance Definition _ := NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.
2471+
HB.instance Definition _ (V : vectType R) := Vector.on (max_space V).
24702472

2471-
HB.instance Definition _ :=
2472-
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
2473-
(@Norm.normZ _ _ (@max_norm _ V)).
2473+
HB.instance Definition _ (V : vectType R) := Pointed.copy (max_space V) V^o.
24742474

2475-
End InfiniteNorm.
2475+
Let max_norm_ge0 (V : vectType R) (x : V) : 0 <= max_norm x.
2476+
Proof.
2477+
rewrite /max_norm.
2478+
by elim/big_ind : _ => //= ? ? ? ?; rewrite /Order.max; case: ifP.
2479+
Qed.
24762480

2477-
Section EquivalenceNorms.
2478-
Variables (R : realType) (V : vectType R).
2479-
Let Voo := max_space V.
2481+
(* FIXME: expose. *)
2482+
Let le_coord_max_norm (V : vectType R) (x : V) i : `|coord (vbasis fullv) i x| <= max_norm x :> R.
2483+
Proof.
2484+
rewrite /max_norm; elim: (index_enum _) (mem_index_enum i) => //= j l IHl.
2485+
rewrite inE big_cons [X in _ <= X _ _]/Order.max/= => /predU1P[<-|/IHl {}IHl];
2486+
case: ifP => [/ltW|]// /negbT.
2487+
set b := (X in _ < X).
2488+
have bR : b \is Num.real by apply: bigmax_real => // a _; apply: normr_real.
2489+
have /comparable_leNgt <- := real_comparable bR (normr_real (coord (vbasis fullv) j x)).
2490+
by move=> /(le_trans IHl).
2491+
Qed.
2492+
2493+
Let max_norm0 (V : vectType R) : @max_norm V 0 = 0.
2494+
Proof.
2495+
apply: le_anti; rewrite max_norm_ge0 andbT.
2496+
apply: bigmax_le => // i _.
2497+
have <-: \sum_(i < \dim (@fullv _ V)) 0 *: (vbasis (@fullv _ V))`_i = 0.
2498+
under eq_bigr do rewrite scale0r.
2499+
by rewrite sumr_const mul0rn.
2500+
by rewrite coord_sum_free ?normr0// (basis_free (vbasisP _)).
2501+
Qed.
2502+
2503+
Let ler_max_normD (V : vectType R) (x y : V) : max_norm (x + y) <= max_norm x + max_norm y.
2504+
Proof.
2505+
apply: bigmax_le => [|/= i _]; first by rewrite addr_ge0// max_norm_ge0.
2506+
by rewrite raddfD/= (le_trans (ler_normD _ _))// lerD// le_coord_max_norm.
2507+
Qed.
2508+
2509+
Let max_norm0_eq0 (V : vectType R) (x : V) : max_norm x = 0 -> x = 0.
2510+
Proof.
2511+
move=> x0; rewrite (coord_vbasis (memvf x)).
2512+
suff: forall i, coord (vbasis fullv) i x = 0.
2513+
by move=> {}x0; rewrite big1//= => j _; rewrite x0 scale0r.
2514+
by move=> i; apply/normr0_eq0/le_anti; rewrite normr_ge0 -x0 le_coord_max_norm.
2515+
Qed.
2516+
2517+
Let max_normZ (V : vectType R) r (x : V) : max_norm (r *: x) = `|r| * max_norm x.
2518+
Proof.
2519+
rewrite /max_norm.
2520+
under eq_bigr do rewrite linearZ/= normrM.
2521+
elim: (index_enum _) => [|i l IHl]; first by rewrite !big_nil mulr0.
2522+
by rewrite !big_cons IHl maxr_pMr.
2523+
Qed.
2524+
2525+
HB.instance Definition _ (V : vectType R) := Norm.isNorm.Build R V (@max_norm V)
2526+
(max_norm0 V) (@max_norm_ge0 V) (@max_norm0_eq0 V) (@ler_max_normD V) (@max_normZ V).
2527+
2528+
Let max_normMn (V : vectType R) (x : V) n : max_norm (x *+ n) = max_norm x *+ n.
2529+
Proof. exact: (Norm.Theory.normMn (@normed_module_max_norm__canonical__Norm_Norm V)). Qed.
2530+
2531+
Let max_normN (V : vectType R) (x : V) : max_norm (- x) = max_norm x.
2532+
Proof. exact: (Norm.Theory.normN (@normed_module_max_norm__canonical__Norm_Norm V)). Qed.
2533+
2534+
HB.instance Definition _ (V : vectType R) := Num.Zmodule_isNormed.Build R
2535+
(max_space V) (@ler_max_normD V) (@max_norm0_eq0 V) (@max_normMn V) (@max_normN V).
2536+
2537+
HB.instance Definition _ (V : vectType R) :=
2538+
PseudoMetric.copy (max_space V) (pseudoMetric_normed (max_space V)).
2539+
2540+
HB.instance Definition _ (V : vectType R) := NormedZmod_PseudoMetric_eq.Build R (max_space V) erefl.
2541+
2542+
HB.instance Definition _ (V : vectType R) :=
2543+
PseudoMetricNormedZmod_Lmodule_isNormedModule.Build R (max_space V)
2544+
(@Norm.normZ _ _ (@max_norm V)).
24802545

24812546
(* N.B. Get Trocq to prove the continuity part automatically. *)
2482-
Lemma sup_closed_ball_compact : compact (closed_ball (0 : Voo) 1).
2547+
Lemma sup_closed_ball_compact (V : vectType R) : compact (closed_ball (0 : max_space V) 1).
24832548
Proof.
24842549
rewrite closed_ballE// /closed_ball_.
24852550
under eq_set do rewrite sub0r normrN.
24862551
rewrite -[forall x, _]/(compact _).
24872552
pose f (X : {ptws 'I_(\dim (@fullv _ V)) -> R}) : V :=
24882553
\sum_(i < \dim (@fullv _ V)) X i *: (vbasis fullv)`_i.
2489-
have -> : [set x : Voo | `|x| <= 1] =
2554+
have -> : [set x : max_space V | `|x| <= 1] =
24902555
f @` [set X | forall i, `[-1, 1]%classic (X i)].
24912556
apply/seteqP; split=> [x/= x1|x/= [X X1 <-]].
24922557
(* FIXME: The type annotation on x is mandatory, otherwise we try to unify V
@@ -2496,24 +2561,32 @@ have -> : [set x : Voo | `|x| <= 1] =
24962561
by move=> i; rewrite in_itv/= -ler_norml (le_trans _ x1)// le_coord_max_norm.
24972562
- rewrite /normr/= /max_norm bigmax_le => //= i _.
24982563
by rewrite coord_sum_free ?ler_norml; [exact: X1|exact/basis_free/vbasisP].
2499-
apply (@continuous_compact _ _ (f : _ -> Voo)).
2564+
apply (@continuous_compact _ _ (f : _ -> max_space V)).
25002565
- apply/continuous_subspaceT/sum_continuous => /= i _ x.
25012566
exact/continuousZr_tmp/proj_continuous.
25022567
- apply: (@tychonoff 'I_(\dim (@fullv _ V)) (fun=> R^o) (fun=> `[-1, 1]%classic)) => _.
25032568
exact: segment_compact.
25042569
Qed.
25052570

2506-
Lemma equivalence_norms (N : Norm.Norm.type V) :
2507-
exists2 M, 0 < M & forall x : Voo, `|x| <= M * N x /\ N x <= M * `|x|.
2571+
Lemma equivalence_norms (V : vectType R) (N N' : Norm.Norm.type V) :
2572+
exists2 M, 0 < M & forall x : max_space V, N' x <= M * N x /\ N x <= M * N' x.
25082573
Proof.
2574+
suff: forall (N : Norm.Norm.type V),
2575+
exists2 M, 0 < M & forall x : max_space V, `|x| <= M * N x /\ N x <= M * `|x|.
2576+
move=> /[dup] /(_ N) []/= M M0 Noo /(_ N') []/= M' M'0 N'oo.
2577+
exists (M * M') => [|x]; first exact: mulr_gt0.
2578+
move: Noo N'oo => /(_ x) [] Nge Nle /(_ x) [] N'ge N'le.
2579+
split; first by apply: (le_trans N'le); rewrite mulrAC mulrC ler_pM2r.
2580+
by apply: (le_trans Nle); rewrite -mulrA ler_pM2l.
2581+
move=> {N'}N.
25092582
set M0 := 1 + \sum_(i < \dim (@fullv _ V)) N (vbasis fullv)`_i.
25102583
have M00 : 0 < M0 by rewrite ltr_pwDl// sumr_ge0// => ? _; apply: Norm.norm_ge0.
2511-
have leNoo (x : Voo) : N x <= M0 * `|x|.
2584+
have leNoo (x : max_space V) : N x <= M0 * `|x|.
25122585
rewrite [in leLHS](coord_vbasis (memvf (x : V))).
25132586
rewrite (le_trans (Norm.Theory.ler_norm_sum _ _ _))//.
25142587
rewrite mulrDl mul1r mulr_suml ler_wpDl// ler_sum => //= i _.
25152588
by rewrite Norm.normZ mulrC ler_pM// ?le_coord_max_norm// Norm.norm_ge0.
2516-
have NC0 : continuous (N : Voo -> R).
2589+
have NC0 : continuous (N : max_space V -> R).
25172590
move=> /= x; rewrite /continuous_at.
25182591
apply: cvg_zero; first exact: nbhs_filter.
25192592
apply/cvgr0Pnorm_le; first exact: nbhs_filter.
@@ -2526,17 +2599,17 @@ have NC0 : continuous (N : Voo -> R).
25262599
by rewrite opprB !lerBlDl NB -opprB Norm.Theory.normN NB.
25272600
rewrite (le_trans (leNoo _))// mulrC -ler_pdivlMr// -opprB normrN.
25282601
by near: y; apply: cvgr_dist_le; [exact: cvg_id|exact: divr_gt0].
2529-
have: compact [set x : Voo | `|x| = 1].
2530-
apply: (subclosed_compact _ sup_closed_ball_compact).
2602+
have: compact [set x : max_space V | `|x| = 1].
2603+
apply: (subclosed_compact _ (@sup_closed_ball_compact V)).
25312604
- apply: (@closed_comp _ _ _ [set 1 : R]); last exact: closed_eq.
25322605
by move=> *; exact: norm_continuous.
25332606
- by move => x/=; rewrite closed_ballE// /closed_ball_/= sub0r normrN => ->.
2534-
move=> /(@continuous_compact _ _ (N : Voo -> R)) -/(_ _)/wrap[].
2607+
move=> /(@continuous_compact _ _ (N : max_space V -> R)) -/(_ _)/wrap[].
25352608
exact: continuous_subspaceT.
25362609
move=> /(@continuous_compact _ _ (@GRing.inv R)) -/(_ _)/wrap[].
25372610
move=> /= x; rewrite /continuous_at.
25382611
apply: (@continuous_in_subspaceT _ _
2539-
[set N x | x in [set x : Voo | `|x| = 1]] (@GRing.inv R)).
2612+
[set N x | x in [set x : max_space V | `|x| = 1]] (@GRing.inv R)).
25402613
move=> /= r /set_mem/= [y y1 <-].
25412614
apply: inv_continuous.
25422615
apply: contra_eq_neq y1 => /Norm.norm0_eq0 ->.
@@ -2559,12 +2632,7 @@ rewrite ler_pdivrMr// => /le_trans; apply.
25592632
by rewrite ler_pM2r// le_max lexx orbT.
25602633
Unshelve. all: by end_near. Qed.
25612634

2562-
End EquivalenceNorms.
2563-
2564-
Section LinearContinuous.
2565-
Variables (R : realType) (V : normedVectType R) (W : normedModType R).
2566-
2567-
Lemma linear_findim_continuous (f : {linear V -> W}) : continuous f.
2635+
Lemma linear_findim_continuous (V : normedVectType R) (W : normedModType R) (f : {linear V -> W}) : continuous f.
25682636
Proof.
25692637
set V' := @fullv _ V.
25702638
set B := vbasis V'.
@@ -2578,10 +2646,10 @@ apply: cvg_sum => i _.
25782646
rewrite [X in _ --> X]linearZ/= -/B.
25792647
apply: cvgZr_tmp.
25802648
move: x; apply/linear_bounded_continuous/bounded_funP => r/=.
2581-
have [M M0 MP] := equivalence_norms (@Num.norm _ V).
2649+
have [M M0 MP] := equivalence_norms (@Num.norm _ V) (@max_norm V).
25822650
exists (M * r) => x.
25832651
move: MP => /(_ x) [Mx _] xr.
25842652
by rewrite (le_trans (le_coord_max_norm _ _))// (le_trans Mx) ?ler_wpM2l// ltW.
25852653
Qed.
25862654

2587-
End LinearContinuous.
2655+
End EquivalenceNorms.

0 commit comments

Comments
 (0)