OAI/Combinatorics/Progressions/Probability/SlicedRemainderDensityFamily.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realDensityMeasure_map_add_right line 18
  2. theorem OAI.Erdos3.haarShiftDensity_image_law line 26
  3. theorem OAI.Erdos3.realDensityMeasure_le_of_cap line 40
  4. theorem OAI.Erdos3.haarShiftDensity_image_le line 47
  5. def OAI.Erdos3.sigmaAxisMeasure line 69
  6. instance OAI.Erdos3.sigmaAxisMeasure_probability line 72
  7. theorem OAI.Erdos3.sigmaAxisMeasure_projection line 77
  8. theorem OAI.Erdos3.sigmaAxisMeasure_integral line 85
  9. theorem OAI.Erdos3.sigmaAxisSampler_measurable line 92
  10. theorem OAI.Erdos3.sigmaAxisSampler_image_law line 97
  11. theorem OAI.Erdos3.sigmaAxisMeasure_withDensity line 127
  12. theorem OAI.Erdos3.sigmaAxisMeasure_volume line 136
  13. theorem OAI.Erdos3.sigmaAxisMeasure_density line 140
  14. theorem OAI.Erdos3.sigmaAxisMeasure_unitBox line 157
  15. theorem OAI.Erdos3.realDensityMeasure_unit_lift line 163
  16. theorem OAI.Erdos3.unit_lift_integral line 171
  17. theorem OAI.Erdos3.scalarJoint_image_density line 175
  18. def OAI.Erdos3.principalProductValue line 219
  19. theorem OAI.Erdos3.principalProductValue_measurable line 223
  20. def OAI.Erdos3.booleanOneCubeEndpoints line 228
  21. theorem OAI.Erdos3.booleanOneCubeEndpoints_eq line 234
  22. theorem OAI.Erdos3.booleanOneCubeEndpoints_measurable line 243
  23. theorem OAI.Erdos3.booleanOneCubeEndpoints_image line 250
  24. def OAI.Erdos3.jointBooleanSource line 280
  25. instance OAI.Erdos3.jointBooleanSource_probability line 283
  26. theorem OAI.Erdos3.jointBooleanSampler_image_law line 288
  27. def OAI.Erdos3.principalSliceValue line 308
  28. theorem OAI.Erdos3.principalSliceValue_measurable line 313
  29. def OAI.Erdos3.blockCubeShiftScale line 319
  30. theorem OAI.Erdos3.blockCubeShiftScale_measurable line 326
  31. theorem OAI.Erdos3.booleanOneCube_shiftScale line 334
  32. theorem OAI.Erdos3.slicedBooleanOneCube_image line 344
  33. def OAI.Erdos3.SlicedProductBlock.packPair line 379
  34. theorem OAI.Erdos3.SlicedProductBlock.packPair_measurePreserving line 382
  35. def OAI.Erdos3.SlicedProductBlock.packFour line 391
  36. theorem OAI.Erdos3.SlicedProductBlock.packFour_measurePreserving line 394
  37. def OAI.Erdos3.SlicedProductBlock.fourBoxPacking line 409
  38. theorem OAI.Erdos3.SlicedProductBlock.fourBoxPacking_measurePreserving line 412
  39. def OAI.Erdos3.SlicedProductBlock.fourBoxValue line 421
  40. theorem OAI.Erdos3.SlicedProductBlock.fourBoxValue_eq line 425
  41. theorem OAI.Erdos3.SlicedProductBlock.fourBoxValue_image line 430
  42. def OAI.Erdos3.principalSliceBlock line 448
  43. theorem OAI.Erdos3.principalSliceValue_eq_blocks line 457
  44. theorem OAI.Erdos3.principalSliceValue_four_image line 468
  45. theorem OAI.Erdos3.slicedBooleanOneCube_four_density line 483
  46. theorem OAI.Erdos3.independentShiftDensity_of_image line 506
  47. def OAI.Erdos3.principalSumBoxSplit line 530
  48. theorem OAI.Erdos3.principalSumBoxSplit_measurePreserving line 535
  49. theorem OAI.Erdos3.principalSliceValue_sum line 543
  50. def OAI.Erdos3.principalFourRemainderDensity line 555
  51. theorem OAI.Erdos3.principalSliceValue_extra_image line 566
  52. theorem OAI.Erdos3.principalFourRemainderDensity_bounds line 602
  53. theorem OAI.Erdos3.principalFourRemainderDensity_probability line 630
  54. theorem OAI.Erdos3.principalFourRemainderDensity_measurable line 642
  55. theorem OAI.Erdos3.slicedBooleanOneCube_extra_density line 649
  56. theorem OAI.Erdos3.slicedOneCube_extra_density_bounds line 662
  57. theorem OAI.Erdos3.principalSliceValue_reindex line 689
  58. theorem OAI.Erdos3.principalSliceValue_reindex_image line 706
  59. def OAI.Erdos3.reindexedSlicedPrincipalDensity line 730
  60. theorem OAI.Erdos3.reindexedSlicedPrincipalDensity_law_bounds line 737
  61. def OAI.Erdos3.fourBlockDecomposition line 758
  62. def OAI.Erdos3.canonicalSlicedPrincipalDensity line 762
  63. theorem OAI.Erdos3.canonicalSlicedPrincipalDensity_law_bounds line 767
  64. theorem OAI.Erdos3.independentShiftDensity_measurable_family line 791
  65. theorem OAI.Erdos3.principalFourRemainderDensity_measurable_family line 802
  66. theorem OAI.Erdos3.canonicalSlicedPrincipalDensity_measurable_family line 829