OAI/MeasureTheory/Falconer/Angular/SuffixDirection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transferring the suffix witness test to the cell-center direction

The test is imposed on the full conditional law in the witness direction. Only the direction changes; its quadratic error is absorbed by the test width before the original-law collision estimate is used.

  1. theorem OAI.Falconer.normalized_difference_le line 17
  2. theorem OAI.Falconer.DyadicCube.pair_direction_approximation line 38
  3. theorem OAI.Falconer.cell_projection_direction_transfer line 59
  4. theorem OAI.Falconer.suffix_witness_projection_transfer line 85