OAI/MeasureTheory/Falconer/Radial/RadialDischarge.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Independent proof of the precise published radial input, using the actual Euclidean surface measure, orthogonal slices, and smooth approximation.

  1. theorem OAI.Falconer.finite_euclidean_radial_moment line 13
  2. theorem OAI.Falconer.published_radial_moment line 40