OAI/Geometry/PinnedDistances/FiberOverlap.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.SmallFiber.slice line 28
  2. def OAI.WeakPinned.SmallFiber.edgeCell line 31
  3. lemma OAI.WeakPinned.SmallFiber.edgeCell_formula line 35
  4. lemma OAI.WeakPinned.SmallFiber.slice_nonneg line 55
  5. lemma OAI.WeakPinned.SmallFiber.slice_le_edgeCell line 63
  6. lemma OAI.WeakPinned.SmallFiber.slice_le_lam line 73
  7. lemma OAI.WeakPinned.SmallFiber.edgeLaw_diag line 87
  8. lemma OAI.WeakPinned.SmallFiber.edgeCell_dom line 96
  9. lemma OAI.WeakPinned.SmallFiber.slice_singleton line 111
  10. lemma OAI.WeakPinned.SmallFiber.large_slice_bound line 123
  11. lemma OAI.WeakPinned.SmallFiber.small_slice_bound line 143
  12. lemma OAI.WeakPinned.Hierarchy.Depth.sum_source_cell line 166
  13. lemma OAI.WeakPinned.Hierarchy.Depth.sumCells_split line 179
  14. lemma OAI.WeakPinned.Hierarchy.Depth.sum_complement_prob line 190
  15. lemma OAI.WeakPinned.SmallFiber.nongiant_small_slice line 213
  16. lemma OAI.WeakPinned.SmallFiber.pointwise_split line 244
  17. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_sumCells line 295
  18. lemma OAI.WeakPinned.SmallFiber.integral_split line 311
  19. lemma OAI.WeakPinned.SmallFiber.local_small_fiber line 339
  20. lemma OAI.WeakPinned.SmallFiber.pair_integral_edgeCell line 369
  21. lemma OAI.WeakPinned.SmallFiber.local_small_fiber_reduced line 400