OAI/Analysis/FactorGeneration/MatrixRefinement.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

A normal element of a diffuse finite factor has L2 approximations in constructed full dyadic matrix algebras. No prescribed MASA is needed.

  1. theorem OAI.Generator.Tracial.exists_normal_matrix_approximation line 22
  2. theorem OAI.Generator.Tracial.commutator_norm₂_bound line 56
  3. theorem OAI.Generator.Tracial.commutator_norm₂_approximation line 64
  4. theorem OAI.Generator.Tracial.expectation_energy_descent_of_unitary_approximation line 79
  5. theorem OAI.Generator.Tracial.exists_irreducible_matrix_energy_descent line 106
  6. theorem OAI.Generator.Tracial.conditionalExpectation_restricted line 157
  7. theorem OAI.Generator.MatrixUnitSystem.relative_antitone line 174
  8. theorem OAI.Generator.MatrixUnitSystem.relative_product_inside line 188

    Source documentation

    The product commutant is exactly the commutant of the new system inside of the old commutant, with both algebras represented on the same H.

    theorem relative_product_inside (E : MatrixUnitSystem ι M.toStarSubalgebra)
    (F : MatrixUnitSystem κ E.relativeVonNeumann.toStarSubalgebra)
    (hc : ∀ i j k l,Commute (E.entry i j)
      ((F.map (coordinateInclusion E.relativeVonNeumann_le)).entry k l)) :
    (E.product (F.map (coordinateInclusion E.relativeVonNeumann_le)) hc).relativeVonNeumann =
      F.relativeVonNeumann := by
…

    Mentions: OAI.Generator.MatrixUnitSystem, OAI.Generator.MatrixUnitSystem.relativeVonNeumann

  9. theorem OAI.Generator.Tracial.exists_compatible_matrix_energy_descent line 221
  10. def OAI.Generator.MatrixUnitSystem.reindex line 289
  11. theorem OAI.Generator.MatrixUnitSystem.reindex_algebra line 295
  12. theorem OAI.Generator.MatrixUnitSystem.map_algebra_mono line 308
  13. theorem OAI.Generator.MatrixUnitSystem.mapped_reindex_relative line 321
  14. theorem OAI.Generator.Tracial.exists_commuting_matrix_extension line 338