Normed vector types, infinite norm, norm equivalence thm, continuity … #1718
Conversation
…of linear functions in finite dimension
|
@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
| 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 |
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