OAI/Combinatorics/Progressions/Probability/PositiveDensityNormalization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.selectedJointDensityMass line 18
  2. def OAI.Erdos3.selectedJointReference line 21
  3. theorem OAI.Erdos3.selectedJointReference_densityMass line 25
  4. theorem OAI.Erdos3.selectedJointDensityMass_bounds line 34
  5. theorem OAI.Erdos3.selectedJointDensityMass_close line 41
  6. def OAI.Erdos3.selectedJointFiniteLaw line 47
  7. theorem OAI.Erdos3.selectedJointFiniteLaw_weight line 54
  8. theorem OAI.Erdos3.selectedJointFiniteLaw_complexMean line 66
  9. theorem OAI.Erdos3.selectedJointFiniteLaw_local_comparison line 75
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.prod_reweightPositive_mean_le_of_conditional line 120
  11. theorem OAI.Erdos3.selectedJointFiniteLaw_conditional_event_le line 149
  12. theorem OAI.Erdos3.selectedJointDensityMass_smooth_mass_pos line 193
  13. theorem OAI.Erdos3.selectedJointFiniteLaw_mass_le_reference line 226
  14. theorem OAI.Erdos3.selectedJointReference_retained_mass line 247
  15. theorem OAI.Erdos3.selectedJointReference_retained_exp_mass line 260
  16. theorem OAI.Erdos3.selectedJointFiniteLaw_weighted_expectation line 300
  17. def OAI.Erdos3.selectedJointTupleLaw line 320
  18. theorem OAI.Erdos3.selectedJointTupleLaw_complexMean line 324
  19. theorem OAI.Erdos3.selectedJointReference_residue_expectation line 359
  20. theorem OAI.Erdos3.selectedJointFiniteLaw_residue_expectation line 375
  21. theorem OAI.Erdos3.BooleanCubeKernel.selectedJointFiniteLaw_physical_cube line 396
  22. def OAI.Erdos3.residueCoordinateProductLaw line 435
  23. theorem OAI.Erdos3.residueSmoothIndexPMF_grouped line 446
  24. theorem OAI.Erdos3.residueSmoothIndexPMF_grouped_expectation line 455
  25. theorem OAI.Erdos3.selectedJointFiniteLaw_grouped_expectation line 465
  26. theorem OAI.Erdos3.positiveProjectionAccuracy_mass_bound line 500
  27. theorem OAI.Erdos3.positiveProjectionAccuracy_normalizer line 522
  28. theorem OAI.Erdos3.selectedJointDensityMass_positive_accuracy line 535