OAI/Combinatorics/ThinTrees/Coarea.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.Geometry.integrable_interval_indicator line 15
  2. lemma OAI.StrongThinTree.Geometry.integral_interval_indicator line 19
  3. lemma OAI.StrongThinTree.Geometry.threshold_interval line 24
  4. lemma OAI.StrongThinTree.Geometry.finite_coarea line 33
  5. lemma OAI.StrongThinTree.Geometry.integrable_cut_card line 56
  6. lemma OAI.StrongThinTree.Geometry.cut_range_bound line 73
  7. def OAI.StrongThinTree.Geometry.clamp line 92
  8. lemma OAI.StrongThinTree.Geometry.clamp_eq_left line 94
  9. lemma OAI.StrongThinTree.Geometry.clamp_eq_right line 97
  10. lemma OAI.StrongThinTree.Geometry.clamp_bounds line 100
  11. lemma OAI.StrongThinTree.Geometry.clamp_lt_iff line 104
  12. lemma OAI.StrongThinTree.MultiGraph.clamped_variation_lower line 122
  13. lemma OAI.StrongThinTree.Geometry.clamp_mono line 156
  14. lemma OAI.StrongThinTree.Geometry.clipped_affine_interval_increasing line 159
  15. lemma OAI.StrongThinTree.Geometry.clipped_affine_interval line 202
  16. lemma OAI.StrongThinTree.Geometry.clamped_affine_disjoint_sum line 219
  17. def OAI.StrongThinTree.Geometry.cube line 259
  18. def OAI.StrongThinTree.Geometry.binary line 261
  19. def OAI.StrongThinTree.Geometry.l1dist line 263
  20. lemma OAI.StrongThinTree.Geometry.binary_cube line 265
  21. lemma OAI.StrongThinTree.Geometry.l1dist_nonneg line 269
  22. lemma OAI.StrongThinTree.Geometry.l1dist_comm line 272
  23. lemma OAI.StrongThinTree.Geometry.l1dist_reverse line 275
  24. lemma OAI.StrongThinTree.Geometry.cube_segment line 286
  25. lemma OAI.StrongThinTree.Geometry.binary_radial_affine line 296
  26. lemma OAI.StrongThinTree.Geometry.binary_shell_edge_bound line 313
  27. lemma OAI.StrongThinTree.MultiGraph.binary_shell_length_bound line 338