OAI/MeasureTheory/Falconer/Slicing/GaussianCloseMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Localized pairs in the actual Gaussian direction slices

  1. def OAI.Falconer.gaussianDirectionSliceMeasure line 13
  2. instance OAI.Falconer.gaussianDirectionSliceMeasure_finite line 17
  3. def OAI.Falconer.gaussianDirectionCloseMass line 23
  4. theorem OAI.Falconer.gaussianDirectionSlice_close_identity line 28
  5. theorem OAI.Falconer.gaussian_direction_close_average line 39