OAI/Analysis/KadisonSimilarity/FreeProduct/AngularCutLimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Bounded convergence of the angular cut functions and the elementary identification of the limiting open angular arc.

  1. theorem OAI.KadisonSimilarity.angularIntegral_cut_tendsto line 14
  2. theorem OAI.KadisonSimilarity.cos_gt_iff_mem_open_arc line 47
  3. theorem OAI.KadisonSimilarity.angularIntegral_centered_cut line 55
  4. theorem OAI.KadisonSimilarity.angularIntegral_cut_eq line 75