Zulip Chat Archive
Stream: mathlib4
Topic: Elements of a Hölder triple can be zero
Yaël Dillies (Apr 04 2025 at 07:54):
@Jireh Loreaux, is it expected that ENNReal.HolderTriple 0 0 0 is true? I would have expected a nonzero assumption on r in docs#ENNReal.HolderTriple
Jireh Loreaux (Apr 04 2025 at 12:36):
Why not? If f and g are measurable, so is their product?
Last updated: May 02 2025 at 03:31 UTC