OAI/Probability/LatticeSurface/Coercivity/SparseClusters.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SparseClusters.component line 11
  2. lemma OAI.SparseClusters.mem_component line 15
  3. lemma OAI.SparseClusters.walk_boundary line 19
  4. lemma OAI.SparseClusters.walk_mem_component line 30
  5. lemma OAI.SparseClusters.closed_walk_witness line 34
  6. lemma OAI.SparseClusters.card_walks_le line 70
  7. lemma OAI.SparseClusters.walk_all_bad line 101
  8. lemma OAI.SparseClusters.walk_start_bad line 113
  9. lemma OAI.SparseClusters.sparse_component_tail line 120
  10. lemma OAI.SparseClusters.card_le_fiber_mul_image line 164
  11. lemma OAI.SparseClusters.sparse_box_component_tail line 174
  12. lemma OAI.SparseClusters.measurable_graph_statistic line 226
  13. lemma OAI.SparseClusters.summable_box_moment line 260
  14. def OAI.SparseClusters.boxMoment line 270
  15. lemma OAI.SparseClusters.boxMoment_nonneg line 273
  16. lemma OAI.SparseClusters.nat_moment_of_geometric_tail line 276
  17. lemma OAI.SparseClusters.nat_pow_measurable line 321
  18. lemma OAI.SparseClusters.nat_pow_integrable_of_bound line 325
  19. lemma OAI.SparseClusters.nat_real_moment_of_geometric_tail line 333
  20. lemma OAI.SparseClusters.maximum_nat_moment_bound line 347
  21. lemma OAI.SparseClusters.reachable_of_edge_reachable line 374
  22. lemma OAI.SparseClusters.component_card_le_cover line 382
  23. def OAI.SparseClusters.badBoxGraph line 395
  24. lemma OAI.SparseClusters.sparse_cover_component_tail line 400