OAI/Combinatorics/Progressions/Probability/DensityMixtureAELaw.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarDensityConvolution line 13
  2. theorem OAI.Erdos3.scalarDensityConvolution_lipschitz line 16
  3. theorem OAI.Erdos3.scalarDensityConvolution_cap line 26
  4. theorem OAI.Erdos3.scalarDensityConvolution_joint_integrable line 36
  5. theorem OAI.Erdos3.scalarDensityConvolution_integrable line 49
  6. theorem OAI.Erdos3.scalarDensityConvolution_mass line 54
  7. theorem OAI.Erdos3.scalarDensityConvolution_test_integral line 64
  8. theorem OAI.Erdos3.realDensityMeasure_map_equiv line 100
  9. theorem OAI.Erdos3.realDensityMeasure_pi line 110
  10. theorem OAI.Erdos3.finiteMeasure_eq_of_integrals line 131
  11. theorem OAI.Erdos3.imageLaw_eq_density_of_bounded_tests line 149
  12. theorem OAI.Erdos3.scalarDensityConvolution_image_law line 169
  13. theorem OAI.Erdos3.densityMixture_mappedTest line 210
  14. theorem OAI.Erdos3.densityMixture_image_law line 232
  15. theorem OAI.Erdos3.pmf_support_ae line 271
  16. theorem OAI.Erdos3.pmf_real_mass line 278
  17. theorem OAI.Erdos3.pmf_real_integrable line 281
  18. theorem OAI.Erdos3.pmf_realDensity_count line 287
  19. theorem OAI.Erdos3.independentIntegerLaw_density line 294
  20. theorem OAI.Erdos3.realDensityMeasure_map_embedding line 314
  21. theorem OAI.Erdos3.realDensityMeasure_restrict_support line 324
  22. theorem OAI.Erdos3.realDensityMeasure_smul_real line 335
  23. def OAI.Erdos3.embeddingDensity line 345
  24. theorem OAI.Erdos3.embeddingDensity_apply line 349
  25. theorem OAI.Erdos3.embeddingDensity_zero line 354
  26. theorem OAI.Erdos3.embeddingDensity_measurable line 358
  27. theorem OAI.Erdos3.embeddingDensity_nonneg line 363
  28. theorem OAI.Erdos3.embeddingDensity_bound line 373
  29. theorem OAI.Erdos3.embeddingDensity_law line 383
  30. theorem OAI.Erdos3.measurePreserving_realDensity_map line 401
  31. theorem OAI.Erdos3.productDensity_pushforward line 427
  32. theorem OAI.Erdos3.densityMixture_mappedTest_of_ae line 455
  33. theorem OAI.Erdos3.densityMixture_image_law_of_ae line 477