OAI/Probability/LatticeSurface/Geometry/CapReflection.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ExtremalEdges.finite_partition_measure line 16
  2. lemma OAI.ExtremalEdges.finite_switch_preserving line 29
  3. def OAI.ExtremalEdges.lock line 63
  4. def OAI.ExtremalEdges.reflect line 68
  5. lemma OAI.ExtremalEdges.preserving_reflect line 72
  6. lemma OAI.ExtremalEdges.reflect_involutive line 86
  7. lemma OAI.ExtremalEdges.restore_reflect line 93
  8. lemma OAI.ExtremalEdges.abs_restore_reflect line 102
  9. lemma OAI.ExtremalEdges.lock_reflect line 110
  10. lemma OAI.ExtremalEdges.measurable_lock_fiber line 116
  11. lemma OAI.ExtremalEdges.lock_same_sign line 140
  12. lemma OAI.ExtremalEdges.reachable_same_sign line 157
  13. def OAI.ExtremalEdges.freeCluster line 165
  14. lemma OAI.ExtremalEdges.disjoint_freeCluster line 168
  15. lemma OAI.ExtremalEdges.freeCluster_closed line 175
  16. lemma OAI.ExtremalEdges.reflect_cluster_feasible line 183
  17. def OAI.ExtremalEdges.clusterFlip line 222
  18. lemma OAI.ExtremalEdges.preserving_clusterFlip line 226
  19. lemma OAI.ExtremalEdges.positive_freeCluster line 239
  20. lemma OAI.ExtremalEdges.clusterFlip_positive line 253
  21. def OAI.ExtremalEdges.below line 274
  22. lemma OAI.ExtremalEdges.measurable_below line 278
  23. lemma OAI.ExtremalEdges.volume_below_insert line 285
  24. theorem OAI.ExtremalEdges.volume_one_sided line 310