OAI/Combinatorics/Progressions/Lattices/AffineCoefficientLaw.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineProbabilityProfile line 14
  2. theorem OAI.Erdos3.affineProbabilityProfile_nonneg line 17
  3. theorem OAI.Erdos3.affineProbabilityProfile_le line 21
  4. theorem OAI.Erdos3.affineProbabilityProfile_contDiff line 26
  5. theorem OAI.Erdos3.affineProbabilityProfile_zero line 32
  6. theorem OAI.Erdos3.affineProbabilityProfile_zero_outside line 39
  7. theorem OAI.Erdos3.affineProbabilityProfile_compact line 46
  8. theorem OAI.Erdos3.affineProbabilityProfile_integrable line 53
  9. theorem OAI.Erdos3.affineProbabilityProfile_integral line 58
  10. def OAI.Erdos3.affineProductProfile line 77
  11. def OAI.Erdos3.profileWidthFactor line 80
  12. theorem OAI.Erdos3.affineProductProfile_eq line 83
  13. theorem OAI.Erdos3.profileWidthFactor_pos line 89
  14. theorem OAI.Erdos3.affineProductProfile_nonneg line 92
  15. theorem OAI.Erdos3.affineProductProfile_norm_le line 96
  16. theorem OAI.Erdos3.affineProductProfile_contDiff line 102
  17. theorem OAI.Erdos3.affineProductProfile_compact line 110
  18. theorem OAI.Erdos3.affineProductProfile_integrable line 115
  19. theorem OAI.Erdos3.affineProductProfile_integral line 120
  20. theorem OAI.Erdos3.affineProductProfile_zero_outside line 126
  21. theorem OAI.Erdos3.affineProbabilityProfile_integral_test line 150
  22. theorem OAI.Erdos3.affineProbabilityProfile_law line 163
  23. theorem OAI.Erdos3.affineProductProfile_law line 182
  24. theorem OAI.Erdos3.affineProbabilityProfile_support line 215
  25. theorem OAI.Erdos3.realDensityMeasure_ae_of_support line 225
  26. def OAI.Erdos3.affineCoefficientMeasure line 231
  27. theorem OAI.Erdos3.affineCoefficientMeasure_probability line 234
  28. theorem OAI.Erdos3.affineCoefficientMeasure_support line 239
  29. theorem OAI.Erdos3.affineCoefficientMeasure_law line 244
  30. theorem OAI.Erdos3.affineProductProfile_integral_test line 260
  31. theorem OAI.Erdos3.affineProductProfile_retained_integral line 271
  32. theorem OAI.Erdos3.affineCoefficientDensity_unit_source line 279
  33. theorem OAI.Erdos3.affineProductProfile_measurable_comp line 298