Direct sum of inner product spaces

Stream: Is there code for X?

[Apurva Nakade]

Do we have an inner product space structure on the direct sum of finitely many inner product spaces?

[Apurva Nakade]

I also could not find direct sums of submodules of different modules.

Would it be useful to add these two to the library?

[Scott Morrison]

I don't think we want the second. If you want to take the direct sum of submodules of different modules, you should just forget they are submodules and take their direct sum as modules.

[Eric Wieser]

I think this is a good argument for dropping PiLp and replacing it with WithLp (Π i, A i), WithLp (A × B), WithLp (⊕ I, A I) etc

[Eric Wieser]

Though I imagine like Lex, it doesn't really deduplicate anything besides spelling

[Yaël Dillies]

I agree with you that this is the right design, though. I believe we already mentioned it a few months back.

[Apurva Nakade]

I'm stuck without an innerproduct structure on direct sums/products. I'll try to implement some minimal structure and see how it goes.

[Eric Wieser]

Can you just use the inner product on the correponding PiLp space instead?

[Apurva Nakade]

I'll read this file carefully and see if it helps.

The same suggests that these are products of L^p space. The proof I'm working on is for general Hilbert spaces though. They don't have a natural L^p norm on them.

[Eric Wieser]

Got it, your problem is that you have direct sums with finite support over an infinite space

[Apurva Nakade]

Exactly!

[Apurva Nakade]

I could restrict to finite dimensional spaces for now ...

[Apurva Nakade]

Where this comes up is that if $K$ is a cone in $V$ and $L$ is a cone in $W$ then $K \oplus L$ needs to be a cone in $V \oplus W$ and moreover we should get $(K \oplus L)^* \cong K^* \oplus L^*$. But to make sense of the duals, we need an inner product on $V \oplus W$.

[Apurva Nakade]

Here $V$ and $W$ are just Hilbert spaces.

[Eric Wieser]

Wait, do you mean a binary direct sum (docs#Prod) instead of docs#DirectSum ?

[Apurva Nakade]

Either should be fine tbh.

[Apurva Nakade]

I don't think I'll be taking direct sums over infinite indices, so the two are isomorphic for the case I need.

[Apurva Nakade]

Do we have an inner product space structure on docs#Prod of inner product spaces?

[Moritz Doll]

mathlib4#6136

[Apurva Nakade]

Perfect!! Thank you

[Kevin Buzzard]

Apurva Nakade said:

I don't think I'll be taking direct sums over infinite indices, so the two are isomorphic for the case I need.

Yes but they're not definitionally equal! So it still makes a big difference.

[Eric Wieser]

Eric Wieser said:

Though I imagine like Lex, it doesn't really deduplicate anything besides spelling

Actually this isn't true at all, it deduplicates all the boring code that copies across the module structure

[Eric Wieser]

So maybe we should make this refactor before #6136

[Yaël Dillies]

Sounds sensible to me

[Eric Wieser]

branch#eric-wieser/WithLp has a start, feel free to push further to it

[Anatole Dedecker]

Let me just indicate that the reason we don't have direct sums of inner product spaces is because in most cases what we really care about are Hilbert spaces, and in general the algebraic direct sum of Hilbert spaces is not an Hilbert space, and its completion is exactly docs#PiLp with p = 2

[Apurva Nakade]

Anatole Dedecker said:

Let me just indicate that the reason we don't have direct sums of inner product spaces is because in most cases what we really care about are Hilbert spaces, and in general the algebraic direct sum of Hilbert spaces is not an Hilbert space, and its completion is exactly docs#PiLp with p = 2

This is helpful, thanks! From the name at least I don't understand what docs#PiLp is - I thought this was a very specific metric space. I'll need to read more about this object and it's adjacent defs.