OAI/MeasureTheory/Falconer/Estimates/TripleGram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Gram determinants for the endpoint's three original chart directions

  1. def OAI.Falconer.tripleGram line 12
  2. def OAI.Falconer.gramPolynomial line 15
  3. theorem OAI.Falconer.tripleGram_polynomial line 18
  4. theorem OAI.Falconer.tripleGram_nonnegative line 28
  5. theorem OAI.Falconer.tripleGram_smul line 32
  6. theorem OAI.Falconer.northLift_inner line 40
  7. theorem OAI.Falconer.northLift_tripleGram_identity line 45
  8. theorem OAI.Falconer.northLift_tripleGram_lower line 54
  9. theorem OAI.Falconer.gnomonic_tripleGram line 60