OAI/MeasureTheory/Falconer/Estimates/TripleColumns.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Explicit cofactor coordinates for three transverse directions

  1. def OAI.Falconer.tripleCofactors line 11
  2. theorem OAI.Falconer.tripleCofactors_inner line 14
  3. def OAI.Falconer.tripleColumnLinear line 29
  4. def OAI.Falconer.tripleDualCoordinates line 35
  5. theorem OAI.Falconer.tripleDualCoordinates_column line 39
  6. theorem OAI.Falconer.tripleColumnLinear_injective line 49
  7. def OAI.Falconer.tripleColumnEquiv line 54
  8. theorem OAI.Falconer.tripleColumnEquiv_apply line 60
  9. theorem OAI.Falconer.tripleColumnEquiv_symm_apply line 64