Create `LinearIsometryEquiv` with `WithLp 2 (α × β)` and..

Stream: mathlib4

[Jihoon Hyun]

.. EuclideanSpace ℝ (Fin (Module.finrank ℝ α + Module.finrank ℝ β))

I want to fill in the sorry in this code, which will give a nice connection between Euclidean spaces and their products.
However, the difficult part is, I couldn't figure out how to make instances, like SeminormedAddCommGroup (WithLp 2 (α × β)) for example.
May I get some help?

import Mathlib

abbrev euclideanProd
    (α : Type*) [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [T2Space α]
    [Module ℝ α] [ContinuousSMul ℝ α] [FiniteDimensional ℝ α]
    (β : Type*) [AddCommGroup β] [TopologicalSpace β] [IsTopologicalAddGroup β] [T2Space β]
    [Module ℝ β] [ContinuousSMul ℝ β] [FiniteDimensional ℝ β] :=
  WithLp 2 (α × β)

@[inherit_doc] infixl:35 " ×ₑ " => euclideanProd

namespace EuclideanProd

variable {α : Type*} [AddCommGroup α] [TopologicalSpace α] [IsTopologicalAddGroup α] [T2Space α]
variable [Module ℝ α] [ContinuousSMul ℝ α] [FiniteDimensional ℝ α]
variable {β : Type*} [AddCommGroup β] [TopologicalSpace β] [IsTopologicalAddGroup β] [T2Space β]
variable [Module ℝ β] [ContinuousSMul ℝ β] [FiniteDimensional ℝ β]

section Instances

instance : AddCommGroup (α ×ₑ β) :=
  WithLp.instAddCommGroup 2 _

instance : TopologicalSpace (α ×ₑ β) :=
  WithLp.instProdTopologicalSpace 2 _ _

instance : IsTopologicalAddGroup (α ×ₑ β) :=
  Prod.instIsTopologicalAddGroup

instance : T0Space (α ×ₑ β) :=
  WithLp.instProdT0Space 2 _ _

instance : R1Space (α ×ₑ β) :=
  instR1SpaceProd

instance : T2Space (α ×ₑ β) :=
  instT2SpaceOfR1SpaceOfT0Space

instance : Module ℝ (α ×ₑ β) :=
  WithLp.instModule 2 _ _

instance : ContinuousSMul ℝ (α ×ₑ β) :=
  Prod.continuousSMul

instance : FiniteDimensional ℝ (α ×ₑ β) :=
  WithLp.instModuleFinite 2 _ _

instance : MeasurableSpace (α ×ₑ β) :=
  borel (α ×ₑ β)

instance : BorelSpace (α ×ₑ β) :=
  ⟨rfl⟩

end Instances

@[simp]
theorem finrank_eq_finrank_add_finrank :
    Module.finrank ℝ (α ×ₑ β) = Module.finrank ℝ α + Module.finrank ℝ β := by
  rw [← Module.finrank_prod]; rfl

noncomputable def toEuclidean :
    (α ×ₑ β) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin (Module.finrank ℝ α + Module.finrank ℝ β)) :=
  sorry

end EuclideanProd

[Eric Wieser]

Here's a start:

import Mathlib

universe u
variable {ι κ} (α : ι ⊕ κ → Type*) {p : ENNReal} {R}
variable [NormedField R] [∀ i, NormedAddCommGroup (α i)]
variable [∀ i, NormedSpace R (α i)] [Fintype ι] [Fintype κ] [Fact (1 ≤ p)]

def WithLp.sumPiEquivProdPi : WithLp p (Π i, α i) ≃ₗᵢ[R] WithLp p (WithLp p (Π i, α (.inl i)) × WithLp p (Π i, α (.inr i))) where
  __ :=
    WithLp.equiv p _
      |>.trans <| Equiv.sumPiEquivProdPi α
      |>.trans <| Equiv.prodCongr (WithLp.equiv p _).symm (WithLp.equiv p _).symm
      |>.trans <| (WithLp.equiv p _).symm
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  norm_map' := (WithLp.equiv p _).symm.surjective.forall.2 fun x => by
    rename_i src
    obtain rfl | hp := p.dichotomy
    · simp [src]
      sorry
    · sorry

[Eric Wieser]

I'll start a PR since I know where to put this, but perhaps leave the sorries to you?

[Jihoon Hyun]

If you're busy or if you don't mind me filling sorries!

[Eric Wieser]

#22973

[Eric Wieser]

(edited in the PR; the sorries should be easy now, though might justify a new lemma)

[Jihoon Hyun]

Thanks for the huge effort! Still, I'm struggling with instances here.

I'd like to make an measurable equivalence WithLp p (ι ⊕ κ) ≃ᵐ[𝕜] WithLp p ((WithLp p ι) × (WithLp p κ)).
I thought I could simply use LinearIsometryEquiv.toMeasurableEquiv, but there is no instance MeasurableSpace (WithLp p (EuclideanSpace ℝ ι × EuclideanSpace ℝ κ)).
I couldn't define the instance with borel _, since BorelSpace (WithLp p (EuclideanSpace ℝ ι × EuclideanSpace ℝ κ)) is not constructed using rfl, which I think it should.
Could you suggest a solution for this?

[Eric Wieser]

@loogle MeasurableSpace, WithLp

[loogle]

:shrug: nothing found

[Eric Wieser]

@loogle MeasurableSpace, EuclideanSpace

[Eric Wieser]

docs#EuclideanSpace.instMeasurableSpaceReal should generalize trivially to Prod