Cartesian product of two Hilbert spaces

Stream: mathlib4

[Zhang Ruichong]

It is well known that if A and B a two Hilbert spaces, then A × B is a Hilbert space. So I want to prove this:

import Mathlib.LinearAlgebra.FiniteDimensional
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Basic
open InnerProductSpace
noncomputable section

variable {A B : Type _} [NormedAddCommGroup A] [NormedAddCommGroup B]
variable [InnerProductSpace ℝ A] [InnerProductSpace ℝ B]

def prod_inner (x y : A × B) : ℝ :=
  inner x.1 y.1 + inner x.2 y.2

instance prod_inner_product_space :
  InnerProductSpace ℝ (A × B) where
  inner := prod_inner

I'm completely stuck on this, I haven't found any relevant lemmas in Mathlib yet.
Do I really need to construct it by myself?

[Yaël Dillies]

See #6136

[Anatole Dedecker]

To explain a bit more: this issue has been discussed several times already, but the main problem is that, as currently stated, this is false. The reason is that, in mathlib, the default norm on A × B is $\Vert(a, b)\Vert = \max(\Vert a\Vert, \Vert b\Vert)$, not $\Vert(a, b)\Vert = (\Vert a\Vert^2 + \Vert b\Vert^2)^{\frac12}$. And in general this norm is not a Hilbert space norm at all.

[Anatole Dedecker]

The solution will be to use WithLp 2 (A × B), which will soon have the structure you are looking for

[Anatole Dedecker]

docs#WithLp

[Zhang Ruichong]

Anatole Dedecker said:

The solution will be to use WithLp 2 (A × B), which will soon have the structure you are looking for

Did you mean that it hasn't been implemented, and I have to wait for some time before implementation?

[Yaël Dillies]

Yes, the implementation is here, which is not part of mathlib yet.