HolderTriple vs IsConjExponent

Stream: mathlib4

[Rémy Degenne]

The class ENNReal.HolderTriple was recently added. We also had ENNReal.IsConjExponent which is mathematically a particular case of the new definition.
Should we do something about that duplication? Remove IsConjExponent for ENNReal?

[Rémy Degenne]

@Jireh Loreaux

[Yaël Dillies]

I think having both is useful, if only because docs#Real.IsConjExponent and docs#NNReal.IsConjExponent are a thing

[Jireh Loreaux]

Ugh... I didn't realize we had these when I created HolderTriple. Note that we also have the abbrev docs#ENNReal.HolderConjugate. The new class does serve a purpose not currently served by docs#ENNReal.IsConjExponent, which is that (a) it is the proper generality for Hölder's inequality, and (b) since it's a class, it can be used in instances (as is done in #21583).

I'm inclined to agree with Yaël, that we should keep the Real and NNReal structures, because they do have the slightly different condition that p > 1. However:

1. we should standardize the names.
2. docs#ENNReal.IsConjExponent and docs#ENNReal.HolderConjugate should be merged.
3. Along with the above, the API should be merged and uniformized.

[Yaël Dillies]

Jireh Loreaux said:

Ugh... I didn't realize we had these when I created HolderTriple

Oh. That was the purpose of my very first comment on this PR series.

[Yaël Dillies]

I would have recommented on #21854 but it got insta-merged

[Jireh Loreaux]

I realize that now, but at the time I thought you meant "conjugate exponents generally", not "ENNReal.IsConjExponent".

[Yaël Dillies]

Yeah sorry, I see it was confusing. Honestly I was just very certain you already knew about ENNReal.IsConjExponent

[Jireh Loreaux]

I expected that it would have existed (or rather the more general triple version), but when I went to work with Hölder's inequality, the hypotheses in those theorems were simply 1/r = 1/p + 1/q, so I thought that if it had existed, it would be used there. And then in the HolderTriple thread on Zulip, no one mentioned this ENNReal.IsConjExponent.

[Jireh Loreaux]

In any case, there's now some clean-up to do, but It I think Mathlib will be better for it in the end.

[Jireh Loreaux]

Two questions:

1. Should I create Triple versions of the Real and NNReal variants?
2. Which name do we prefer? ENNReal.HolderConjugate or ENNReal.IsConjExponent? Presumably, if we choose the former, it would mean also changing names for the Real and NNReal versions.

[Yaël Dillies]

1. Yes please :pray:
2. I'm not fussed. I never really liked IsConjExponent, eg I would much prefer IsConjExp (why would "conjugate" be abbreviated but not "exponent"?)

[Rémy Degenne]

Please not IsConjExp :) . HolderConjugate at least has actual understandable words in it.

[Yaël Dillies]

What about HolderConj then?

[Rémy Degenne]

In that case I prefer an understandable name over a shorter one. Also if we keep HolderConjugate that's one less thing to deprecate.
About the Real and NNReal triple variants: let's create them only if a review of the library indicates they would be useful?

[Yaël Dillies]

Rémy Degenne said:

if we keep HolderConjugate that's one less thing to deprecate.

Arguably, the PR introducing HolderConjugate was barely reviewed, so...

[Jireh Loreaux]

#22944 does (probably too much, but I ddin't realize that when I started) the two things mentioned above: adds {NN}Real.HolderTriple and redefines IsConjExponent in terms of it (and renames IsConjExponent to HolderConjugate).

I put all the deprecations at the end of the file in the same order they appear in the original, which is probably the easiest way to review those.