OAI/Combinatorics/Progressions/Probability/PairedProductDensity.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.densityMixture line 14
  2. theorem OAI.Erdos3.densityMixture_section_integrable line 17
  3. theorem OAI.Erdos3.densityMixture_cap line 24
  4. theorem OAI.Erdos3.densityMixture_lipschitz line 36
  5. theorem OAI.Erdos3.densityMixture_joint_integrable line 55
  6. theorem OAI.Erdos3.densityMixture_probability_density line 67
  7. theorem OAI.Erdos3.densityMixture_l1_le line 93
  8. theorem OAI.Erdos3.measurable_normalizedIntervalWindow line 125
  9. def OAI.Erdos3.randomIntervalDensity line 134
  10. theorem OAI.Erdos3.randomIntervalDensity_cap line 138
  11. theorem OAI.Erdos3.randomIntervalDensity_probability_density line 149
  12. theorem OAI.Erdos3.densityMixture_uniform_bound line 172
  13. theorem OAI.Erdos3.densityMixture_test_integral line 196
  14. theorem OAI.Erdos3.densityMixture_translation_l1 line 221
  15. def OAI.Erdos3.unitScalarMeasure line 258
  16. instance OAI.Erdos3.unitScalarMeasure_probability line 260
  17. theorem OAI.Erdos3.normalizedIntervalWindow_test_integral line 264
  18. theorem OAI.Erdos3.randomIntervalDensity_measurable line 281
  19. theorem OAI.Erdos3.randomIntervalDensity_test_integral line 289
  20. def OAI.Erdos3.haarShiftDensity line 332
  21. theorem OAI.Erdos3.haarShiftDensity_measurable line 339
  22. theorem OAI.Erdos3.haarShiftDensity_cap line 346
  23. theorem OAI.Erdos3.haarShiftDensity_probability line 355
  24. theorem OAI.Erdos3.haarShiftDensity_test_integral line 366
  25. def OAI.Erdos3.independentShiftDensity line 397
  26. theorem OAI.Erdos3.independentShiftDensity_measurable line 400
  27. theorem OAI.Erdos3.independentShiftDensity_cap line 407
  28. theorem OAI.Erdos3.independentShiftDensity_lipschitz line 417
  29. theorem OAI.Erdos3.independentShiftDensity_joint_integrable line 434
  30. theorem OAI.Erdos3.independentShiftDensity_probability_density line 444
  31. theorem OAI.Erdos3.independentShiftDensity_test_integral line 455
  32. theorem OAI.Erdos3.densityMixture_test_integral_complex line 488
  33. theorem OAI.Erdos3.haarShiftDensity_test_integral_complex line 507
  34. def OAI.Erdos3.pairedProductParameterMeasure line 540
  35. instance OAI.Erdos3.pairedProductParameterMeasure_probability line 544
  36. def OAI.Erdos3.pairedProductWidth line 548
  37. def OAI.Erdos3.pairedProductShift line 550
  38. theorem OAI.Erdos3.pairedProductWidth_measurable line 553
  39. theorem OAI.Erdos3.pairedProductShift_measurable line 556
  40. theorem OAI.Erdos3.pairedProductWidth_pos line 560
  41. theorem OAI.Erdos3.pairedProductWidth_inverse_integrable line 564
  42. theorem OAI.Erdos3.pairedProductWidth_inverse_integral_le line 568
  43. def OAI.Erdos3.pairedProductDensity line 574
  44. theorem OAI.Erdos3.pairedProductDensity_measurable line 577
  45. theorem OAI.Erdos3.pairedProductDensity_cap line 580
  46. theorem OAI.Erdos3.pairedProductDensity_probability_density line 587
  47. theorem OAI.Erdos3.pairedProductDensity_test_sorted line 593