OAI/Probability/UnimodularPercolation/Kernel/Sprinkling.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Sprinkling estimates for finite and infinite graph operators.

  1. def OAI.Percolation.sprinkleParameter line 18
  2. def OAI.Percolation.pairParameter line 24
  3. theorem OAI.Percolation.map_bool_or line 26
  4. def OAI.Percolation.fieldLaw line 61
  5. def OAI.Percolation.fieldUnion line 64
  6. theorem OAI.Percolation.measurable_fieldUnion line 66
  7. theorem OAI.Percolation.map_fieldUnion line 77
  8. theorem OAI.Percolation.fieldLaw_map_pair line 118
  9. theorem OAI.Percolation.law_map_union line 125
  10. theorem OAI.Percolation.exists_operator_of_row_column_bound line 147
  11. theorem OAI.Percolation.Along.first_outside line 228
  12. theorem OAI.Percolation.conn_first_outside line 247
  13. theorem OAI.Percolation.law_map_preimage_embedding line 275
  14. theorem OAI.Percolation.exists_orParameter_small line 295
  15. theorem OAI.Percolation.conn_map_edges line 314
  16. theorem OAI.Percolation.finiteWitness_inter line 328
  17. def OAI.Percolation.colorInclusion line 337
  18. def OAI.Percolation.baseColors line 340
  19. def OAI.Percolation.baseField line 342
  20. theorem OAI.Percolation.not_mem_baseColors line 345
  21. theorem OAI.Percolation.fst_inter_baseColors line 356
  22. theorem OAI.Percolation.measurable_baseField line 368
  23. theorem OAI.Percolation.law_map_baseField line 374
  24. def OAI.Percolation.dartSource line 385
  25. def OAI.Percolation.dartTarget line 387
  26. theorem OAI.Percolation.exists_dart line 390
  27. theorem OAI.Percolation.colored_conn_probability line 397
  28. theorem OAI.Percolation.base_conn_probability line 409
  29. theorem OAI.Percolation.twoPoint_or_succ_le line 423
  30. def OAI.Percolation.edgeVertices line 486
  31. theorem OAI.Percolation.mem_edgeVertices line 489
  32. theorem OAI.Percolation.conn_eq_or_mem_edgeVertices line 492
  33. theorem OAI.Percolation.operatorBounded_finite_edges line 500
  34. theorem OAI.Percolation.dart_edge line 528
  35. theorem OAI.Percolation.card_darts_at_source line 535
  36. theorem OAI.Percolation.card_darts_at_target line 549
  37. def OAI.Percolation.adjacencyOperator line 564
  38. theorem OAI.Percolation.adjacencyOperator_apply line 569
  39. theorem OAI.Percolation.adjacencyOperator_norm_le line 575
  40. theorem OAI.Percolation.finite_sprinkling_bound line 628
  41. theorem OAI.Percolation.twoPoint_restrict_edges line 699
  42. theorem OAI.Percolation.twoPoint_restrict_le line 719
  43. theorem OAI.Percolation.degree_restrict_le line 725
  44. theorem OAI.Percolation.sprinkling_bound line 738
  45. theorem OAI.Percolation.operatorBounded_open_right line 786
  46. theorem OAI.Percolation.mainConclusion_of_critical_bounded line 821