OAI/MeasureTheory/Falconer/Estimates/AdaptedFailure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single adapted chart for a discarded cell--cap term

The frame is chosen using the cap center and the center displacement. It works simultaneously for every point displacement allowed by the cell-replacement error. No choice depends on an individual point pair.

  1. theorem OAI.Falconer.failed_test_adapted_phase_lower line 17
  2. theorem OAI.Falconer.failed_test_sphere_nonstationary line 48