OAI/Probability/FreeIsing/Trees/EdgePercolationLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.EdgePercolationLaw.edgeInterval line 11
  2. theorem OAI.Problem367.EdgePercolationLaw.measurableSet_edgeInterval line 14
  3. theorem OAI.Problem367.EdgePercolationLaw.uniform01_Iic line 18
  4. theorem OAI.Problem367.EdgePercolationLaw.uniform01_Ioi line 28
  5. theorem OAI.Problem367.EdgePercolationLaw.uniform01_edgeInterval line 38
  6. def OAI.Problem367.EdgePercolationLaw.cylinder line 46
  7. theorem OAI.Problem367.EdgePercolationLaw.measurableSet_cylinder line 50
  8. theorem OAI.Problem367.EdgePercolationLaw.infinitePi_cylinder line 54
  9. theorem OAI.Problem367.EdgePercolationLaw.infinitePi_all_open line 62
  10. theorem OAI.Problem367.EdgePercolationLaw.cylinder_of_measurePreserving line 72
  11. theorem OAI.Problem367.EdgePercolationLaw.all_open_of_measurePreserving line 81
  12. theorem OAI.Problem367.EdgePercolationLaw.joint_cylinder_of_measurePreserving line 90