OAI/Probability/UnimodularPercolation/Kernel/Bounds.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Kernel domination, monotone couplings and endpoint bounds.

  1. theorem OAI.Percolation.no_positive_lower_bound line 20
  2. theorem OAI.Percolation.not_operatorBounded_of_positive_column line 32
  3. theorem OAI.Percolation.not_operatorBounded_one line 43
  4. theorem OAI.Percolation.operatorNorm_one line 50
  5. def OAI.Percolation.finiteEmbedding line 62
  6. theorem OAI.Percolation.finiteEmbedding_single line 65
  7. theorem OAI.Percolation.finiteEmbedding_dense line 69
  8. theorem OAI.Percolation.exists_operator_of_matrix_tendsto line 80
  9. theorem OAI.Percolation.measurableSet_conn line 124
  10. instance OAI.Percolation.labelLaw_isProbabilityMeasure line 161
  11. theorem OAI.Percolation.measurable_threshold line 166
  12. theorem OAI.Percolation.map_threshold line 171
  13. theorem OAI.Percolation.map_openEdges line 192
  14. theorem OAI.Percolation.finiteEmbedding_apply line 211
  15. def OAI.Percolation.positivePart line 221
  16. theorem OAI.Percolation.positivePart_apply line 224
  17. theorem OAI.Percolation.norm_positivePart line 227
  18. theorem OAI.Percolation.exists_operator_of_matrix_domination line 238
  19. theorem OAI.Percolation.measurable_openEdges line 298
  20. theorem OAI.Percolation.twoPoint_eq_labelLaw line 303
  21. theorem OAI.Percolation.openEdges_mono line 312
  22. theorem OAI.Percolation.twoPoint_mono line 316
  23. theorem OAI.Percolation.operatorBounded_of_le line 331
  24. theorem OAI.Percolation.operatorNorm_mono line 340
  25. theorem OAI.Percolation.conn_iUnion_iff line 358
  26. theorem OAI.Percolation.ae_labels_ne line 374
  27. theorem OAI.Percolation.openEdges_eq_iUnion_of_tendsto line 387
  28. theorem OAI.Percolation.twoPoint_tendsto_of_monotone line 403
  29. theorem OAI.Percolation.operatorNorm_eq_sup_below line 432
  30. theorem OAI.Percolation.operatorBounded_iff_uniform_below line 465