OAI/Probability/InvariantIsing/Cavity/CavityRationalMass.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The rational count progression has exactly the prescribed normalized masses at every size, and its ordered block endpoints have exact limits.

  1. lemma OAI.InvariantIsing.cavityRationalCount_ratio line 14
  2. lemma OAI.InvariantIsing.cavityRationalDimension_tendsto line 22
  3. lemma OAI.InvariantIsing.cavityRationalStart line 28
  4. lemma OAI.InvariantIsing.cavityRationalStart_ratio line 32
  5. lemma OAI.InvariantIsing.cavityRationalEnd_ratio line 42
  6. lemma OAI.InvariantIsing.cavityRationalStart_alternative line 49
  7. lemma OAI.InvariantIsing.cavityRationalEnd_tendsto line 60