OAI/MeasureTheory/Falconer/Graphs/RegularGraphCosts.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Polynomial losses in the refined graph obstruction, specialized to a single weak scale parameter.

  1. def OAI.Falconer.regularGraphCost line 9
  2. theorem OAI.Falconer.regularGraphCost_one_le line 13
  3. theorem OAI.Falconer.regular_graph_weak_costs line 19