OAI/Analysis/KadisonSimilarity/Representation/NormalOrthogonalUnitaries.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The diffuse normal matrix source supplies the unitary sequence used in the free-factor center argument. The sequence consists of positive powers of the constructed full-corner Haar unitary.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_orthogonal_unitaries_of_normal_matrix_tower line 25

    Source documentation

    An actual centered orthogonal unitary family in the original source.

    theorem exists_orthogonal_unitaries_of_normal_matrix_tower
    (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (N : VonNeumannAlgebra H) (hN : G.left.range = N.toStarSubalgebra)
    (hsize : Filter.Tendsto (fun j => (Fintype.card (I j) : ℝ)) Filter.atTop Filter.atTop) :
    ∃ u : ℕ → unitary P, (∀ n, G.trace (u n : P) = 0) ∧
      ∀ i j, G.trace ((u i : P) * star (u j : P)) = if i = j then 1 else 0 := by
…