OAI/MeasureTheory/Falconer/Estimates/DyadicFailedTests.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All failed geometric tests for an original cell pair

For probability starting laws the four restricted masses are at most one. Each discarded edge fails one of the two perpendicular tests or the longitudinal test. The estimate below is derived from those three cases.

  1. theorem OAI.Falconer.four_restrictions_mass_le_one line 20
  2. theorem OAI.Falconer.dyadic_failed_tests_bound line 34