OAI/Probability/ClassicalON/PinnedBlocks.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ClassicalON.sum_fibers line 14
  2. theorem OAI.ClassicalON.prod_fibers line 20
  3. abbrev OAI.ClassicalON.BlockVertex line 25
  4. def OAI.ClassicalON.blockSpin line 27
  5. theorem OAI.ClassicalON.continuous_blockSpin line 32
  6. theorem OAI.ClassicalON.blockSpin_eq_glue line 46
  7. def OAI.ClassicalON.blockEnergy line 57
  8. def OAI.ClassicalON.blockBondWeight line 62
  9. def OAI.ClassicalON.blockBondMean line 68
  10. theorem OAI.ClassicalON.block_energy_sum line 75
  11. theorem OAI.ClassicalON.block_bond_product line 93
  12. theorem OAI.ClassicalON.poleBondMean_collapse line 110
  13. theorem OAI.ClassicalON.block_event_product line 125
  14. theorem OAI.ClassicalON.poleBondMean_blocks line 137