OAI/Geometry/PinnedDistances/ArithmeticHierarchy.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPinned.Global.good line 28
  2. lemma OAI.WeakPinned.Global.embedding_ne line 35
  3. lemma OAI.WeakPinned.Global.measurableSet_good line 40
  4. lemma OAI.WeakPinned.Global.good_ae line 60
  5. instance OAI.WeakPinned.Global.good_decidable line 66
  6. def OAI.WeakPinned.Global.arch line 69
  7. lemma OAI.WeakPinned.Global.arch_value_ae line 83
  8. lemma OAI.WeakPinned.Global.arch_measurable line 90
  9. lemma OAI.WeakPinned.Global.arch_integrable line 100
  10. lemma OAI.WeakPinned.Global.arch_mean line 117
  11. def OAI.WeakPinned.Global.finite line 128
  12. abbrev OAI.WeakPinned.Global.DiffPair line 139
  13. def OAI.WeakPinned.Global.badPlaces line 141
  14. lemma OAI.WeakPinned.Global.badPlaces_mem line 146
  15. lemma OAI.WeakPinned.Global.finite_value_sum line 154
  16. def OAI.WeakPinned.Global.S line 166
  17. def OAI.WeakPinned.Global.L line 170
  18. def OAI.WeakPinned.Global.M line 174
  19. lemma OAI.WeakPinned.Global.coordinate_overlap_identity line 178
  20. lemma OAI.WeakPinned.Global.S_nonneg line 217
  21. lemma OAI.WeakPinned.Global.L_nonneg line 223
  22. def OAI.WeakPinned.Hierarchy.Depth.count line 236
  23. def OAI.WeakPinned.Hierarchy.Depth.mass line 238
  24. lemma OAI.WeakPinned.Hierarchy.Depth.sum_map_count line 240
  25. lemma OAI.WeakPinned.Hierarchy.Depth.sumCells_count line 250
  26. lemma OAI.WeakPinned.Hierarchy.Depth.count_nonneg line 253
  27. lemma OAI.WeakPinned.Hierarchy.Depth.count_le_overlap line 255
  28. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_count line 262
  29. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_count line 271
  30. lemma OAI.WeakPinned.Hierarchy.Depth.mass_nonneg line 278
  31. lemma OAI.WeakPinned.Hierarchy.Depth.mass_singleton line 284
  32. lemma OAI.WeakPinned.Hierarchy.Depth.mass_le_overlap line 287
  33. lemma OAI.WeakPinned.Hierarchy.Depth.integral_sumCells line 295
  34. lemma OAI.WeakPinned.Hierarchy.Depth.mass_overlap line 310
  35. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_count_param line 326
  36. lemma OAI.WeakPinned.Hierarchy.Depth.measurable_mass_param line 341
  37. lemma OAI.WeakPinned.Hierarchy.Depth.integrable_mass_param line 347
  38. lemma OAI.WeakPinned.Hierarchy.Depth.averaged_mass_overlap line 361