OAI/MeasureTheory/FalconerCompletion/Measures/LocalDistanceCollisionBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Measures and the conditional distance-set completion.

  1. theorem OAI.GraphLiteralSupport.CurrentFalconer.local_distance_collision_boundND line 25
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.measure_smul_condND line 45
  3. theorem OAI.GraphLiteralSupport.CurrentFalconer.local_distance_conditional_collisionND line 51