OAI/Combinatorics/Progressions/Probability/ObservedDensityTesting.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.productSectionDensityWeight line 12
  2. theorem OAI.Erdos3.productSectionDensityWeight_nonneg line 17
  3. theorem OAI.Erdos3.productSectionDensityWeight_le line 24
  4. theorem OAI.Erdos3.productSectionDensityWeight_mul line 36
  5. def OAI.Erdos3.productNormalizedSectionWeight line 46
  6. theorem OAI.Erdos3.productNormalizedSectionWeight_nonneg line 50
  7. theorem OAI.Erdos3.productNormalizedSectionWeight_le line 56
  8. theorem OAI.Erdos3.productNormalizedSection_weighted_eq line 65
  9. theorem OAI.Erdos3.observedProductDensity_nonneg line 87
  10. theorem OAI.Erdos3.observedProductDensity_mono line 93
  11. theorem OAI.Erdos3.observedProductDensity_add line 103
  12. theorem OAI.Erdos3.observedProductDensity_zero line 116
  13. theorem OAI.Erdos3.observedProductDensity_mean line 122
  14. theorem OAI.Erdos3.observedProductDensity_marginal_le line 130
  15. theorem OAI.Erdos3.exists_massNormalizedSection_density_data line 155
  16. theorem OAI.Erdos3.productNormalizedSection_density_data line 197
  17. theorem OAI.Erdos3.observedProductDensity_factor line 235
  18. theorem OAI.Erdos3.observedProductDensity_bounded_factor line 244
  19. theorem OAI.Erdos3.ProductCylinder.normalized_density_data line 266
  20. def OAI.Erdos3.normalizedObservedDensity line 301
  21. theorem OAI.Erdos3.normalizedObservedDensity_factor line 304
  22. theorem OAI.Erdos3.FiniteProbabilityWeights.mean_fiber_factor line 329
  23. theorem OAI.Erdos3.observedProductDensity_test line 344
  24. theorem OAI.Erdos3.observedProductDensity_component_cap line 354