OAI/Combinatorics/Progressions/Probability/IntervalDivisorProbability.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FiniteProbabilityWeights.reweightPositive line 11
  2. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_weight line 15
  3. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_mean line 19
  4. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_complexMean line 24
  5. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_fiberLaw_weight line 31
  6. theorem OAI.Erdos3.FiniteProbabilityWeights.uniform_reweightPositive_eq line 38
  7. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mul_le_of_capped_comparison line 57
  8. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_test_le line 68
  9. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_lowWeightFibers_mass line 90
  10. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_remove_lowWeightFibers_error line 101
  11. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_lowWeightFibers_mass_le line 112
  12. def OAI.Erdos3.FiniteProbabilityWeights.normalizedDensityTest line 133
  13. theorem OAI.Erdos3.FiniteProbabilityWeights.normalizedDensityTest_norm_le_one line 136
  14. theorem OAI.Erdos3.FiniteProbabilityWeights.normalizedDensityTest_measurable line 144
  15. theorem OAI.Erdos3.FiniteProbabilityWeights.normalizedDensityTest_integrable line 151
  16. theorem OAI.Erdos3.FiniteProbabilityWeights.integral_normalizedDensityTest_compare line 159
  17. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_prod line 192
  18. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_mem_Icc line 197
  19. theorem OAI.Erdos3.FiniteProbabilityWeights.abs_mean_sub_const_le line 203
  20. theorem OAI.Erdos3.FiniteProbabilityWeights.reweightPositive_complexMean_eq_normalizedDensityTest line 210
  21. theorem OAI.Erdos3.FiniteProbabilityWeights.normalizedDensityTest_remove_normalization line 216
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.joint_normalization_compare line 222
  23. def OAI.Erdos3.FiniteProbabilityWeights.uniformFinset line 246
  24. theorem OAI.Erdos3.FiniteProbabilityWeights.uniformFinset_mean line 251
  25. theorem OAI.Erdos3.FiniteProbabilityWeights.uniformFinset_complexMean line 258
  26. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberLaw_complexMean line 275
  27. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberLaw_mean line 281
  28. def OAI.Erdos3.FiniteProbabilityWeights.siteLaw line 287
  29. theorem OAI.Erdos3.FiniteProbabilityWeights.siteLaw_mean line 291
  30. theorem OAI.Erdos3.FiniteProbabilityWeights.siteLaw_complexMean line 297
  31. def OAI.Erdos3.intervalUniformWeights line 313
  32. theorem OAI.Erdos3.intervalUniformWeights_mean line 318
  33. theorem OAI.Erdos3.interval_mod_probability line 324
  34. theorem OAI.Erdos3.interval_divisor_probability line 344