OAI/MeasureTheory/Falconer/Geometry/ProjectionKernel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Normalized projection kernels, including their diagonal convention.

  1. def OAI.Falconer.directionalProjectionKernel line 11
  2. theorem OAI.Falconer.directionalProjectionKernel_measurable line 16
  3. theorem OAI.Falconer.projection_kernel_factor line 23
  4. theorem OAI.Falconer.directionalProjectionKernel_rpow line 39
  5. theorem OAI.Falconer.directionalProjectionKernel_angular_bound line 47