OAI/MeasureTheory/Falconer/Incidence/SampledFurstenberg.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The published Furstenberg input applied to sampled incidence lists

The original direction labels may repeat their coordinates and may have different covering families. All geometric lines are rounded to one grid before applying the published cardinality bound.

  1. theorem OAI.Falconer.sampled_furstenberg_obstruction line 17