OAI/Probability/InvariantIsing/Core/FiniteIndexDistribution.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The positive part of a finite random label has the same distribution.

  1. def OAI.InvariantIsing.finiteIndexWeight line 15

    Distinct definitions of this name: ComparatorChallenges/InvariantIsing.lean:173 (different declaration text). Qualify references as OAI.InvariantIsing.finiteIndexWeight@path.

  2. lemma OAI.InvariantIsing.finiteIndexWeight_sum line 18
  3. lemma OAI.InvariantIsing.ae_finiteIndexWeight_pos line 25
  4. lemma OAI.InvariantIsing.positiveIndexWeight line 38
  5. lemma OAI.InvariantIsing.finiteIndex_map line 49