Hölder triples

Stream: maths

[Jireh Loreaux]

@Sébastien Gouëzel , @Yury G. Kudryashov I have just created #21583 and marked it as RFC. This PR introduces a ENNReal.HolderTriple class which just says that 1 / r = 1 / p + 1 / q. This makes it possible to define an HMul instance on MeasureTheory.Lp. From there I develop the natural map from Lp 𝕜 p μ into the dual of Lp 𝕜 q μ for HolderTriple 1 p q.

Let me know what you think. I've left out simp lemmas and various other details from the PR for now until I get some feedback from you about it.

[Kevin Buzzard]

I guess you could also do this with Fact?

[Jireh Loreaux]

I think not because you need r to be at least a semiOutParam? I'll double check though.

[Yury G. Kudryashov]

If there is no feedback from me in the next 20h, then please don't wait for it, as I'm travelling Feb 9-15

[Sébastien Gouëzel]

This looks very nice! I'm just wondering about the generality, as always: if f is a scalar-valued function in L^p and g is a vector-valued function in L^q, should we also introduce f • g for the vector-valued function in L^r (which would specialize to your construction when g is in fact scalar-valued)? And for the duality statement, for a general normed vector space E, there is a natural map from Lp (Dual E) p to Dual (Lq E q), should we look at this one (and at the specialized one when E is a Hilbert space) or just at the one-dimensional case?

[Jireh Loreaux]

I think these generalizations all make sense, and we should do those. If we need bespoke material for one dimension we can do that when we need it.

[Yury G. Kudryashov]

BTW, should we use HMul/HSMul or a docs#MeasureTheory.convolution style operator?

[Floris van Doorn]

To expand Yury's comment: I also think it might be nice to work with vector-valued functions and a bilinear map, like we do with docs#MeasureTheory.convolution. Then this can be instantiated to (scalar) multiplication.

Btw, my experience is to avoid docs#MeasureTheory.Lp as much as possible, and work with explicit functions instead. But it's possible of course that with more API using these quotients is also feasible, so I'm definitely not against adding this to Mathlib.

[Jireh Loreaux]

I agree that using Lp explicitly is generally not desirable, but sometimes you need it to state the correct result. For example, we will I think need the ultraweak topology on Lp \infty in order to state the Borel functional calculus properly, even though the API for it will still use bare functions.

[Jireh Loreaux]

I just had a look at docs#MeasureTheory.convolution, as I wasn't really familiar with it prior to this. @Floris van Doorn can you expand on this comment? What exactly are you wanting to replace with something that looks like this? Just the toDual map I have in the PR, or am I missing something bigger?

[Jireh Loreaux]

Nevermind, I think I understand. This, right?

variable {𝕜 α E F G : Type*} {m : MeasurableSpace α} {μ : Measure α} [NontriviallyNormedField 𝕜]
    [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    [NormedAddCommGroup F] [NormedSpace 𝕜 F]
    [NormedAddCommGroup G] [NormedSpace 𝕜 G]
    {p q r : ℝ≥0∞} [HolderTriple p q r] [Fact (1 ≤ p)] [Fact (1 ≤ q)] [Fact (1 ≤ r)]
    (B : E →L[𝕜] F →L[𝕜] G)

def MeasureTheory.Lp.applyBilinear : Lp E p μ →L[𝕜] Lp F q μ →L[𝕜] Lp G r μ :=
  LinearMap.mkContinuous₂
    (LinearMap.mk₂ 𝕜 (fun e f ↦ Memℒp.toLp (fun x ↦ B (e x) (f x)) sorry) sorry sorry sorry sorry)
    ‖B‖
    sorry

[Anatole Dedecker]

Related issue: #6108

[Jireh Loreaux]

Anatole, the links in #6108 are broken. Do you remember what you were referencing exactly?

[Jireh Loreaux]

I guess the lemma was docs#MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm

[Jireh Loreaux]

(deleted)

[Jireh Loreaux]

I've created #21792 to address #6108 and now #21583 depends on this. In addition, #21583 implements the convolution-style bilinear map approach, and uses it to get the map Lp (Dual 𝕜 E) p μ →L[𝕜] Dual 𝕜 (Lp E q μ). Finally, I switch from mul to smul, but I left it as a separate construction (i.e., I did not use the bilinear map construction) because it is possible to get slightly more general results without it. If we decide this slight increase in generality isn't worth it, I can implement • via the bilinear map approach. It's close to the same amount of work either way.

There are probably still some missing simp lemmas, and perhaps some other small bits of clean-up before I would put it on the queue for review, but right now it's still marked RFC, so please comment.

[Anatole Dedecker]

I will look at this tomorrow, sorry for the delay.

[Jireh Loreaux]

I think I've converged on something pretty nice:

• #21854 implements the HolderTriple type class, and does nothing else
• #21792 generalizes the existing Hölder inequality results to more general continuous bilinear forms per #6108, and makes use of the new type class. (Sorry there was some variable shuffling here also.)
• #21583 puts it together and defines for B : E →L[𝕜] F →L[𝕜] a map B.holder : Lp p E μ → Lp q E μ → Lp r E μ, and upgrades it so a continuous linear map under appropriate hypotheses. It also defines an HSMul instance for Lp spaces.

[Jireh Loreaux]

no problem, I am in no rush.

[Anatole Dedecker]

I've just looked at the (now merged) #21792, and indeed I think it solves everything I had in mind when writing #6108 (although to be fair I don't remember exactly what the state of this file was at the time).

[Jireh Loreaux]

:ping_pong: on #21583. I think there's not much left to do here, unless someone says otherwise.