OAI/MeasureTheory/FalconerCompletion/Graphs/SharedBinSupportCollision.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Graph energies and pair estimates.

  1. lemma OAI.GraphLiteralSupport.CurrentFalconer.shared_bin_support_collisionND line 28
  2. theorem OAI.GraphLiteralSupport.CurrentFalconer.finite_positive_bin_assemblyND line 52
  3. def OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND line 84
  4. instance OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_finite line 87
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_mono line 90
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_mass line 94
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_collision line 98
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_bin_sq_le line 106
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.pairDistanceLawND_cell_support line 115
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.suffix_witness_local_binsND line 129
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.treeCell_dist_sqrt line 160
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.classConditional_eq_cond line 191
  13. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.CentreSeparated line 201
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.separated_parent_points line 205
  15. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffix_dyadic_ratio line 226
  16. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.suffix_taylor_widths line 232
  17. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.source_suffix_projection_mem line 258
  18. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.atCells line 274
  19. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.PositiveDistanceState.uniform_actual_suffix_local_bins line 276