OAI/MeasureTheory/Falconer/Shells/NormalizedShellCoefficients.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform radial coefficients after the stationary shell normalization

The inverse order pays for the sum of the two endpoint derivative orders. The remaining radial ratio is bounded on the fixed shell, independently of its frequency and cell depth.

  1. theorem OAI.Falconer.normalized_stationary_coefficient_le line 14
  2. theorem OAI.Falconer.restored_normalized_stationary_coefficient_le line 30