OAI/Combinatorics/Progressions/Estimates/WeightedPlateauSiteApproximation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sigma_sum_coefficient_norm_le line 13
  2. theorem OAI.Erdos3.sigma_sum_approximation_error line 25
  3. theorem OAI.Erdos3.sigma_partition_card_le line 43
  4. theorem OAI.Erdos3.finiteSitePrefactor_substitution_identity line 68
  5. theorem OAI.Erdos3.finiteSitePrefactor_substitution_error line 80
  6. theorem OAI.Erdos3.finiteSitePrefactor_coefficient_mass line 100
  7. def OAI.Erdos3.weightedPlateauModeCoefficient line 121
  8. theorem OAI.Erdos3.weightedPlateauModeCoefficient_sum_le line 127
  9. def OAI.Erdos3.weightedPlateauModeModel line 140
  10. theorem OAI.Erdos3.weightedPlateauModeModel_norm line 150
  11. theorem OAI.Erdos3.weightedPlateauModeModel_lipschitz line 165
  12. theorem OAI.Erdos3.weightedPlateauModeModel_grid_value line 182
  13. def OAI.Erdos3.selectedBooleanSiteRows line 213
  14. theorem OAI.Erdos3.selectedBooleanSiteRows_lipschitz line 218
  15. theorem OAI.Erdos3.selectedBooleanSiteRows_integer line 235
  16. def OAI.Erdos3.rationalBooleanSitePhase line 244
  17. theorem OAI.Erdos3.rationalBooleanSitePhase_norm line 249
  18. theorem OAI.Erdos3.rationalBooleanSitePhase_prod line 253
  19. theorem OAI.Erdos3.exists_plateau_mode_site_approximation line 270
  20. theorem OAI.Erdos3.exists_residue_plateau_site_approximation line 294
  21. theorem OAI.Erdos3.exists_integer_plateau_site_approximation line 337
  22. theorem OAI.Erdos3.exists_scalar_residue_plateau_site_approximation line 382
  23. theorem OAI.Erdos3.exists_scalar_integer_plateau_site_approximation line 414
  24. abbrev OAI.Erdos3.PlateauSiteIndex line 461
  25. theorem OAI.Erdos3.plateauSiteIndex_card_le line 466
  26. theorem OAI.Erdos3.exists_integer_plateau_sum_site_approximation line 476
  27. def OAI.Erdos3.weightedCubePlateauCoefficient line 531
  28. theorem OAI.Erdos3.weightedCubePlateauCoefficient_sum_le line 536
  29. theorem OAI.Erdos3.weightedCubePlateauMixture_model line 551
  30. theorem OAI.Erdos3.exists_weightedCube_plateau_site_approximation line 572
  31. theorem OAI.Erdos3.exists_weighted_plateau_site_approximation line 628