OAI/MeasureTheory/Falconer/Slicing/GaussianRowMap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Linear maps and kernel planes for the Gaussian slicing parameters

  1. def OAI.Falconer.gaussianRowMap line 14
  2. theorem OAI.Falconer.gaussianRowMap_apply line 18
  3. theorem OAI.Falconer.gaussianRowMap_eq_coordinates line 23
  4. theorem OAI.Falconer.gaussianRowMap_adjoint_basis line 28
  5. theorem OAI.Falconer.coordinate_norm_le_card_mul line 35
  6. theorem OAI.Falconer.gaussianRowMap_norm_le_of_bands line 48