OAI/MeasureTheory/Falconer/Shells/DescriptorShellRegime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual source shell satisfies the descriptor stationary regime

  1. theorem OAI.Falconer.source_shell_frequency_bounds line 11
  2. theorem OAI.Falconer.eventual_descriptor_source_shell_regime line 30
  3. theorem OAI.Falconer.eventually_separated_inverse_frequency line 59
  4. theorem OAI.Falconer.eventual_descriptor_pair_shell_regime line 88