OAI/Analysis/KadisonSimilarity/FreeProduct/DyadicHaarUnitary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A Haar unitary in each corner of a diffuse finite tracial von Neumann algebra, constructed as a norm limit of finite dyadic spectral sums.

  1. def OAI.KadisonSimilarity.dyadicUnitaryApprox line 24
  2. theorem OAI.KadisonSimilarity.dyadicUnitaryApprox_mem line 27
  3. theorem OAI.KadisonSimilarity.dyadicUnitaryApprox_step line 43
  4. theorem OAI.KadisonSimilarity.dyadicUnitaryApprox_cauchy line 51
  5. def OAI.KadisonSimilarity.dyadicCornerTrace line 58
  6. theorem OAI.KadisonSimilarity.trace_dyadicUnitaryApprox_pow line 68
  7. theorem OAI.KadisonSimilarity.exists_dyadicCornerHaar line 80

    Source documentation

    The constructed corner unitary has every nonzero integer moment zero. No Haar-unitary existence theorem is assumed.

    theorem exists_dyadicCornerHaar (p : AlgebraProjection M) :
    ∃ z : unitary (CStarCorner p.val p.property),
      ∀ k : ℤ, k ≠ 0 → τ.trace (haarCornerPower z k) = 0 := by
…

    Mentions: OAI.KadisonSimilarity.CStarCorner, OAI.KadisonSimilarity.haarCornerPower