tensor product and inner product on linear maps and vectors

Stream: Is there code for X?

[Jam Kabeer Ali Khan]

Hi, I am trying to define a property on the inner product of tensor products of vectors and linear maps but I am struggling a bit

/-
This lemma shows the `Tensor` product property `(⟨φ₁|⨂⟨φ₂|)(A₁ ⨂ A₂)(|φ₁⟩⨂|φ₂⟩) = (⟨φ₁|A₁|φ₁⟩)·(⟨φ₂|A₂|φ₂⟩)`
-/
lemma tensor_product
  (φ₁ φ₂ : E)
  (A₁ A₂ : E →ₗ[𝕜] E)
  (_ : LinearMap.isPositiveSemiDefinite A₁)
  (_ : LinearMap.isPositiveSemiDefinite A₂)
  (h : ∀ x y x' y', inner 𝕜 (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y') :
  inner 𝕜 (φ₁ ⊗ₜ[𝕜] φ₂)
          ((TensorProduct.map A₁ A₂) (φ₁ ⊗ₜ[𝕜] φ₂)) =
    inner 𝕜 φ₁ (A₁ φ₁) * inner 𝕜 φ₂ (A₂ φ₂) := by
  sorry

it is not working properly, and I am getting the following errors:

failed to synthesize
  Inner 𝕜 (E ⊗[𝕜] E)

would appreciate any help if there is some relevant code in mathlib or whether i am misusing the tensor product! thank you!

[Aaron Liu]

This means Lean does not know how to take the inner product of the tensor, probably because you need to add an InnerProductSpace argument to your lemma.

[Aaron Liu]

Can you post a #mwe?

[Jam Kabeer Ali Khan]

sure! here a minimum example i could get

import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.Analysis.InnerProductSpace.Positive
import Mathlib.Analysis.InnerProductSpace.Projection
import Mathlib.LinearAlgebra.Trace

variable {𝕜 E : Type*} [RCLike 𝕜]
-- notation:100 T "⊗ₗ" N:100 => TensorProduct.map T N

variable? [HilbertSpace 𝕜 E] => [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
variable [FiniteDimensional 𝕜 E]
omit [CompleteSpace E]

namespace LinearMap

/-- Positive semidefinite operators. -/
def isPositiveSemiDefinite (T : E →ₗ[𝕜] E) : Prop :=
  IsSelfAdjoint T ∧ ∀ x, 0 ≤ RCLike.re (inner 𝕜 (T x) x)

end LinearMap

lemma tensor_product
  (φ₁ φ₂ : E)
  (A₁ A₂ : E →ₗ[𝕜] E)
  (_ : LinearMap.isPositiveSemiDefinite A₁)
  (_ : LinearMap.isPositiveSemiDefinite A₂)
  (h : ∀ x y x' y', inner 𝕜 (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') = inner 𝕜 x x' * inner 𝕜 y y') :
  inner 𝕜 (φ₁ ⊗ₜ[𝕜] φ₂)
          ((TensorProduct.map A₁ A₂) (φ₁ ⊗ₜ[𝕜] φ₂)) =
    inner 𝕜 φ₁ (A₁ φ₁) * inner 𝕜 φ₂ (A₂ φ₂) := by
  sorry

please let me know if this is not good, i will try to get a better one, i am still new to lean

[Aaron Liu]

The problem is that the inner product on tensor products has not been defined

[Aaron Liu]

I don't see it in mathlib anywhere...

[Jam Kabeer Ali Khan]

I see in that case I would need to define it myself? I am a bit new to lean, any word of advice on how should I go about this?

[Anatole Dedecker]

Aaron Liu said:

The problem is that the inner product on tensor products has not been defined

Indeed we don't have it. See #mathlib4 > Semilinearizing

[Eric Wieser]

Or #6020

[Iván Renison]

Hi
I saw the links in #6020, but I see that the definitions are for the reals instead of for RCLike.
They work using bilinearity and lifting, but I think that does not work for RCLike because the complex conjugate is not linear, and that makes the inner not lineal. Do you have any idea of how it could be done for RCLike?

[Frédéric Dupuis]

I think it shouldn't be too hard to generalize docs#TensorProduct.lift to the semilinear case, and then follow the same strategy.

[Iván Renison]

Ok, thanks for the hint