OAI/Combinatorics/Progressions/Estimates/NativeRoundedGraphEnergy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.floor_four_difference_bound line 12
  2. def OAI.Erdos3.roundedCoefficient line 32
  3. def OAI.Erdos3.coefficientRoundingErrors line 35
  4. theorem OAI.Erdos3.coefficientRoundingErrors_card_le line 41
  5. theorem OAI.Erdos3.roundedCoefficient_four_mem line 49
  6. theorem OAI.Erdos3.exists_unrounded_scalar line 97
  7. theorem OAI.Erdos3.exists_unrounded_vector line 119
  8. theorem OAI.Erdos3.rounded_graph_energy line 150
  9. theorem OAI.Erdos3.rounded_graph_energy_density line 168
  10. def OAI.Erdos3.coordinateDenominatorGrid line 210
  11. def OAI.Erdos3.variableRoundedCoefficient line 213
  12. def OAI.Erdos3.variableRoundingErrors line 217
  13. theorem OAI.Erdos3.variableRoundingErrors_card_le line 223
  14. theorem OAI.Erdos3.variableRoundedCoefficient_four_mem line 231
  15. theorem OAI.Erdos3.map_integer_coordinates line 277
  16. def OAI.Erdos3.finiteCoefficientLift line 287
  17. theorem OAI.Erdos3.finiteCoefficientLift_mem_Ico line 291
  18. theorem OAI.Erdos3.exists_unrounded_affine line 304
  19. theorem OAI.Erdos3.variable_graph_energy line 340
  20. theorem OAI.Erdos3.variable_graph_energy_density line 358
  21. def OAI.Erdos3.variableCoefficientLift line 402
  22. theorem OAI.Erdos3.variableCoefficientLift_mem_Ico line 406
  23. theorem OAI.Erdos3.exists_variable_unrounded_affine line 411
  24. theorem OAI.Erdos3.exists_coordinate_rounding_moduli line 446
  25. theorem OAI.Erdos3.NativeRankRelation.CommonData.rounded_coefficient_graph_energy line 474
  26. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_rounded_coefficient_graph_energy line 494