OAI/Probability/InvariantIsing/Cavity/CavityAffineCounts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Fixed integer offsets in the block counts cover every residue class of physical dimensions without changing the limiting rational masses.

  1. def OAI.InvariantIsing.cavityAffineCount line 14
  2. def OAI.InvariantIsing.cavityAffineSize line 17
  3. lemma OAI.InvariantIsing.cavityAffineCount_sum line 20
  4. lemma OAI.InvariantIsing.cavityAffineSize_tendsto line 25
  5. lemma OAI.InvariantIsing.cavityAffineCount_tendsto line 29
  6. lemma OAI.InvariantIsing.cavityAffineSize_ge_three line 34
  7. lemma OAI.InvariantIsing.cavityAffineSize_succ line 38
  8. lemma OAI.InvariantIsing.cavity_affine_ratio_tendsto line 43
  9. lemma OAI.InvariantIsing.cavityAffineCount_ratio line 62
  10. lemma OAI.InvariantIsing.cavityAffineStart line 68
  11. lemma OAI.InvariantIsing.cavityAffineStart_ratio line 74
  12. lemma OAI.InvariantIsing.cavityAffineEnd_ratio line 82