OAI/MeasureTheory/FalconerCompletion/Shells/MonotoneShellTestDensity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Dyadic shells and prefix decompositions.

  1. lemma OAI.CurrentFalconer.MonotoneShell.monotone_shell_test_density line 20
  2. theorem OAI.CurrentFalconer.MonotoneShell.monotone_measure_shell_criterion line 99
  3. lemma OAI.CurrentFalconer.MonotoneShell.complexVariationError_nonneg line 143
  4. lemma OAI.CurrentFalconer.MonotoneShell.shell_sqrt_summable_of_decay line 145
  5. theorem OAI.CurrentFalconer.MonotoneShell.monotone_measure_shell_criterion_of_decay line 158
  6. lemma OAI.CurrentFalconer.AssemblyCompletion.shell_cutoff_exists line 187
  7. lemma OAI.CurrentFalconer.AssemblyCompletion.direction_cutoff_exists line 202