OAI/Analysis/BrownMeasure/Model.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.FiniteFactor.productHilbertNontrivial line 14

   Also declared: ComparatorChallenges/ProductBrown.lean:618 (same declaration text).

2. abbrev OAI.FiniteFactor.ProductOp line 73

   Also declared: ComparatorChallenges/ProductBrown.lean:678 (same declaration text).

3. def OAI.FiniteFactor.logarithmCutoff line 86

   Also declared: ComparatorChallenges/ProductBrown.lean:692 (same declaration text).

4. def OAI.FiniteFactor.FugledeKadisonDeterminant line 93

   Also declared: ComparatorChallenges/ProductBrown.lean:699 (same declaration text).

5. def OAI.FiniteFactor.expLogPotential line 117

   Also declared: ComparatorChallenges/ProductBrown.lean:723 (same declaration text).

6. def OAI.FiniteFactor.IsBrownMeasure line 120

   Also declared: ComparatorChallenges/ProductBrown.lean:726 (same declaration text).

7. def OAI.FiniteFactor.ProductBrownClaim line 132

   Also declared: ComparatorChallenges/ProductBrown.lean:738 (same declaration text).