OAI/Probability/UnimodularPercolation/Criticality/Operator.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Critical boundedness of the percolation operator under unimodularity and simple edge indexing.

  1. def OAI.Percolation.criticalApproach line 19
  2. theorem OAI.Percolation.criticalApproach_half line 26
  3. theorem OAI.Percolation.criticalApproach_lt line 32
  4. theorem OAI.Percolation.criticalApproach_gap line 37
  5. theorem OAI.Percolation.log_sublinear_of_geometric_gap line 44
  6. theorem OAI.Percolation.critical_bounded_of_fixed_data line 68
  7. theorem OAI.Percolation.nonempty_bonds_of_connected line 132
  8. theorem OAI.Percolation.critical_bounded_of_transport_finiteness line 144
  9. def OAI.Percolation.AutUnimodular line 195
  10. theorem OAI.Percolation.critical_bounded_of_unimodular_finiteness line 203
  11. theorem OAI.Percolation.critical_finite_of_unimodular line 223
  12. theorem OAI.Percolation.critical_bounded_of_unimodular line 243
  13. theorem OAI.Percolation.critical_operator line 262