Normed vector types, infinite norm, norm equivalence thm, continuity …

[Tragicus]

Continuity of linear functions in finite dimension

Motivation for this change

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[CohenCyril]

@mkerjean FYI

[affeldt-aist]

99d840c is just a linting commit

[affeldt-aist]

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 {nonneg _} because I know of at least to other PRs that are using the same elements (to deal with mx_norm or with variations of functions).

[affeldt-aist]

For example, Zmodule_isSemiNormed in MathComp provides a similar interface with the difference that norm is one of the field of the record (whereas here it is the subject). I guess the apparent duplication is unavoidable but doesn't it deserve a comment in the code?

[Tragicus]

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?

[affeldt-aist]

What about adding the hypothesis "temporarily"? Just leave an issue to be addressed later or add a warning to indicate to the user that it is experimental. I apologize for proposing this option without understanding completely the problem but I was under the impression that other users (@mkerjean , @agontard) also have an interest in the abstraction.

[CohenCyril]

Uh oh... this is more than fishy! This definition does depend on a basis (and not only the fact that the given tuple is a basis) and is thus morally not a valid vector space definition, which ought to be invariant wrt to the choice of a basis, and this one is clearly not. This is exactly why this definition does depend on a choice of basis. What it does is build the (unique) normed space on top of V that makes the given basis normal. This means that max_norm is probably not the right name (it would be the case when given a function, finite function or tuple with values in a normed vector space), probably the right name is something like norm_from_basis B Bbasis and normedVect_from_basis B Basis .

[CohenCyril]

However we can do slightly better: indeed we can amend the given candidate B, keeping the smallest initial family that is generating, pruning it in order to make it free, completing it thus making a basis out of it. If B was indeed a basis, the tuple would stay the same, otherwise we have a non canonical normed vector space, but that's life. It can still be useful though, because if we give it a free family, the generated norm will be unique on the vector space generated by this family, which is what a user might expect. I believe this is the right way to go.

[CohenCyril]

We can probably go further and generate a Hilbert space :)

[CohenCyril]

No you do not have to assume B is generating, you can complete it to be generating. (I was tired when I wrote my previous messages)

[Tragicus]

Ah, true, and in that case I might as well start from an empty B, i.e. get rid of B completely.

[CohenCyril]

No... please don't do that. 😿 we have to be able to provide a basis!

[CohenCyril]

We have to be able to mention a basis that is normed.

[CohenCyril]

Indeed it is not useful for your application, but it is nice to control which class of basis become normed.

To answer your other question the max_norm I had in mind would be the norm of a product of normed vector spaces, e.g. vT ^ i or more generally {dffun forall i : 'I_n, vT_ i} where vT_ : normedVectType^i.

[affeldt-aist]

I have rebased this PR on the current master and pushed force. There was a few conflicts because we recently generalized and moved a few lemmas from normed_module.v.

[CohenCyril]

Convention is:

Suggested change

	Variables (K : numFieldType) (V : vectType K).
	Let V' := @fullv _ V.
	Variables (K : numFieldType) (vT : vectType K).
	Let V' := {:vT}

And V' can be inlined.