instead of lspace_master

[affeldt-aist]

Motivation for this change

Closes #1506

I wasn't able to rebase, hence the new PR closing the old one. @hoheinzollern @CohenCyril @proux01 @t6s

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

[affeldt-aist]

The last commit renames the HB structure Lfun to Lfunction. There is no impact
on scripts but lets us write \in Lfun instead of \in lfun as we did so far.
The type remains LfunType (this is similar to the contraction of zmodType for Zmodule).

[CohenCyril]

I think the issues about the conjugate should be solved before merging.

[CohenCyril]

I suspect this would be better, and perhaps

Suggested change

	Lemma Lnorm0 p : 1 <= p -> 'N_p[cst 0] = 0.
	Lemma Lnorm0 p : p != 0 -> 'N_p[cst 0] = 0.

Or even without condition when we enable (mu (f @^-1` (setT `\ 0%R))) when p = 0 (which looks like a saner convention than the current one)?
No need to fix this right away, but maybe open an issue.

[CohenCyril]

Those two look a bit awkward, I would posit the other way around, without match and making it a bijection of extended reals relating $-\infty$ and $0$ (both ways):

Suggested change

	match p with
	| r%:E => [get q : R | r^-1 + q^-1 = 1]%:E
	| +oo => 1
	| -oo => 0
	end.
	Lemma conjugateE :
	conjugate = if p is r%:E then (r * (r-1)^-1)%:E
	else if p == +oo then 1 else 0.
	if p == +oo then 1 else if p == 0 then -oo else p / (p - 1).
	Local Notation "p^*" := holder_conjugate.
	Lemma hoelder_conjugate_eq1 : p > -oo -> p^-1 + p^*^-1 = 1.

and add lemmas:

Lemma hoelder_conjugate1 : 1^* = +oo.
Lemma hoelder_conjugate2 : 2^* = 2.
Lemma hoelder_conjugatey : +oo^* = 1.

Lemma hoelder_conjugateP p q : p > -oo -> p^-1 + q^-1 = 1 <-> q = p^*.

Lemma hoelder_conjugate0 : 0^* = -oo.
Lemma hoelder_conjugateNy : -oo^* = 0.

Lemma hoelder_conjugateK : involutive hoelder_conjugate.

Lemma hoelder_Mconjugate : p > -oo -> p != 0 -> p * p^* = p + p^*.
Lemma hoelder_div_conjugate : p > -oo -> p != 0 -> p / p^* = p - 1.
Lemma hoelder_conjugate_div : p > -oo -> p != 0 -> p^* / p = p^* - 1.

[CohenCyril]

Suggested change

	Definition conjugate :=
	Definition hoelder_conjugate :=

[CohenCyril]

Not sure there are already users... is it worth doing a two-stage deprecation notice?

[CohenCyril]

Suggested change

	#[deprecated(since="mathcomp-analysis 1.10.0",
	note="use `minkowski_EFin` or `eminkowski` instead")]
	#[deprecated(since="mathcomp-analysis 1.10.0",
	note="use `minkowski_EFin` or `minkowski` instead")]

[CohenCyril]

Suggested change

	Lemma eminkowski f g (p : \bar R) :
	Lemma minkowski f g (p : \bar R) :

Indeed the functions f anf g are still with values in R while they could be in \bar R.

[CohenCyril]

Not sure there are already users... is it worth doing a two-stage deprecation notice?

[CohenCyril]

Lemmas relying on this specialization should be future proof for when the restriction on the argument of the norm is lifted. i.e. when this become Local Notation "'N_ p [ f ]" := (Lnorm mu p f)., in particular eminkowski might be a misnommer (see comment below).