OAI/Combinatorics/Progressions/Estimates/FiniteGraphEnergy.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.shiftedAdditiveQuadruples line 13
  2. theorem OAI.Erdos3.shiftedAdditiveQuadruples_card line 17
  3. theorem OAI.Erdos3.shiftedAdditiveQuadruples_card_le_energy line 39
  4. def OAI.Erdos3.additiveGraph line 63
  5. theorem OAI.Erdos3.additiveGraph_card line 67
  6. def OAI.Erdos3.additiveGraphQuadruple line 71
  7. theorem OAI.Erdos3.additiveGraphQuadruple_injective line 77
  8. theorem OAI.Erdos3.graph_energy_of_few_quadruple_differences line 86