OAI/Probability/BenjaminiSchramm/GhostCluster.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalPercolation.BondGraph.quarterGhostWeight line 15
  2. lemma OAI.CriticalPercolation.BondGraph.coe_quarterGhostWeight line 18
  3. lemma OAI.CriticalPercolation.BondGraph.quarterGhostWeight_change_base line 23
  4. lemma OAI.CriticalPercolation.BondGraph.quarterGhostField_change_base line 31
  5. lemma OAI.CriticalPercolation.BondGraph.quarterTiltedMass_finite_sum line 43
  6. lemma OAI.CriticalPercolation.BondGraph.quarterTiltedMass_toReal_finite_sum line 55
  7. lemma OAI.CriticalPercolation.BondGraph.ghost_hit_cluster_joint_measurable line 66
  8. theorem OAI.CriticalPercolation.BondGraph.quarterGhostField_hit_cluster line 72
  9. theorem OAI.CriticalPercolation.BondGraph.quarterTwoGhostField_hit_cluster line 80
  10. theorem OAI.CriticalPercolation.BondGraph.quarterGhostConnection_average line 90
  11. theorem OAI.CriticalPercolation.BondGraph.quarterGhostConnection_change_base line 123