OAI/Analysis/FreeGroupFactor/Model.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.FreeGroupFactorMain.GroupHilbert line 13

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:13 (same declaration text).

2. abbrev OAI.FreeGroupFactorMain.GroupOperator line 14

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:14 (same declaration text).

3. def OAI.FreeGroupFactorMain.leftTranslations line 16

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:16 (same declaration text).

4. def OAI.FreeGroupFactorMain.groupVonNeumann line 19

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:19 (same declaration text).

5. def OAI.FreeGroupFactorMain.canonicalTrace line 23

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:23 (same declaration text).

6. def OAI.FreeGroupFactorMain.ultraweakOperatorTopology line 27

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:27 (same declaration text).

7. def OAI.FreeGroupFactorMain.groupUltraweakTopology line 34

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:34 (same declaration text).

8. abbrev OAI.FreeGroupFactorMain.FreeGroupRank line 39

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:39 (same declaration text).

9. instance OAI.FreeGroupFactorMain.groupVN_isClosed line 41

   Also declared: ComparatorChallenges/InterpolatedFactors.lean:41 (same declaration text).

10. instance OAI.FreeGroupFactorMain.groupVN_CStarAlgebra line 47

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:47 (same declaration text).

11. def OAI.FreeGroupFactorMain.Amplification.cornerSubalgebra line 61

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:61 (same declaration text).

12. abbrev OAI.FreeGroupFactorMain.Amplification.Corner line 78

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:78 (same declaration text).

13. instance OAI.FreeGroupFactorMain.Amplification.cornerClosed line 80

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:80 (same declaration text).

14. instance OAI.FreeGroupFactorMain.Amplification.cornerSemiring line 85

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:85 (same declaration text).

15. instance OAI.FreeGroupFactorMain.Amplification.cornerRing line 91

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:91 (same declaration text).

16. instance OAI.FreeGroupFactorMain.Amplification.cornerAlgebra line 95

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:95 (same declaration text).

17. instance OAI.FreeGroupFactorMain.Amplification.cornerNormedRing line 98

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:98 (same declaration text).

18. instance OAI.FreeGroupFactorMain.Amplification.cornerCStarAlgebra line 102

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

19. def OAI.FreeGroupFactorMain.Amplification.cornerTopology line 113

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:113 (same declaration text).

20. def OAI.FreeGroupFactorMain.Amplification.normalizedCornerTrace line 117

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:117 (same declaration text).

21. def OAI.FreeGroupFactorMain.Amplification.stabilizedRightTranslations line 122

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:122 (same declaration text).

22. def OAI.FreeGroupFactorMain.Amplification.stabilization line 126

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:126 (same declaration text).

23. instance OAI.FreeGroupFactorMain.Amplification.stabilization_isClosed line 129

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:129 (same declaration text).

24. instance OAI.FreeGroupFactorMain.Amplification.stabilization_CStarAlgebra line 134

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:134 (same declaration text).

25. def OAI.FreeGroupFactorMain.Amplification.stabilizedProjectionTrace line 137

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:137 (same declaration text).

26. def OAI.FreeGroupFactorMain.Amplification.stabilizedTrace line 142

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:142 (same declaration text).

27. def OAI.FreeGroupFactorMain.Amplification.stabilizationTopology line 147

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:147 (same declaration text).

28. structure OAI.FreeGroupFactorMain.Amplification.NormalTracialEquiv line 155

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:155 (same declaration text).

29. abbrev OAI.FreeGroupFactorMain.Interpolation.RankTwoProjection line 171

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:171 (same declaration text).

30. instance OAI.FreeGroupFactorMain.Interpolation.rankTwoProjectionInhabited line 173

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:173 (same declaration text).

31. def OAI.FreeGroupFactorMain.Interpolation.selectedProjection line 176

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:176 (same declaration text).

32. def OAI.FreeGroupFactorMain.Interpolation.interpolationScale line 179

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:179 (same declaration text).

33. inductive OAI.FreeGroupFactorMain.Interpolation.Model line 181

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:181 (same declaration text).

34. def OAI.FreeGroupFactorMain.Interpolation.Model.Algebra line 186

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:186 (same declaration text).

35. instance OAI.FreeGroupFactorMain.Interpolation.modelCStarAlgebra line 192

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:192 (same declaration text).

36. def OAI.FreeGroupFactorMain.Interpolation.Model.trace line 195

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:195 (same declaration text).

37. def OAI.FreeGroupFactorMain.Interpolation.Model.topology line 201

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:201 (same declaration text).

38. def OAI.FreeGroupFactorMain.Interpolation.parameterModel line 207

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:207 (same declaration text).

39. abbrev OAI.FreeGroupFactorMain.Interpolation.InterpolatedFactor line 212

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:212 (same declaration text).

40. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedTrace line 213

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:213 (same declaration text).

41. abbrev OAI.FreeGroupFactorMain.Interpolation.interpolatedTopology line 214

    Also declared: ComparatorChallenges/InterpolatedFactors.lean:214 (same declaration text).

42. def OAI.FreeGroupFactorMain.HasNormalTracialIso line 222