OAI/Combinatorics/Progressions/Sampling/ControlledJointGrid.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.integrable_snd_probability line 13
  2. theorem OAI.Erdos3.integral_snd_probability line 21
  3. theorem OAI.Erdos3.retained_density_test_error line 29
  4. theorem OAI.Erdos3.pmf_real_integral_count line 65
  5. theorem OAI.Erdos3.independentPMF_count_density line 72
  6. theorem OAI.Erdos3.independentPMF_retained_grid_error line 84
  7. theorem OAI.Erdos3.realDensityMeasure_integral_complex line 130
  8. theorem OAI.Erdos3.density_bounded_complex_test_error line 138
  9. theorem OAI.Erdos3.retained_density_complex_test_error line 158
  10. theorem OAI.Erdos3.independentPMF_retained_complex_grid_error line 180
  11. theorem OAI.Erdos3.count_finite_sum_le_integral line 221
  12. theorem OAI.Erdos3.independentPMF_finite_test_error line 231
  13. theorem OAI.Erdos3.conditionalPMF_retained_grid_error line 267
  14. theorem OAI.Erdos3.gridDensityTest_independent line 303
  15. theorem OAI.Erdos3.independentPMF_grid_test_error line 323
  16. theorem OAI.Erdos3.fixed_mixed_output_grid_error line 368
  17. theorem OAI.Erdos3.coefficientGridBoxFactor_le_exp line 409
  18. theorem OAI.Erdos3.coefficientGridReplacementScale_le line 427
  19. theorem OAI.Erdos3.affineCoefficientGrid_joint_tolerance line 461