OAI/MeasureTheory/Falconer/Estimates/FiniteOverlap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Counting heavy members of a finite family with bounded overlap

  1. theorem OAI.Falconer.finite_measure_sum_le_overlap line 14
  2. theorem OAI.Falconer.heavy_family_card_bound line 34