OAI/MeasureTheory/Falconer/Estimates/ScalarRatioFamily.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Counting and ball regularity for the actual ratio coefficients retained by the common-rectangle selection.

  1. theorem OAI.Falconer.scalar_ball_bound_all_radii line 10
  2. theorem OAI.Falconer.scalar_ratio_family_card line 23
  3. theorem OAI.Falconer.scalar_ratio_family_ball line 31