OAI/Probability/UnimodularPercolation/TwoCluster/Score.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Decision-tree scores and influences for two-cluster events.

  1. theorem OAI.Percolation.ProbeTree.score_mean_zero line 19
  2. theorem OAI.Percolation.ProbeTree.score_second_moment line 40
  3. theorem OAI.Percolation.ProbeTree.score_abs_mean_le_sqrt line 68
  4. theorem OAI.Percolation.EdgeQueryTree.capped_score_abs_mean_le line 93
  5. theorem OAI.Percolation.incidenceSearch_abs_mean_le line 110
  6. def OAI.Percolation.finiteClusterScore line 125
  7. def OAI.Percolation.cappedDensity line 130
  8. theorem OAI.Percolation.cappedDensity_nonneg line 132
  9. theorem OAI.Percolation.cappedDensity_le_one line 136
  10. theorem OAI.Percolation.exists_four_scale line 142
  11. theorem OAI.Percolation.nat_le_four_pow line 152
  12. theorem OAI.Percolation.cappedDensity_le_four_scale line 157
  13. theorem OAI.Percolation.cappedDensity_score_le_stopped line 171
  14. theorem OAI.Percolation.sqrt_four_cap line 203
  15. theorem OAI.Percolation.cappedDensity_score_expectation_bound line 211
  16. theorem OAI.Percolation.incident_cluster_insert_iff line 258
  17. theorem OAI.Percolation.cluster_insert_eq_of_not_incident line 273
  18. theorem OAI.Percolation.finite_incident_insert_iff line 288
  19. theorem OAI.Percolation.finiteRootComponent_insert_eq_of_not_incident line 298
  20. theorem OAI.Percolation.finiteRootComponent_card_pos line 313
  21. theorem OAI.Percolation.cappedDensity_antitone line 321
  22. def OAI.Percolation.finiteDensity line 335
  23. def OAI.Percolation.finiteDensityInfluence line 338
  24. theorem OAI.Percolation.finiteDensityInfluence_nonneg line 342
  25. theorem OAI.Percolation.finiteDensityInfluence_le_one line 358
  26. theorem OAI.Percolation.finiteDensity_score_one_bit line 366
  27. theorem OAI.Percolation.finiteDensity_score_identity line 416
  28. theorem OAI.Percolation.finiteDensityInfluence_sum_bound line 442