OAI/MeasureTheory/Falconer/Estimates/CommonRegularFamily.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common regular parameter set extracted from a family of regular rows. The loss is explicit and polynomial in the union-to-row cardinality ratio.

  1. theorem OAI.Falconer.common_regular_family line 9
  2. theorem OAI.Falconer.popular_family_rows line 39