OAI/MeasureTheory/Falconer/Slicing/GaussianRowStability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Quantitative kernel geometry near a fixed orthonormal row frame

  1. theorem OAI.Falconer.gaussianRowMap_adjoint_apply line 11
  2. theorem OAI.Falconer.row_adjoint_near_isometry line 20
  3. theorem OAI.Falconer.row_adjoint_lower_near_isometry line 40
  4. theorem OAI.Falconer.kernel_projection_bound_of_adjoint_lower line 51
  5. theorem OAI.Falconer.row_kernel_projection_bound line 80