OAI/MeasureTheory/Falconer/Estimates/TripleGramStability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Stability of the three-direction Gram determinant under projection

  1. theorem OAI.Falconer.product_three_difference line 10
  2. def OAI.Falconer.determinantTerms line 37
  3. theorem OAI.Falconer.determinant_eq_sum line 41
  4. theorem OAI.Falconer.determinant_three_stability line 48
  5. theorem OAI.Falconer.gram_three_stability line 77