OAI/Combinatorics/Progressions/Lattices/AveragedAffineGrid.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.flatAffineMixtureDensity line 27
  2. def OAI.Erdos3.flatAffineUnitSource line 31
  3. theorem OAI.Erdos3.flatAffineUnitSource_measurable line 40
  4. theorem OAI.Erdos3.flatAffineMixtureDensity_measurable line 53
  5. theorem OAI.Erdos3.flatAffineMixtureDensity_image_law line 64
  6. theorem OAI.Erdos3.flatAffineMixtureDensity_probability line 109
  7. theorem OAI.Erdos3.flatAffineMixtureDensity_bounds line 127
  8. theorem OAI.Erdos3.canonicalAffineRawArray_retained_test line 156
  9. def OAI.Erdos3.smallAffineMixtureDensity line 232
  10. theorem OAI.Erdos3.smallAffineMixtureDensity_measurable line 242
  11. theorem OAI.Erdos3.smallAffineMixtureDensity_probability line 253
  12. theorem OAI.Erdos3.smallAffineMixtureDensity_bounds line 292
  13. theorem OAI.Erdos3.smallAffineMixtureDensity_support line 317
  14. theorem OAI.Erdos3.smallAffineMixtureDensity_test line 346
  15. theorem OAI.Erdos3.smallAffineMixtureDensity_log_bounds line 392
  16. theorem OAI.Erdos3.exists_averaged_regularized_affine_l1_with_parameters line 439
  17. theorem OAI.Erdos3.exists_averaged_regularized_affine_l1 line 529
  18. theorem OAI.Erdos3.averagedAffine_density_data line 592
  19. theorem OAI.Erdos3.exists_averaged_affine_l1_with_parameter_bounds line 662
  20. theorem OAI.Erdos3.averagedAffine_grid_error line 751