OAI/Combinatorics/Progressions/Estimates/PinnedSectionMeans.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productCoordinateMix_section line 14
  2. abbrev OAI.Erdos3.ProductCylinder line 33
  3. def OAI.Erdos3.ProductCylinder.ofAssignment line 39
  4. def OAI.Erdos3.ProductCylinder.assignment line 42
  5. def OAI.Erdos3.ProductCylinder.Contains line 45
  6. theorem OAI.Erdos3.ProductCylinder.assignment_mem line 48
  7. theorem OAI.Erdos3.ProductCylinder.contains_iff line 52
  8. theorem OAI.Erdos3.ProductCylinder.contains_assignment line 61
  9. def OAI.Erdos3.ProductCylinder.bounded line 68
  10. theorem OAI.Erdos3.ProductCylinder.mem_bounded line 72
  11. theorem OAI.Erdos3.ProductCylinder.bounded_nonempty line 77
  12. def OAI.Erdos3.ProductCylinder.mass line 81
  13. theorem OAI.Erdos3.ProductCylinder.mass_ofAssignment line 85
  14. theorem OAI.Erdos3.ProductCylinder.mass_empty line 94
  15. theorem OAI.Erdos3.ProductCylinder.mass_mono line 99
  16. def OAI.Erdos3.productSectionAverage line 117
  17. theorem OAI.Erdos3.productSectionAverage_depends line 122
  18. theorem OAI.Erdos3.productSectionAverage_nonneg line 135
  19. theorem OAI.Erdos3.productSectionAverage_le line 140
  20. theorem OAI.Erdos3.productConditionalMean_sectionAverage line 146
  21. theorem OAI.Erdos3.productSectionAverage_eq_conditionalMean line 156
  22. theorem OAI.Erdos3.ProductCylinder.bounded_card line 176
  23. theorem OAI.Erdos3.ProductCylinder.bounded_card_le line 187
  24. def OAI.Erdos3.ProductCylinder.score line 214
  25. def OAI.Erdos3.ProductCylinder.Maximizes line 216
  26. theorem OAI.Erdos3.ProductCylinder.exists_maximizer line 219
  27. theorem OAI.Erdos3.ProductCylinder.Maximizes.empty_le line 227
  28. theorem OAI.Erdos3.ProductCylinder.Maximizes.mass_gt line 235
  29. theorem OAI.Erdos3.ProductCylinder.Maximizes.card_le line 242
  30. theorem OAI.Erdos3.ProductCylinder.Maximizes.refinement_bound line 255
  31. theorem OAI.Erdos3.productSectionAverage_self line 287
  32. theorem OAI.Erdos3.productFiberIndicator_mul_section line 292
  33. theorem OAI.Erdos3.productSectionAverage_mono line 317
  34. theorem OAI.Erdos3.productSectionAverage_smul line 322
  35. theorem OAI.Erdos3.productSectionAverage_weighted_cap line 327
  36. theorem OAI.Erdos3.productSectionAverage_weighted_zero line 341
  37. def OAI.Erdos3.ProductBoundedMarginals line 361
  38. def OAI.Erdos3.productNormalizedSection line 366
  39. theorem OAI.Erdos3.productNormalizedSection_nonneg line 370
  40. theorem OAI.Erdos3.productNormalizedSection_le line 375
  41. theorem OAI.Erdos3.productNormalizedSection_boundedMarginals line 384
  42. theorem OAI.Erdos3.productSectionAverage_eq_normalized line 412
  43. def OAI.Erdos3.ProductCylinder.normalizedSection line 428
  44. theorem OAI.Erdos3.ProductCylinder.Maximizes.normalized_bounded line 433
  45. theorem OAI.Erdos3.ProductCylinder.exists_regular line 454
  46. def OAI.Erdos3.ProductMarginalsClose line 476
  47. theorem OAI.Erdos3.ProductMarginalsClose.mono line 480
  48. theorem OAI.Erdos3.ProductMarginalsClose.section line 484
  49. theorem OAI.Erdos3.ProductBoundedMarginals.mono line 496
  50. theorem OAI.Erdos3.scaled_bounded_marginals line 511
  51. theorem OAI.Erdos3.productSectionAverage_self_mean line 532
  52. theorem OAI.Erdos3.ProductCylinder.normalizedSection_mean line 539