OrthogonalConstantPairing.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded vector has zero constant pairing with an infinite orthogonal family of fixed norm. This is the Hilbert-space step of the free-factor center argument.

theorem OAI.KadisonSimilarity.orthonormal_constant_pairing_eq_zero line 15

theorem OAI.KadisonSimilarity.orthogonal_constant_pairing_eq_zero line 27

Source documentation

The family need not be normalized before applying the argument.

theorem orthogonal_constant_pairing_eq_zero (v : ℕ → H) (κ : ℝ)
    (hv : ∀ i j, inner ℂ (v i) (v j) = if i = j then (κ : ℂ) ^ 2 else 0)
    (x : H) (z : ℂ) (hz : ∀ n, inner ℂ (v n) x = z) : z = 0 := by
…