47 lines
1.1 KiB
Plaintext
47 lines
1.1 KiB
Plaintext
import Mathlib.Analysis.InnerProductSpace.PiL2
|
||
|
||
|
||
open RCLike Real Filter
|
||
open Topology ComplexConjugate
|
||
open LinearMap (BilinForm)
|
||
open TensorProduct
|
||
open InnerProductSpace
|
||
open Inner
|
||
|
||
|
||
example
|
||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
|
||
{F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
|
||
: 1 = 0 := by
|
||
|
||
let e : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := innerₗ E
|
||
let f : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₗ F
|
||
let e₂ := TensorProduct.map₂ e f
|
||
let l := TensorProduct.lid ℝ ℝ
|
||
|
||
have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) =
|
||
|
||
let X : InnerProductSpace.Core ℝ (E ⊗[ℝ] F) := {
|
||
inner := by
|
||
intro a b
|
||
exact TensorProduct.lid ℝ ℝ ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
|
||
conj_symm := by
|
||
simp
|
||
intro x y
|
||
|
||
unfold innerₗ
|
||
|
||
simp
|
||
sorry
|
||
nonneg_re := _
|
||
definite := _
|
||
add_left := _
|
||
smul_left := _
|
||
}
|
||
|
||
let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 :=
|
||
--let x := TensorProduct.lift
|
||
--E.inner
|
||
--TensorProduct.map₂
|
||
sorry
|
||
sorry |