Normed vector types, infinite norm, norm equivalence thm, continuity …#1718
Normed vector types, infinite norm, norm equivalence thm, continuity …#1718Tragicus wants to merge 5 commits intomath-comp:masterfrom
Conversation
|
@mkerjean FYI |
| Let V' := @fullv _ V. | ||
| Hypothesis (Bbasis : basis_of V' B). | ||
|
|
||
| Definition oo_norm x := \big[Order.max/0]_(i < \dim V') `|coord B i x|. |
There was a problem hiding this comment.
Is it really a good name? Because it is a bit like using a notation inside an identifier, also we have been using oo to mean "open-open" in MathComp (when talking about intervals). What about infty_norm? (like in LaTeX). Possibly coupling it with a notation using +oo in some way.
There was a problem hiding this comment.
max_norm is maybe also an option
There was a problem hiding this comment.
"Inifinity norm" or "supremum norm" (or "norme sup" or "norme infinie" in french) is the traditional name.
| 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|. |
There was a problem hiding this comment.
I think this deserve an abstraction of norm and an abstraction of norm comparison :)
|
99d840c is just a linting commit |
|
I was also wondering whether we should not try to extract the lemmas about bigmax (of non-negative terms using 0 as the default element) or try to use bigmax with |
Tragicus
force-pushed
the
linear_findim_continuous
branch
from
99d840c to
994f950
Compare
CohenCyril
force-pushed
the
linear_findim_continuous
branch
from
1a0fa98 to
6f03a34
Compare
classical/unstable.v
Outdated
| by move=> /(le_trans IHl). | ||
| Qed. | ||
|
|
||
| Lemma max_norm0 : max_norm 0 = 0. |
There was a problem hiding this comment.
Shouldn't this lemma by declared as a Let? (same comment for the following lemmas in this section)
| 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|. |
There was a problem hiding this comment.
Maybe max_norm should be documented in the header (maybe also max_space just below)?
classical/unstable.v
Outdated
| 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). |
There was a problem hiding this comment.
| norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i). | |
| norm (\sum_(i <- r) F i) <= \sum_(i <- r) norm (F i). |
|
For example, |
Tragicus
force-pushed
the
linear_findim_continuous
branch
2 times, most recently
from
f678a8e to
eb94092
Compare
…of linear functions in finite dimension
Tragicus
force-pushed
the
linear_findim_continuous
branch
from
eb94092 to
c7c7aa1
Compare
Tragicus
force-pushed
the
linear_findim_continuous
branch
from
c7c7aa1 to
e09f221
Compare
| 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|. |
There was a problem hiding this comment.
Inference of a Norm.type for max_norm fails because the instance requires B to be a basis. However, it feels wrong to me to add the hypothesis in the definition of max_norm. What do you think?
3 participants
Continuity of linear functions in finite dimension
Motivation for this change
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers