OAI/MeasureTheory/Falconer/Recursion/FiniteCountingPotential.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The finite point potential needed by the elementary planar incidence bound.

  1. def OAI.Falconer.planarCountingMeasure line 13
  2. theorem OAI.Falconer.planarCountingMeasure_apply line 16
  3. theorem OAI.Falconer.planarCountingMeasure_lintegral line 23
  4. theorem OAI.Falconer.finite_dyadic_truncated_potential line 28
  5. def OAI.Falconer.planarPotentialConstant line 79
  6. theorem OAI.Falconer.planarPotentialConstant_pos line 82
  7. theorem OAI.Falconer.finite_dyadic_truncated_potential_real line 89