OAI/MeasureTheory/Falconer/Graphs/WitnessGraph.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Schur bound from the original parallel-test witnesses

For each endpoint, all retained cells in an ancestor group are charged to one actual eligible witness. Combining both candidate bounds with the center tests gives the smaller of the two profile counts.

  1. def OAI.Falconer.DyadicParallelTest line 17
  2. def OAI.Falconer.DyadicCapWitnesses line 25
  3. theorem OAI.Falconer.retainedDyadic_witness_schur line 30