OAI/Geometry/PinnedDistances/Hierarchy.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WeakPinned.Hierarchy.Depth line 21
  2. def OAI.WeakPinned.Hierarchy.Depth.share line 31
  3. instance OAI.WeakPinned.Hierarchy.Depth.(instance at line 32) line 32
  4. lemma OAI.WeakPinned.Hierarchy.Depth.share_refl line 35
  5. lemma OAI.WeakPinned.Hierarchy.Depth.share_symm line 37
  6. lemma OAI.WeakPinned.Hierarchy.Depth.share_trans line 42
  7. lemma OAI.WeakPinned.Hierarchy.Depth.share_mono line 53
  8. def OAI.WeakPinned.Hierarchy.Depth.cell line 56
  9. lemma OAI.WeakPinned.Hierarchy.Depth.mem_cell line 58
  10. lemma OAI.WeakPinned.Hierarchy.Depth.self_mem_cell line 61
  11. lemma OAI.WeakPinned.Hierarchy.Depth.cell_nonempty line 64
  12. lemma OAI.WeakPinned.Hierarchy.Depth.cell_eq_of_share line 66
  13. lemma OAI.WeakPinned.Hierarchy.Depth.cell_mono line 72
  14. def OAI.WeakPinned.Hierarchy.Depth.cells line 76
  15. lemma OAI.WeakPinned.Hierarchy.Depth.mem_cells line 77
  16. lemma OAI.WeakPinned.Hierarchy.Depth.cell_mem_cells line 79
  17. lemma OAI.WeakPinned.Hierarchy.Depth.cell_of_mem line 81
  18. lemma OAI.WeakPinned.Hierarchy.Depth.cells_disjoint line 86
  19. lemma OAI.WeakPinned.Hierarchy.Depth.cells_pair_sum line 92
  20. def OAI.WeakPinned.Hierarchy.Depth.giants line 106
  21. lemma OAI.WeakPinned.Hierarchy.Depth.mem_giants line 109
  22. lemma OAI.WeakPinned.Hierarchy.Depth.giants_unique line 112
  23. lemma OAI.WeakPinned.Hierarchy.Depth.giants_card_le_one line 121
  24. def OAI.WeakPinned.Hierarchy.Depth.giant line 124
  25. lemma OAI.WeakPinned.Hierarchy.Depth.giant_eq line 126
  26. def OAI.WeakPinned.Hierarchy.Depth.transformed line 132
  27. def OAI.WeakPinned.Hierarchy.Depth.sumCells line 136
  28. def OAI.WeakPinned.Hierarchy.Depth.pairOverlap line 138
  29. def OAI.WeakPinned.Hierarchy.Depth.giantIndicator line 141
  30. def OAI.WeakPinned.Hierarchy.Depth.outsideIndicator line 143
  31. lemma OAI.WeakPinned.Hierarchy.Depth.sumCells_formula line 146
  32. lemma OAI.WeakPinned.Hierarchy.Depth.pairOverlap_formula line 161
  33. lemma OAI.WeakPinned.Hierarchy.Depth.giants_nonempty_iff line 180
  34. lemma OAI.WeakPinned.Hierarchy.Depth.giants_mono line 193
  35. lemma OAI.WeakPinned.Hierarchy.Depth.isClosed_giants line 199
  36. def OAI.WeakPinned.Hierarchy.Depth.radius line 218
  37. lemma OAI.WeakPinned.Hierarchy.Depth.radius_nonneg line 221
  38. lemma OAI.WeakPinned.Hierarchy.Depth.abs_value_le_radius line 224
  39. lemma OAI.WeakPinned.Hierarchy.Depth.cell_of_low line 231
  40. lemma OAI.WeakPinned.Hierarchy.Depth.cell_of_high line 237
  41. lemma OAI.WeakPinned.Hierarchy.Depth.giants_of_low line 243
  42. lemma OAI.WeakPinned.Hierarchy.Depth.giants_le_radius line 252
  43. def OAI.WeakPinned.Hierarchy.Depth.M line 262

    Source documentation

    The last level containing a giant.

    def M : ℝ := sSup {r : ℝ | (d.giants r).Nonempty}
  44. lemma OAI.WeakPinned.Hierarchy.Depth.giants_cutoff line 264
  45. lemma OAI.WeakPinned.Hierarchy.Depth.M_bounds line 271
  46. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cell line 277
  47. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cells line 283
  48. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giants line 288
  49. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giant line 292
  50. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giantIndicator line 295
  51. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_outsideIndicator line 299
  52. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_pairOverlap line 305
  53. lemma OAI.WeakPinned.Hierarchy.Depth.outsideIndicator_bounds line 317
  54. lemma OAI.WeakPinned.Hierarchy.Depth.pairOverlap_bounds line 322
  55. lemma OAI.WeakPinned.Hierarchy.Depth.outsideIndicator_zero_low line 340
  56. lemma OAI.WeakPinned.Hierarchy.Depth.outsideIndicator_zero_high line 346
  57. lemma OAI.WeakPinned.Hierarchy.Depth.pairOverlap_zero_low line 351
  58. lemma OAI.WeakPinned.Hierarchy.Depth.pairOverlap_zero_high line 357
  59. def OAI.WeakPinned.Hierarchy.Depth.potential line 367

    Source comment

    The diagonal is deliberately absent from overlapLength's domain: the transformed singleton tails have infinite diagonal overlap.
    def potential (x : P) : ℝ := ∫ r : ℝ, d.outsideIndicator r x
  60. def OAI.WeakPinned.Hierarchy.Depth.overlapLength line 369
  61. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_supported_Icc line 371
  62. lemma OAI.WeakPinned.Hierarchy.Depth.outsideIndicator_zero_compl line 384
  63. lemma OAI.WeakPinned.Hierarchy.Depth.pairOverlap_zero_compl line 392
  64. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_outsideIndicator line 400
  65. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_pairOverlap line 408
  66. lemma OAI.WeakPinned.Hierarchy.Depth.integral_cutoff line 416
  67. lemma OAI.WeakPinned.Hierarchy.Depth.depth_identity line 423
  68. lemma OAI.WeakPinned.Hierarchy.Depth.potential_nonneg line 464
  69. lemma OAI.WeakPinned.Hierarchy.Depth.overlapLength_nonneg line 467
  70. lemma OAI.WeakPinned.Hierarchy.Depth.integral_bound_supported line 470
  71. lemma OAI.WeakPinned.Hierarchy.Depth.potential_le line 482
  72. lemma OAI.WeakPinned.Hierarchy.Depth.overlapLength_le line 488
  73. lemma OAI.WeakPinned.Hierarchy.Depth.zero_values line 495
  74. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cell_param line 520
  75. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_cells_param line 526
  76. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giants_param line 531
  77. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giant_param line 536
  78. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_giantIndicator_param line 540
  79. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_outsideIndicator_param line 544
  80. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_pairOverlap_param line 549
  81. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_potential_param line 562
  82. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_overlapLength_param line 568
  83. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_M_param line 575
  84. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_radius_param line 593
  85. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_potential_param line 597
  86. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_overlapLength_param line 605
  87. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_M_param line 613
  88. lemma OAI.WeakPinned.Hierarchy.Depth.integral_depth_identity line 619