OAI/MeasureTheory/Falconer/Slicing/GaussianThreshold.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform positive incidence threshold on the bounded parameter box

  1. def OAI.Falconer.gaussianSelectionThreshold line 11
  2. theorem OAI.Falconer.gaussianSelectionThreshold_pos line 14
  3. theorem OAI.Falconer.gaussianSelectionThreshold_budget line 19
  4. theorem OAI.Falconer.gaussianSelectionThreshold_uniform line 27