OAI/Combinatorics/Progressions/Probability/PreparedModularGeneralCenteredLaw.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_weight_measurable line 16
  2. theorem OAI.Erdos3.selectedJointDensityMass_measurable line 36
  3. theorem OAI.Erdos3.selectedJointFiniteLaw_weight_measurable line 44
  4. theorem OAI.Erdos3.selectedJointFiniteLaw_realTest_measurable line 56
  5. theorem OAI.Erdos3.selectedJointFiniteLaw_realTest_integrable line 68
  6. theorem OAI.Erdos3.VectorPolynomial.jointSelectedPhysicalDensity_measurable_center line 105
  7. def OAI.Erdos3.VectorPolynomial.allocatedJointBaseDensity line 142
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedJointBaseDensity_nonneg line 152
  9. def OAI.Erdos3.VectorPolynomial.allocatedOriginalJointLaw line 178
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalJointLaw_source line 186
  11. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalSource_base_average_bound line 203
  12. def OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw line 260
  13. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_cube_source line 269
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_self_cube_source line 317
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_finite_self_cube_source line 338
  16. def OAI.Erdos3.VectorPolynomial.allocatedSlicedCubeSource line 364
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_sliced_cube_source line 377
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedJointBaseDensity_subtractConstant_affine line 434
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedJointBaseDensity_subtractConstant_selected line 448
  20. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_positive_affine line 478
  21. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_subtractConstant_eq_selected line 493
  22. def OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity line 533
  23. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity_eq_affine line 542
  24. theorem OAI.Erdos3.VectorPolynomial.allocatedJointBaseDensity_subtractConstant_centered line 556
  25. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity_nonneg line 573
  26. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity_measurable_center line 585
  27. theorem OAI.Erdos3.VectorPolynomial.allocatedOriginalPathLaw_subtractConstant_eq_centered line 607
  28. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity_cap line 665
  29. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointDensity_fixedScale_le_exp line 674
  30. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedScale_center_mixture_compare line 701
  31. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralCentered_degree line 821
  32. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralCentered_rank line 827
  33. theorem OAI.Erdos3.VectorPolynomial.preparedModularGeneralCenteredLaw line 850