OAI/Combinatorics/Progressions/Probability/SpatialProductDensity.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.affinePairDensity_measurable_family line 13
  2. theorem OAI.Erdos3.scalarDensityConvolution_measurable_family line 32
  3. structure OAI.Erdos3.SlicedProductBlock.MeasurableFamily line 54
  4. theorem OAI.Erdos3.SlicedProductBlock.prefixProduct_measurable_family line 61
  5. theorem OAI.Erdos3.SlicedProductBlock.slope_measurable_family line 69
  6. theorem OAI.Erdos3.SlicedProductBlock.base_measurable_family line 74
  7. theorem OAI.Erdos3.SlicedProductBlock.pairDensity_measurable_family line 79
  8. theorem OAI.Erdos3.SlicedProductBlock.fourDensity_measurable_family line 94
  9. def OAI.Erdos3.SlicedProductBlock.mixedFourDensity line 115
  10. theorem OAI.Erdos3.SlicedProductBlock.mixedFourDensity_spec line 118
  11. theorem OAI.Erdos3.SlicedProductBlock.mixedFourDensity_test_integral line 140
  12. abbrev OAI.Erdos3.SlicedProductBlock.PairInput line 168
  13. def OAI.Erdos3.SlicedProductBlock.pairSource line 170
  14. instance OAI.Erdos3.SlicedProductBlock.pairSource_probability line 174
  15. def OAI.Erdos3.SlicedProductBlock.pairValue line 178
  16. theorem OAI.Erdos3.SlicedProductBlock.pairValue_measurable line 181
  17. theorem OAI.Erdos3.SlicedProductBlock.pairSource_image line 185
  18. abbrev OAI.Erdos3.SlicedProductBlock.FourInput line 209
  19. def OAI.Erdos3.SlicedProductBlock.fourSource line 211
  20. instance OAI.Erdos3.SlicedProductBlock.fourSource_probability line 214
  21. def OAI.Erdos3.SlicedProductBlock.fourValue line 218
  22. theorem OAI.Erdos3.SlicedProductBlock.fourValue_measurable line 221
  23. theorem OAI.Erdos3.SlicedProductBlock.fourSource_image line 226
  24. theorem OAI.Erdos3.SlicedProductBlock.twoSiteSource_image line 243
  25. def OAI.Erdos3.SlicedProductBlock.jointMixedDensity line 268
  26. theorem OAI.Erdos3.SlicedProductBlock.jointMixedDensity_spec line 272
  27. theorem OAI.Erdos3.SlicedProductBlock.jointMixedDensity_test_product line 287
  28. def OAI.Erdos3.SlicedProductBlock.twoSiteDensity line 315
  29. theorem OAI.Erdos3.SlicedProductBlock.twoSiteDensity_probability line 319
  30. theorem OAI.Erdos3.SlicedProductBlock.twoSiteDensity_uniform_slice_bound line 328
  31. theorem OAI.Erdos3.SlicedProductBlock.value_measurable_family line 343
  32. theorem OAI.Erdos3.SlicedProductBlock.pairValue_measurable_family line 350
  33. theorem OAI.Erdos3.SlicedProductBlock.fourValue_measurable_family line 358
  34. theorem OAI.Erdos3.SlicedProductBlock.twoSiteDensity_measurable_family line 367
  35. theorem OAI.Erdos3.SlicedProductBlock.averagedTwoSiteDensity_image line 381
  36. theorem OAI.Erdos3.SlicedProductBlock.averagedTwoSiteDensity_of_bounds line 398
  37. theorem OAI.Erdos3.SlicedProductBlock.averagedTwoSiteDensity_uniform_bound line 411
  38. def OAI.Erdos3.spatialProductDensity line 444
  39. theorem OAI.Erdos3.spatialProductDensity_spec line 449
  40. theorem OAI.Erdos3.spatialProductDensity_test_product line 478