OAI/MeasureTheory/FalconerCompletion/Estimates/ScaleAbout.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Quantitative estimates for the distance-set construction.

  1. def OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.scaleAbout line 22
  2. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.scaleAbout_ball_preimage line 25
  3. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.projectionCollision_scale line 36
  4. def OAI.GraphLiteralSupport.CurrentFalconer.TreeND.rescaledConditional line 54
  5. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.rescaledConditional_probability line 58
  6. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.rescaledConditional_support line 65
  7. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.rescaledConditional_dyadic_ball line 80
  8. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.profile_power_dyadic line 103
  9. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.rescaledConditional_ball_bound line 117
  10. theorem OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.critical_projection_collision_mean line 172
  11. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.testWidth_zero line 218
  12. lemma OAI.GraphLiteralSupport.CurrentFalconer.TreeND.scaled_testWidth_zero line 222
  13. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.actual_projection_collision_mean line 228
  14. lemma OAI.GraphLiteralSupport.CurrentFalconer.Exceptional.exceptional_of_mean line 318
  15. theorem OAI.GraphLiteralSupport.CurrentFalconer.TreeND.uniform_actual_projection_exceptional line 341