OAI/MeasureTheory/Falconer/Slicing/GaussianIncidenceAverage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Incidence averaging for the original point and direction labels

  1. theorem OAI.Falconer.gaussian_point_band_label_average line 13
  2. theorem OAI.Falconer.gaussian_incidence_raw_point_average line 36
  3. theorem OAI.Falconer.gaussian_slice_incidence_point_average line 55
  4. theorem OAI.Falconer.gaussian_slice_incidence_mean_lower line 89