OAI/Probability/UnimodularPercolation/Criticality/Phase.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Strict operator-threshold gaps and infinite-cluster phase classification.

  1. theorem OAI.Percolation.strict_gap_of_critical_bounded line 18
  2. theorem OAI.Percolation.unique_probability_zero_of_lt_pu line 43
  3. theorem OAI.Percolation.finite_count_empty_ae_of_lt_pu line 57
  4. theorem OAI.Percolation.infinitely_many_of_pc_lt_lt_pu line 94