OAI/Combinatorics/Progressions/Estimates/ActiveAveragedProfileComparison.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.maskedSiteFactor line 15
  2. theorem OAI.Erdos3.maskedSiteFactor_prod line 20
  3. theorem OAI.Erdos3.maskedSiteExpansion_identity line 36
  4. theorem OAI.Erdos3.maskedSiteFactor_bound line 48
  5. theorem OAI.Erdos3.maskedSiteExpansion_coefficient_sum line 56
  6. theorem OAI.Erdos3.maskedSiteExpansion_error line 68
  7. theorem OAI.Erdos3.maskedSiteExpansion_coefficient_le_exp line 77
  8. theorem OAI.Erdos3.maskedSiteIndex_card line 86
  9. theorem OAI.Erdos3.unitCoefficientSource_abs_le line 99
  10. theorem OAI.Erdos3.jointUnitCoefficientSource_abs_le line 104
  11. theorem OAI.Erdos3.affineAuxiliaryVariables_joint_unit_bound line 112
  12. def OAI.Erdos3.averagedRegularizedIdeal line 130
  13. theorem OAI.Erdos3.regularizedAffineIdealDensity_joint_measurable line 139
  14. theorem OAI.Erdos3.averagedRegularizedIdeal_measurable line 152
  15. theorem OAI.Erdos3.averagedRegularizedIdeal_spec line 162
  16. def OAI.Erdos3.idealSiteLogBudget line 193
  17. theorem OAI.Erdos3.idealSiteLogBudget_bounds line 196
  18. theorem OAI.Erdos3.idealSiteProfile_bounds line 209
  19. def OAI.Erdos3.averagedIdealSiteFunction line 240
  20. theorem OAI.Erdos3.averagedIdealSiteFunction_bound line 243
  21. theorem OAI.Erdos3.averagedIdealSiteFunction_lipschitz line 248
  22. theorem OAI.Erdos3.exists_averaged_ideal_site_approximation line 268
  23. theorem OAI.Erdos3.exists_buffered_ideal_site_approximation line 315
  24. theorem OAI.Erdos3.exists_masked_ideal_site_approximation line 357
  25. def OAI.Erdos3.activeProfileIdeal line 413
  26. theorem OAI.Erdos3.activeProfileIdeal_measurable line 418
  27. def OAI.Erdos3.activeAveragedProfileIdeal line 425
  28. theorem OAI.Erdos3.activeAveragedProfileIdeal_measurable line 430
  29. theorem OAI.Erdos3.activeAveragedProfileIdeal_spec line 435
  30. theorem OAI.Erdos3.activeAveragedProfileIdeal_zero_outside line 456
  31. def OAI.Erdos3.activeProfileSample line 477
  32. theorem OAI.Erdos3.exists_active_averaged_profile_comparison line 489