Product of Euclidean spaces

Stream: Is there code for X?

[Michael Rothgang]

The following should be some fact about pi types (i.e., I would prove this first at that level, and then for PiLp): does mathlib really not have this yet?

def EuclideanSpace.prod (α β : Type*) :
    (EuclideanSpace ℝ α) × (EuclideanSpace ℝ β) ≃ EuclideanSpace ℝ (α ⊕ β) := sorry

(I'm interested in the corollary with α = Fin n and β = Fin m.)

[Floris van Doorn]

Isn't this docs#Equiv.sumArrowEquivProdArrow up to defeq? The Pi-version is docs#Equiv.sumPiEquivProdPi or docs#Equiv.prodPiEquivSumPi

[Floris van Doorn]

Found with

[Floris van Doorn]

@loogle Prod, Equiv, Sum

[loogle]

:search: Equiv.boolProdEquivSum, Equiv.sumArrowEquivProdArrow, and 61 more

[Floris van Doorn]

(it's not easy to search for Pi-types in Loogle, I think)

[Floris van Doorn]

docs#ContinuousLinearEquiv.sumPiEquivProdPi might also be relevant.

[Michael Rothgang]

Thanks, the first one did the trick!

[Eric Wieser]

I would guess you want WithLp on the LHS?

[Michael Rothgang]

I do in fact want a homeomorphism between these spaces, so I guess WithLp does help.

[Eric Wieser]

docs#LinearIsometryEquiv.piLpCurry may also be of interest

[Michael Rothgang]

I was just looking for that: this looks helpful, thanks!

[Eric Wieser]

Probably we should have LinearIsometryEquiv.sumPiLpEquivProdPiLp for the version you asked for

[Michael Rothgang]

That sounds exactly like what I need, indeed!

[Michael Rothgang]

Linking #22973 for posterity

[Eric Wieser]

Whoops, I'd forgotten that this is the second time this has been asked for

[Eric Wieser]

I've marked it "please adopt", since in the other thread about it I delegated filling the final two sorrys

[Jihoon Hyun]

The full proof has now been committed to #22973 !

[Eric Wieser]

The dependencies of that PR are now all resolved. Thanks for filling in the gaps, @Jihoon Hyun!

[Ben Eltschig]

I just came across this thread because I needed the exact thing Michael asked about - a continuous linear equivalence between EuclideanSpace 𝕜 (Fin (n + m)) and EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m). Using the equivalence from #22973, this is what I ended up with:

def EuclideanSpace.sumEquivProd (𝕜 : Type*) [RCLike 𝕜] (ι κ : Type*) [Fintype ι] [Fintype κ] :
    EuclideanSpace 𝕜 (ι ⊕ κ) ≃L[𝕜] EuclideanSpace 𝕜 ι × EuclideanSpace 𝕜 κ :=
  (PiLp.sumPiLpEquivProdLpPiLp 2 _).toContinuousLinearEquiv.trans <|
    WithLp.prodContinuousLinearEquiv _ _ _ _

def EuclideanSpace.finAddEquivProd {𝕜 : Type*} [RCLike 𝕜] {n m : ℕ} :
    EuclideanSpace 𝕜 (Fin (n + m)) ≃L[𝕜] EuclideanSpace 𝕜 (Fin n) × EuclideanSpace 𝕜 (Fin m) :=
  (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 finSumFinEquiv.symm).toContinuousLinearEquiv.trans <|
    sumEquivProd 𝕜 _ _

Would it be a good idea to PR these two as well? They're not too hard to obtain from what's already there, but since this seems to be a relatively common scenario, maybe it's good to have them nonetheless

[Eric Wieser]

I think I'd claim these are more useful in the isometry forms we already somewhat have

[Eric Wieser]

Do we have the pieces to get the second one as an isometry?

[Ben Eltschig]

The second one isn't an isometry because binary products carry the supremum norm, just like arbitrary products do

[Ben Eltschig]

neither is the first

[Ben Eltschig]

For what I'm doing continuity suffices because all continuous linear maps between normed spaces are smooth - I assume that's the reason Michael needed continuity as well

[Jihoon Hyun]

They are also measurable equivalent, so I was planning to add that version of #22973 in the near future.

[Eric Wieser]

I'm aware that they're only isometries with an extra WithLp

[Ben Eltschig]

Right, sorry. I misinterpreted your question there

[Ben Eltschig]

It should be easy to get that second lemma as an isometry with an extra WithLp on the rhs - though the other form is more useful to me

[Michael Rothgang]

Cross-linking some discussion here