OAI/MeasureTheory/Falconer/Geometry/NormalizedRegularGain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The good-scale estimate normalized by the actual pencil cardinality. Small pencils use the regular-set theorem, and large pencils use the interpolated second moment. No upper bound on the union is assumed.

  1. theorem OAI.Falconer.normalized_regular_fine_gain line 13