OAI/Combinatorics/Progressions/Probability/DiagonalImageDensity.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realDensityMeasure_integral line 14
  2. theorem OAI.Erdos3.realDensityMeasure_finite line 22
  3. theorem OAI.Erdos3.realDensityMeasure_real_univ line 29
  4. theorem OAI.Erdos3.mappedTest_eq_density line 36
  5. theorem OAI.Erdos3.imageTranslationBound_of_density line 45
  6. def OAI.Erdos3.fixedSpatialBlockDensity line 85
  7. def OAI.Erdos3.fixedSpatialBlockDensityCap line 92
  8. def OAI.Erdos3.fixedSpatialBlockDensityLipschitz line 96
  9. theorem OAI.Erdos3.fixedSpatialBlockKernel_lipschitz line 102
  10. theorem OAI.Erdos3.fixedSpatialBlockDensity_measurable line 109
  11. theorem OAI.Erdos3.fixedSpatialBlockDensity_bounds line 116
  12. theorem OAI.Erdos3.fixedSpatialBlockDensity_probability_density line 140
  13. theorem OAI.Erdos3.fixedSpatialBlockDensity_probability line 154
  14. theorem OAI.Erdos3.fixedSpatialBlockDensity_real_test_integral line 161
  15. theorem OAI.Erdos3.fixedSpatialBlockDensity_complex_test_integral line 194
  16. theorem OAI.Erdos3.boundedDensity_mass line 237
  17. theorem OAI.Erdos3.density_l1_le_of_bounded_tests line 260
  18. theorem OAI.Erdos3.imageComparison_density_l1 line 289
  19. theorem OAI.Erdos3.realDensityMeasure_mul line 313
  20. theorem OAI.Erdos3.ae_realDensityMeasure_of_forall_nonzero line 322
  21. theorem OAI.Erdos3.fixedSpatialBlockDensityCap_eq line 344
  22. theorem OAI.Erdos3.fixedSpatialNegBlock_inverse_norm line 350
  23. theorem OAI.Erdos3.fixedSpatialBlockDensityLipschitz_eq line 362
  24. theorem OAI.Erdos3.fixedSpatialBlockDensity_bounds_of_inverseBounds line 375
  25. theorem OAI.Erdos3.boxProbabilityWindow_one_eq_indicator line 407
  26. theorem OAI.Erdos3.unitBoxMeasure_eq_boxWindowDensity line 424
  27. theorem OAI.Erdos3.unitBoxMeasure_real_integral line 436
  28. theorem OAI.Erdos3.fixedSpatialBlockDensity_mapped_real_integral line 445
  29. theorem OAI.Erdos3.fixedSpatialBlockDensity_image_law line 471
  30. theorem OAI.Erdos3.coordinateScaleEquiv_det line 509
  31. def OAI.Erdos3.diagonalImageDensity line 513
  32. theorem OAI.Erdos3.diagonalImageDensity_eq_pullback line 517
  33. theorem OAI.Erdos3.diagonalImageDensity_measurable line 525
  34. theorem OAI.Erdos3.diagonalImageDensity_nonneg line 530
  35. theorem OAI.Erdos3.diagonalImageDensity_integrable line 535
  36. theorem OAI.Erdos3.diagonalImageDensity_integral line 540
  37. theorem OAI.Erdos3.diagonalImageDensity_test_integral line 545
  38. theorem OAI.Erdos3.diagonalImageDensity_l1_le_of_tests line 551