OAI/Combinatorics/Progressions/Probability/RegularizedSigmaDensity.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.retainedDensity_mappedTest line 12
  2. theorem OAI.Erdos3.retainedDensity_image_law line 38
  3. theorem OAI.Erdos3.retained_density_l1_comparison line 82
  4. theorem OAI.Erdos3.retained_density_grid_comparison line 104
  5. theorem OAI.Erdos3.affineProductProfile_measurable_center line 143
  6. def OAI.Erdos3.regularizedImageMap line 153
  7. def OAI.Erdos3.regularizedImageDensity line 156
  8. theorem OAI.Erdos3.regularizedImageMap_measurable line 160
  9. theorem OAI.Erdos3.regularizedImageDensity_joint_measurable line 164
  10. theorem OAI.Erdos3.regularizedImageDensity_measurable line 171
  11. theorem OAI.Erdos3.regularizedImageDensity_probability line 176
  12. theorem OAI.Erdos3.regularizedImageDensity_bounds line 187
  13. theorem OAI.Erdos3.regularizedImageDensity_image_law line 205
  14. theorem OAI.Erdos3.regularizedImageDensity_support line 221
  15. theorem OAI.Erdos3.conditionalRegularizedDensity_measurable line 244
  16. theorem OAI.Erdos3.conditionalRegularizedDensity_image_law line 255
  17. theorem OAI.Erdos3.conditionalRegularizedDensity_test_error line 274
  18. theorem OAI.Erdos3.conditionalRegularizedDensity_comparison line 313
  19. theorem OAI.Erdos3.unitCoefficientSource_sigma line 353
  20. theorem OAI.Erdos3.regularizedImageDensity_sigma line 366