OAI/MeasureTheory/Falconer/Slicing/DyadicSliceSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Selecting a slice directly from the two original finite-scale ball bounds

  1. def OAI.Falconer.gaussianPruningRadius line 13
  2. def OAI.Falconer.gaussianPruningWeight line 16
  3. theorem OAI.Falconer.gaussianPruningWeight_eq line 19
  4. theorem OAI.Falconer.dyadic_original_slice_selection line 26