OAI/Analysis/KadisonSimilarity/Tracial/MatrixStageGrowth.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A full finite matrix stage has a minimal diagonal projection. This is the obstruction to a diffuse generated algebra stabilizing at a stage.

  1. theorem OAI.KadisonSimilarity.matrix_diagonal_no_proper_subprojection line 16
  2. theorem OAI.KadisonSimilarity.concreteStage_finrank line 46
  3. theorem OAI.KadisonSimilarity.concreteStage_size_le line 51
  4. theorem OAI.KadisonSimilarity.concreteStage_eq_of_size_eq line 59
  5. theorem OAI.KadisonSimilarity.generated_ne_stage_of_diffuse line 75
  6. theorem OAI.KadisonSimilarity.matrix_stage_sizes_cofinal line 127
  7. theorem OAI.KadisonSimilarity.matrix_stage_sizes_tendsto line 157

    Source documentation

    Diffuseness forces exactly the diverging matrix sizes needed in the finite-factor commutator argument.

    theorem matrix_stage_sizes_tendsto (F : ℕ → FiniteMatrixStage N)
    (hmono : Monotone (fun n => (F n).units.concreteAlgebra))
    (hdiff : ∀ p : (FiniteMatrixStage.generatedVonNeumann F).toStarSubalgebra,
      IsStarProjection p → p ≠ 0 → ∃ q, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧
        p * q = q ∧ q * p = q) :
    Filter.Tendsto (fun n => (Fintype.card (Fin (F n).size) : ℝ))
      Filter.atTop Filter.atTop := by
…