Diamond with `EuclideanSpace` (`PiLp`)

Stream: mathlib4

[Jihoon Hyun]

Here is my attempt to solve the problem:

import Mathlib

open MeasureTheory

example
    {ι : Type*} [Fintype ι] {κ : Type*} [Fintype κ]
    {f : EuclideanSpace ℝ (ι ⊕ κ) → ℝ} (hf : Integrable f) :
    let e :
        EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
      PiLp.sumPiLpEquivProdLpPiLp _ _
    Integrable (f ∘ e.symm) := sorry

This produces an error failed to synthesize MeasureSpace (WithLp 2 (EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ))).
In order to handle this, I add an instance and continue.

import Mathlib

open MeasureTheory

instance {α : Type*} [MeasureSpace α] {p : ENNReal} [Fact (1 ≤ p)] :
    MeasureSpace (WithLp p α) :=
  ‹MeasureSpace α›

example
    {ι : Type*} [Fintype ι] {κ : Type*} [Fintype κ]
    {f : EuclideanSpace ℝ (ι ⊕ κ) → ℝ} (hf : Integrable f) :
    let e :
        EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
      PiLp.sumPiLpEquivProdLpPiLp _ _
    Integrable (f ∘ e.symm) := by
  refine (integrable_comp _ f).mpr hf
  sorry

Now there is an issue with integrable_comp, that instances under volume do not match.
Maybe we don't need MeasureSpace (WithLp p α), so let's replace with MeasureSpace (Euclidean ℝ ι)..

import Mathlib

open MeasureTheory

noncomputable instance {ι : Type*} [Fintype ι] : MeasureSpace (EuclideanSpace ℝ ι) :=
  inferInstance

example
    {ι : Type*} [Fintype ι] {κ : Type*} [Fintype κ]
    {f : EuclideanSpace ℝ (ι ⊕ κ) → ℝ} (hf : Integrable f) :
    let e :
        EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
      PiLp.sumPiLpEquivProdLpPiLp _ _
    Integrable (f ∘ e.symm) := by
  refine (integrable_comp ?_ f).mpr hf
  sorry

Now it fails to synthesize MeasureSpace (WithLp 2 (EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ))) again.
This implies we need to generate MeasureSpace (WithLp 2 _).

import Mathlib

open MeasureTheory

noncomputable instance {α : Type*} [MeasureSpace α] : MeasureSpace (WithLp 2 α) :=
  ‹MeasureSpace α›

example
    {ι : Type*} [Fintype ι] {κ : Type*} [Fintype κ]
    {f : EuclideanSpace ℝ (ι ⊕ κ) → ℝ} (hf : Integrable f) :
    let e :
        EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
      PiLp.sumPiLpEquivProdLpPiLp _ _
    Integrable (f ∘ e.symm) := by
  refine (integrable_comp ?_ f).mpr hf
  sorry

Now integrable_comp gives an error again. Now I'm lost.

Is this related to the diamond mentioned in docs#measureSpaceOfInnerProductSpace ?

[Eric Wieser]

Certainly measureSpaceOfInnerProductSpace is the problem, there are other threads about it causing diamonds too I think

[Eric Wieser]

This works:

import Mathlib

open MeasureTheory

noncomputable instance {α : Type*} [MeasurableSpace α] {p : ENNReal} [Fact (1 ≤ p)] :
    MeasurableSpace (WithLp p α) :=
  ‹MeasurableSpace α›

noncomputable instance {α β : Type*}
    [TopologicalSpace α] [MeasurableSpace α] [BorelSpace α]
    [TopologicalSpace β] [MeasurableSpace β] [BorelSpace β]
    [SecondCountableTopologyEither α β] {p : ENNReal} [Fact (1 ≤ p)] :
    BorelSpace (WithLp p (α × β)) :=
  inferInstanceAs <| BorelSpace (α × β)

example
    {ι : Type*} [Fintype ι] {κ : Type*} [Fintype κ]
    {f : EuclideanSpace ℝ (ι ⊕ κ) → ℝ} (hf : Integrable f) :
    let e :
        EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
      PiLp.sumPiLpEquivProdLpPiLp _ _
    Integrable (f ∘ e.symm) := by
  let e :
      EuclideanSpace ℝ (ι ⊕ κ) ≃ₗᵢ[ℝ] WithLp 2 ((EuclideanSpace ℝ ι) × (EuclideanSpace ℝ κ)) :=
    PiLp.sumPiLpEquivProdLpPiLp _ _
  exact (integrable_comp e.symm f).mpr hf

[Yury G. Kudryashov]

CC: @Sébastien Gouëzel . Here, docs#measureSpaceOfInnerProductSpace conflicts with a natural instance [MeasureSpace α] : MeasureSpace (WithLp α).

[Sébastien Gouëzel]

The instance [MeasureSpace α] : MeasureSpace (WithLp α) is really bad: you expect the natural measure to be scaled naturally with the distance, so if you change the distance you should expect to also change the measure. For instance, Hausdorff measures change when you go from a space to its WithLp version. So, IMHO, the problem is not with the perfectly good instance docs#measureSpaceOfInnerProductSpace.

[Eric Wieser]

Is the MeasurableSpace instance above sensible?

[Eric Wieser]

If nothing else its docstring would be a great place to explain what you wrote there

[Eric Wieser]

Though for the sake of loogle, perhaps we should define a deprecated non-instance to hold that docstring?

[Yury G. Kudryashov]

I think that MeasurableSpace instance is good (+BorelSpace).

[Yury G. Kudryashov]

Wait

[Jihoon Hyun]

Actually there's a problem with this approach also. I'll give an example soon.
Sorry, I figured out that the problem I had is probably not related to this diamond.

[Yury G. Kudryashov]

If we go forward and redefine the norm on Lp spaces (+WithLp spaces) for p < 1, then for p = 0 we'll get a topology that isn't equal to the underlying topology.

[Eric Wieser]

(I'll note that I have a branch that tries to generalize some theorems / instances for p = 0)

[Yury G. Kudryashov]

I think that we should turn WithLp into a structure to be sure that we don't leak defeq.

[Yury G. Kudryashov]

But this is probably offtopic here.