OAI/MeasureTheory/Falconer/Radial/ScalarAffineExceptions.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Exceptional coefficient counts for separated scalar clusters. This is the finite real-variable separation estimate in the porous amplification argument; the coefficient distribution is the original finite set.

  1. theorem OAI.Falconer.scalar_affine_small_subset line 12
  2. theorem OAI.Falconer.scalar_affine_small_card line 25
  3. def OAI.Falconer.scalarBadClusterCoefficients line 40
  4. theorem OAI.Falconer.scalar_bad_cluster_card line 44