OAI/MeasureTheory/Falconer/Estimates/DyadicDisplacements.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Point replacement errors in the original dyadic cubes

The two points of an internal displacement belong to different descendants of the same parent. No separation between the two endpoint parents enters these estimates.

  1. theorem OAI.Falconer.DyadicCube.descendant_displacement_error line 15
  2. theorem OAI.Falconer.DyadicCube.descendant_displacement_bound line 32
  3. theorem OAI.Falconer.DyadicCube.descendant_center_displacement_bound line 40
  4. theorem OAI.Falconer.DyadicCube.descendant_cap_error line 47