OAI/Analysis/FreeEntropy/Model.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.FiniteEntropySeparation.TracialVector line 13

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

2. def OAI.FiniteEntropySeparation.trace line 20

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:21 (same declaration text).

3. def OAI.FiniteEntropySeparation.wordEval line 23

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:24 (same declaration text).

4. def OAI.FiniteEntropySeparation.wordMoment line 26

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

5. def OAI.FiniteEntropySeparation.FreeSubalgebras line 29

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:30 (same declaration text).

6. def OAI.FiniteEntropySeparation.FreeStandardNoise line 37

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:38 (same declaration text).

7. def OAI.FiniteEntropySeparation.polynomialL2 line 45

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:46 (same declaration text).

8. def OAI.FiniteEntropySeparation.derivativeMoment line 49

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:50 (same declaration text).

9. def OAI.FiniteEntropySeparation.ConjugateSystem line 54

   Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:55 (same declaration text).

10. def OAI.FiniteEntropySeparation.freeFisher line 59

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:60 (same declaration text).

11. def OAI.FiniteEntropySeparation.heatTuple line 63

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:64 (same declaration text).

12. def OAI.FiniteEntropySeparation.chiStar line 66

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:67 (same declaration text).

13. abbrev OAI.FiniteEntropySeparation.MatrixCoordinates line 74

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:75 (same declaration text).

14. def OAI.FiniteEntropySeparation.hermitianMatrix line 76

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:77 (same declaration text).

15. def OAI.FiniteEntropySeparation.matrixOpNorm line 82

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:83 (same declaration text).

16. def OAI.FiniteEntropySeparation.matrixMoment line 85

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:86 (same declaration text).

17. def OAI.FiniteEntropySeparation.microstates line 88

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:89 (same declaration text).

18. def OAI.FiniteEntropySeparation.chiCutoff line 93

    Also declared: ComparatorChallenges/FiniteEntropySeparation.lean:94 (same declaration text).

19. def OAI.FiniteEntropySeparation.chi line 101

    Distinct definitions of this name: ComparatorChallenges/FiniteEntropySeparation.lean:102 (same statement text; different proof or body). Qualify references as OAI.FiniteEntropySeparation.chi@path.