OAI/MeasureTheory/Falconer/Shells/FarPositiveSum.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive far kernels over the actual comparable cell pairs

The maximum ranges over the original tested distance laws. The number of summands is bounded by two free cell labels, not four.

  1. def OAI.Falconer.farCollisionMaximum line 17
  2. theorem OAI.Falconer.far_positive_kernel_sum_le line 26
  3. theorem OAI.Falconer.farCellPartners_regular_card line 60