OAI/MeasureTheory/Falconer/Shells/PositiveKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The scalar far kernel in the actual positive states

The one-dimensional bin estimate is applied to the two original tested pair-distance laws. Both use the same profile normalization at the child scale. No angular symbol is removed before this positive comparison.

  1. theorem OAI.Falconer.real_bin_kernel_le_max_collision line 17
  2. theorem OAI.Falconer.positiveCollision_kernel_max line 47