OAI/Analysis/KadisonSimilarity/Tracial/NormalSmallCorners.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Construct small diffuse corners in the original algebra through its actual faithful normal range, then transport the entire frame back.

  1. def OAI.KadisonSimilarity.TracialCornerGeometry.normalMatrixTower line 26

    Source documentation

    The same full-matrix tower in the concrete normal coordinates.

    def normalMatrixTower (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (N : VonNeumannAlgebra H) (hN : G.left.range = N.toStarSubalgebra) :
    let τ := G.normalTracialRepresentation h1 hf N hN
…
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.normalRange_diffuse_of_matrix_tower line 56

    Source documentation

    The normal represented source has no nonzero minimal projection.

    theorem normalRange_diffuse_of_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) :
    ∀ p : N.toStarSubalgebra, IsStarProjection p → p ≠ 0 →
      ∃ q : N.toStarSubalgebra, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧
        p * q = q ∧ q * p = q := by
…
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.exists_smallFreeCornerData_of_normal_matrix_tower line 86

    Source documentation

    All small-frame, half-projection and Haar data are constructed together.

    theorem exists_smallFreeCornerData_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)
    {s : ℝ} (hs : 0 < s) : Nonempty (SmallFreeCornerData G.trace s) := by
…

    Mentions: OAI.KadisonSimilarity.SmallFreeCornerData