OAI/MeasureTheory/Falconer/Incidence/TroublesomeIncidence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Original-law incidence bound for the actual troublesome-pair relation

  1. theorem OAI.Falconer.troublesome_pair_incidence_bound line 13