OAI/MeasureTheory/Falconer/Angular/NoncomparableSphereKernel.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual noncomparable two-sphere kernel

The small sphere is never expanded. Only the large sphere incurs a stationary remainder, and its bound uses the two existing published inputs.

  1. theorem OAI.Falconer.noncomparable_leading_decay_mono line 16
  2. theorem OAI.Falconer.exists_noncomparable_sphere_kernel line 29