OAI/Combinatorics/Progressions/Probability/SampledWeightCellLaw.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.independentCoordinateDensity line 21
  2. theorem OAI.Erdos3.independentCoordinateDensity_measurable line 24
  3. theorem OAI.Erdos3.independentCoordinateDensity_integrable line 30
  4. theorem OAI.Erdos3.independentCoordinateDensity_mass line 33
  5. theorem OAI.Erdos3.independentCoordinateDensity_cap line 39
  6. theorem OAI.Erdos3.independentCoordinateDensity_lipschitz line 45
  7. theorem OAI.Erdos3.independentCoordinateDensity_test_product line 70
  8. theorem OAI.Erdos3.independentCoordinateDensity_lipschitz_uniform line 77
  9. theorem OAI.Erdos3.abs_sub_eq_add_sub_two_min line 94
  10. theorem OAI.Erdos3.integral_density_overlap line 101
  11. theorem OAI.Erdos3.density_overlap_mass line 111
  12. theorem OAI.Erdos3.product_density_l1_le_sum line 118
  13. def OAI.Erdos3.realDensityMeasure line 183
  14. theorem OAI.Erdos3.realDensityMeasure_apply line 186
  15. theorem OAI.Erdos3.realDensityMeasure_probability line 192
  16. theorem OAI.Erdos3.binaryDensity_measure line 199
  17. theorem OAI.Erdos3.independentCoordinateDensity_measure line 210
  18. theorem OAI.Erdos3.independentCoordinateDensity_translation_l1 line 245
  19. theorem OAI.Erdos3.measured_density_overlap line 277
  20. theorem OAI.Erdos3.tensor_density_l1_le_sum line 293
  21. theorem OAI.Erdos3.continuousDensity_eq_of_measure_eq line 355
  22. theorem OAI.Erdos3.sampledWeightMass_zero_off line 376
  23. def OAI.Erdos3.sampledWeightPMF line 381
  24. theorem OAI.Erdos3.sampledWeightPMF_apply line 391
  25. theorem OAI.Erdos3.sampledWeightPMF_singleton line 397
  26. theorem OAI.Erdos3.normalizedWeightHistogram_cell_integral line 414
  27. theorem OAI.Erdos3.normalizedWeightHistogram_probability line 423
  28. theorem OAI.Erdos3.normalizedWeightHistogram_cell_mass line 431
  29. theorem OAI.Erdos3.normalizedWeightHistogram_rounding_law line 439