OAI/MeasureTheory/Falconer/Geometry/ScalarKernelGeometry.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Relating the scalar collision kernel to the Euclidean potential of the original Cartesian product.

  1. theorem OAI.Falconer.rowPoint_pair_dist_lower line 10
  2. theorem OAI.Falconer.rowPoint_pair_dist_upper line 15
  3. theorem OAI.Falconer.scalar_kernel_le_euclidean line 25
  4. theorem OAI.Falconer.scalar_kernel_sum_le_potential line 55