OAI/MeasureTheory/Falconer/Shells/NormalizedHighShellError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PlanarFalconer.measurable_list_sum line 9
  2. theorem OAI.PlanarFalconer.PositiveDistanceData.normalizedHighShellKernel_measurable line 20
  3. theorem OAI.PlanarFalconer.PositiveDistanceData.uniform_normalized_high_shell_error line 38