OAI/Combinatorics/Progressions/Probability/ScaledArrayLaw.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedQuotientDensity line 16
  2. theorem OAI.Erdos3.normalizedQuotientDensity_apply line 23
  3. theorem OAI.Erdos3.normalizedQuotientDensity_measurable line 31
  4. theorem OAI.Erdos3.normalizedQuotientDensity_nonneg line 39
  5. theorem OAI.Erdos3.normalizedQuotientDensity_bound line 49
  6. theorem OAI.Erdos3.normalizedQuotientDensity_law line 58
  7. theorem OAI.Erdos3.restrictedChartDensity_recover line 84
  8. theorem OAI.Erdos3.restrictedChartDensity_nonzero_iff line 96
  9. theorem OAI.Erdos3.normalizedQuotientDensity_recover line 105
  10. theorem OAI.Erdos3.mixedCoefficient_quotient_law line 127
  11. theorem OAI.Erdos3.mixedCoefficient_quotient_density line 151
  12. def OAI.Erdos3.canonicalMixedDensity line 205
  13. theorem OAI.Erdos3.canonicalMixedDensity_measurable line 209
  14. theorem OAI.Erdos3.canonicalMixedDensity_apply line 214
  15. theorem OAI.Erdos3.canonicalMixedDensity_recover line 222
  16. theorem OAI.Erdos3.canonicalMixedDensity_nonneg line 235
  17. theorem OAI.Erdos3.canonicalMixedDensity_bound line 242
  18. theorem OAI.Erdos3.canonicalMixedDensity_law line 252
  19. theorem OAI.Erdos3.canonicalMixedDensity_mass line 264
  20. theorem OAI.Erdos3.constantCoefficient_quotient_density line 294
  21. def OAI.Erdos3.mixedArrayQuotient line 342
  22. theorem OAI.Erdos3.mixedArrayQuotient_measurable line 349
  23. theorem OAI.Erdos3.mixedArray_quotient_density line 358
  24. def OAI.Erdos3.constantChartDistortion line 442
  25. def OAI.Erdos3.constantChartWidth line 444
  26. theorem OAI.Erdos3.constantChartWidth_pos line 447
  27. theorem OAI.Erdos3.constantChartWidth_small line 451
  28. def OAI.Erdos3.constantChartDensityCap line 461
  29. theorem OAI.Erdos3.constantChartDensityCap_nonneg line 465
  30. theorem OAI.Erdos3.exists_uniform_constant_quotient_density line 470
  31. theorem OAI.Erdos3.scaledCoefficientDensity_product_law line 522
  32. theorem OAI.Erdos3.scaledArrayLaw_rows line 534
  33. theorem OAI.Erdos3.scaledProfile_div_bound line 545
  34. theorem OAI.Erdos3.scaledAbs_le_of_bound line 551
  35. theorem OAI.Erdos3.scaledArray_quotient_density line 557