OAI/Analysis/KadisonKastler/ProductCentralizerSmallProjections.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Small projections in the fixed product-state centralizer

The all-zero diagonal in a finite block of lambda sites is in the exact state centralizer. Its trace is (1 + lambda)⁻ⁿ, hence tends to zero.

  1. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_site_diagonal_mem_centralizer line 28
  2. theorem OAI.KadisonKastler.PointedMatrixSites.twoRatio_block_zero_mem_centralizer line 47
  3. def OAI.KadisonKastler.PointedMatrixSites.centralizerBlockZero line 56
  4. theorem OAI.KadisonKastler.PointedMatrixSites.centralizerBlockZero_trace line 64
  5. theorem OAI.KadisonKastler.PointedMatrixSites.lambda_block_zero_weight line 70
  6. theorem OAI.KadisonKastler.PointedMatrixSites.exists_small_centralizer_projection line 85

    Source documentation

    Nonzero exact centralizer projections with arbitrarily small faithful trace.

    theorem exists_small_centralizer_projection (ε : ℝ) (hε : 0 < ε) :
    ∃ p : AlgebraProjection (stateCentralizerVonNeumann (M := M) Ω),
…

    Mentions: OAI.KadisonKastler.stateCentralizerVonNeumann