OAI/Analysis/KadisonSimilarity/Constants.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The numerical constants fixed by the manuscript.

  1. def OAI.KadisonSimilarity.rowConstant line 12

    Also declared: ComparatorChallenges/KadisonSimilarity.lean:100 (same declaration text).

  2. def OAI.KadisonSimilarity.cyclicConstant line 13

    Also declared: ComparatorChallenges/KadisonSimilarity.lean:101 (same declaration text).

  3. def OAI.KadisonSimilarity.cornerConstant line 14

    Also declared: ComparatorChallenges/KadisonSimilarity.lean:102 (same declaration text).

  4. def OAI.KadisonSimilarity.factorConstant line 15

    Also declared: ComparatorChallenges/KadisonSimilarity.lean:103 (same declaration text).

  5. def OAI.KadisonSimilarity.universalConstant line 16

    Also declared: ComparatorChallenges/KadisonSimilarity.lean:104 (same declaration text).

  6. theorem OAI.KadisonSimilarity.rowConstant_pos line 18
  7. theorem OAI.KadisonSimilarity.cyclicConstant_pos line 20
  8. theorem OAI.KadisonSimilarity.one_le_cyclicConstant line 25
  9. theorem OAI.KadisonSimilarity.cornerConstant_pos line 29
  10. theorem OAI.KadisonSimilarity.finiteFactorConstant_le line 34
  11. theorem OAI.KadisonSimilarity.infiniteFactorConstant_le line 37
  12. theorem OAI.KadisonSimilarity.two_le_factorConstant line 40
  13. theorem OAI.KadisonSimilarity.factorConstant_pos line 42
  14. theorem OAI.KadisonSimilarity.universalConstant_pos line 44