Commit 2025-02-19 07:30 da60520f

refactor: allow for bilinear maps of norm greater than one in Hölder's inequality and use HolderTriple (#21792) This PR does two things, both related to statements of Hölder's inequality:

1. In the generic statements involving a general map b : E → F → G (which we think of as a continuous bilinear map despite the fact that these are not quite the hypotheses), we loosen the assumptions on b so that it need not have norm bounded by 1. This makes it possible to use general continuous bilinear maps in the forthcoming #21583, and addresses the concerns in #6108.
2. Changes the statements to make use of the new ENNReal.HolderTriple type class. Among other things, this makes some existing lemmas specialized to ∞ redundant, so we deprecate them. Closes #6108.