OAI/Analysis/KadisonSimilarity/Representation/ProperlyInfiniteStructure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Two orthogonal isometries yield every finite internal isometry row. The concrete Banach predual supplies the structural existence theorem.

  1. def OAI.KadisonSimilarity.binaryIsometryFamily line 14
  2. theorem OAI.KadisonSimilarity.binaryIsometryFamily_orthogonal line 18
  3. theorem OAI.KadisonSimilarity.internal_isometry_rows_of_no_finite_central_summand line 60
  4. theorem OAI.KadisonSimilarity.central_projection_zero_or_one line 73
  5. theorem OAI.KadisonSimilarity.no_finite_central_summand_of_infinite_factor line 88
  6. theorem OAI.KadisonSimilarity.internal_isometry_rows_of_infinite_factor line 111
  7. theorem OAI.KadisonSimilarity.infinite_factor_commutatorEstimate line 119

    Source documentation

    A properly infinite factor satisfies the complete commutator estimate.

    theorem infinite_factor_commutatorEstimate
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c)
    (hinfinite : ¬ FiniteAlgebra P.toStarSubalgebra) :
    CommutatorEstimate P (1 + 2 * (4 * Real.sqrt 2)) :=
…

    Mentions: OAI.KadisonSimilarity.CommutatorEstimate