OAI/MeasureTheory/Falconer/Incidence/BlockChordGeometry.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A regular profile interval gives both geometric hypotheses for the finite-scale incidence argument, for the original points in each parent.

  1. theorem OAI.Falconer.blockClass_chord_geometry line 12