Lp duality

Stream: Is there code for X?

[Jireh Loreaux]

Am I correct we don't have any version of the duality between MeasureTheory.Lp spaces for Hölder conjugate exponents?

[Sébastien Gouëzel]

We have the fact that if f is in L^p and g is in L^q for conjugate exponents, then their product is integrable, in docs#Memℒp.mul. So L^p embeds in the dual of L^q. Apart from the p=2 case (where it follows from general Hilbert space stuff), we don't have the complete identification, though.

[Jireh Loreaux]

Yeah, I guess what I really meant to ask was if we have surjectivity. Thanks for confirming.