OAI/Combinatorics/Progressions/Dynamics/MultilinearityBudgets.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.MultilinearityBudget.coordinates line 12
  2. def OAI.Erdos3.MultilinearityBudget.ambient line 14
  3. def OAI.Erdos3.MultilinearityBudget.quotient line 16
  4. def OAI.Erdos3.MultilinearityBudget.observable line 18
  5. def OAI.Erdos3.MultilinearityBudget.reconstruction line 20
  6. def OAI.Erdos3.MultilinearityBudget.total line 22
  7. theorem OAI.Erdos3.MultilinearityBudget.ambient_bounds line 24
  8. theorem OAI.Erdos3.MultilinearityBudget.quotient_bounds line 34
  9. theorem OAI.Erdos3.MultilinearityBudget.observable_nonneg line 45
  10. theorem OAI.Erdos3.MultilinearityBudget.reconstruction_bounds line 49
  11. theorem OAI.Erdos3.MultilinearityBudget.total_bounds line 63
  12. theorem OAI.Erdos3.MultilinearityBudget.observable_bound line 72
  13. theorem OAI.Erdos3.MultilinearityBudget.exists_total_bound line 83