OAI/MeasureTheory/Falconer/Shells/AssemblyErrorBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Converting the original-pair deletion bound to its summable majorant

  1. theorem OAI.Falconer.dyadic_leaf_error line 10
  2. theorem OAI.Falconer.class_discard_numeric line 20
  3. theorem OAI.Falconer.restoration_numeric_bound line 32