OAI/MeasureTheory/Falconer/Estimates/GeneralColumns.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual coordinate isomorphisms for a transverse tuple in arbitrary dimension

  1. def OAI.Falconer.euclideanColumnMatrix line 13
  2. def OAI.Falconer.euclideanColumnLinear line 16
  3. theorem OAI.Falconer.euclideanColumnLinear_apply line 22
  4. def OAI.Falconer.euclideanDualCoordinates line 28
  5. theorem OAI.Falconer.euclideanDualCoordinates_column line 31
  6. def OAI.Falconer.euclideanColumnEquiv line 41
  7. theorem OAI.Falconer.euclideanColumnEquiv_apply line 47
  8. theorem OAI.Falconer.euclideanColumnEquiv_symm_apply line 51
  9. theorem OAI.Falconer.euclideanColumnMatrix_gram line 58
  10. theorem OAI.Falconer.euclideanColumnMatrix_gram_sqrt line 65