Lacking theorems involving `Measure`, `Prod` and `WithLp`

Stream: mathlib4

[Jihoon Hyun]

There are few theorems which relates Measure or Integral with WithLp (\a \times \b). One notable example is the integral in the product WithLp space:

import Mathlib

open MeasureTheory

-- Fubini's theorem on `WithLp` space
-- This is not good as the theorem uses `MeasureTheory.Measure.prod`.
-- Instead `hf` should use a product of measures designed for `WithLp`.
theorem WithLp.integral_prod
    {α : Type*} [MeasurableSpace α]
    {β : Type*} [MeasurableSpace β]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    {p : ENNReal} [Fact (1 ≤ p)]
    {μ : Measure (WithLp p α)} [SFinite μ]
    {ν : Measure (WithLp p β)} [SFinite ν]
    (f : WithLp p (WithLp p α × WithLp p β) → E) (hf : Integrable f (μ.prod ν)) :
    ∫ (z : WithLp p (WithLp p α × WithLp p β)), f z ∂μ.prod ν =
    ∫ (x : WithLp p α), ∫ (y : WithLp p β), f (x, y) ∂ν ∂μ :=
  MeasureTheory.integral_prod f hf

I strongly believe that removing the diamond is necessary to prove theorems about EuclideanSpace without similar problems.

[Yury G. Kudryashov]

There was a recent discussion of this topic.

[Yury G. Kudryashov]

What exactly are you trying to prove?

[Yury G. Kudryashov]

What are α and β in the case you care about?

[Yury G. Kudryashov]

It's strange to see WithLp p (WithLp p α × WithLp p β). Does it naturally appear in some context?

[Jihoon Hyun]

Yury G. Kudryashov 말함:

It's strange to see WithLp p (WithLp p α × WithLp p β). Does it naturally appear in some context?

This happens when multiplying two Euclidean spaces, so WithLp p _ are PiLps.

Yury G. Kudryashov 말함:

What exactly are you trying to prove?

@Jineon Baek , @Jaehyeon Seo , @Hyojae Lim , I, and several others are currently formalizing the Brunn-Minkowski theorem here. Specifically, I'm proving the Prekopa-Leindler theorem, which uses the induction on dimension of Euclidean space. However I'm having a hard time proving it, mainly due to integrals and products of EuclideanSpace. As the formalization is almost done except my part, I'm asking if more helper theorems about WithLp (or EuclideanSpace) involving Prod and Measure can be proved.

[Yury G. Kudryashov]

Re: strange WithLps: I see.

[Yury G. Kudryashov]

What measure on WithLp do you have (coming from other parts of your construction)?

[Yury G. Kudryashov]

Is it volume on EuclideanSpace?

[Yury G. Kudryashov]

If yes, then you need a lemma saying that this measure is equal to the product of volumes.

[Yury G. Kudryashov]

(probably, with some no-op Measure.maps here and there)

[Jihoon Hyun]

Yury G. Kudryashov 말함:

Is it volume on EuclideanSpace?

Yes, and the only measure appearing in the theorem is volume (whatever the type is).

[Yury G. Kudryashov]

Then you need the following statement: if E and F are finite dimensional inner product spaces, then the volume on WithLp 2 (E × F) is the product of their volumes.

[Yury G. Kudryashov]

(up to a map along WithLp.equiv)

[Yury G. Kudryashov]

It would be nice to have a similar statement about PiLp of a family of inner product spaces too.

[Jihoon Hyun]

Yury G. Kudryashov 말함:

Then you need the following statement: if E and F are finite dimensional inner product spaces, then the volume on WithLp 2 (E × F) is the product of their volumes.

That's one of the lemmas I was looking for. As you suggested, I'll try to prove that again, but wouldn't that lead to the diamond?

[Yury G. Kudryashov]

E.g., you can choose an orthonormal basis in each space, then use them to construct an orthonormal basis on the product space. Both measures are Haar measures, and they will be equal to one on the parallelepiped corresponding to this basis, hence they're equal.

[Yury G. Kudryashov]

There is no diamond here, as E × F and WithLp 2 (E × F) are different spaces for the typeclass search.

[Yury G. Kudryashov]

(and I think that we should turn WithLp into a 1-field structure)

[Jihoon Hyun]

How about making a product which we are able to set the norm, and define the (currently normal) product as a specialization with an infinite norm?

[Yury G. Kudryashov]

How will it help? The volume on a euclidean space comes from an unspecified orthonormal basis.

[Jihoon Hyun]

I thought about it for a bit, and now I also think that my idea above won't help much.

[Eric Wieser]

We need the Prod version of docs#PiLp.volume_preserving_equiv

[Jihoon Hyun]

Yury G. Kudryashov 말함:

(and I think that we should turn WithLp into a 1-field structure)

So is there a plan to refactor WithLp and eventually remove a diamond?
This diamond will appear as mathlib grows, and if there is a clear insight that instance problems will disappear after the refactorization, then I'd like to work on it soon.

[Eric Wieser]

Making it a structure will not affect whether there is a diamond in mathlib, it will only make it harder for end users to introduce the diamond themselves by accident

[Yury G. Kudryashov]

Also, docs#PiLp.volume_preserving_equiv should be generalized to an indexed product of any inner product spaces, not necessarily $\mathbb R^n$.