OAI/MeasureTheory/FalconerCompletion/Graphs/AmbientDescendants.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. def OAI.GraphLiteralSupport.Attempt4FullFar.ambientDescendantsND line 16
  2. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mem_ambientDescendantsND_iff line 21
  3. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientDescendantsND_card line 36
  4. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientDescendantsND_subset line 48
  5. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ambientDescendantsND_mem_of_point line 55
  6. theorem OAI.GraphLiteralSupport.Attempt4FullFar.ambientDescendantsND_cover line 64
  7. def OAI.GraphLiteralSupport.Attempt4FullFar.farParentPairsND line 75
  8. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mem_farParentPairsND_iff line 81
  9. theorem OAI.GraphLiteralSupport.Attempt4FullFar.far_comparable_finite_coverND line 89
  10. def OAI.GraphLiteralSupport.Attempt4FullFar.firstCoverBinND line 123
  11. lemma OAI.GraphLiteralSupport.Attempt4FullFar.mem_firstCoverBinND line 126
  12. lemma OAI.GraphLiteralSupport.Attempt4FullFar.firstCoverBinND_subset line 132
  13. lemma OAI.GraphLiteralSupport.Attempt4FullFar.firstCoverBinND_disjoint line 137
  14. lemma OAI.GraphLiteralSupport.Attempt4FullFar.firstCoverBinND_cover line 148
  15. lemma OAI.GraphLiteralSupport.Attempt4FullFar.measurableSet_firstCoverBinND line 166
  16. theorem OAI.GraphLiteralSupport.Attempt4FullFar.integral_firstCoverBinND line 173
  17. def OAI.GraphLiteralSupport.Attempt4FullFar.farComparableSetND line 198
  18. lemma OAI.GraphLiteralSupport.Attempt4FullFar.farComparableSetND_measurable line 206
  19. def OAI.GraphLiteralSupport.Attempt4FullFar.farParentRegionND line 217
  20. lemma OAI.GraphLiteralSupport.Attempt4FullFar.farParentRegionND_measurable line 224
  21. theorem OAI.GraphLiteralSupport.Attempt4FullFar.farComparableSetND_cover line 230
  22. theorem OAI.GraphLiteralSupport.Attempt4FullFar.integral_farComparable_binsND line 241
  23. lemma OAI.GraphLiteralSupport.Attempt4FullFar.ae_ambientGridCell_nonzeroND line 270
  24. def OAI.GraphLiteralSupport.Attempt4FullFar.occupiedDescendantsND line 283
  25. def OAI.GraphLiteralSupport.Attempt4FullFar.occupiedFarPairsND line 288
  26. lemma OAI.GraphLiteralSupport.Attempt4FullFar.occupiedFarPairsND_first line 294
  27. def OAI.GraphLiteralSupport.Attempt4FullFar.occupiedFarRegionND line 301
  28. lemma OAI.GraphLiteralSupport.Attempt4FullFar.occupiedFarRegionND_measurable line 309
  29. theorem OAI.GraphLiteralSupport.Attempt4FullFar.occupiedFarRegionND_ae_cover line 316