OAI/Combinatorics/Progressions/FixedDensity/Energy.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.FixedDensity.mean line 17
  2. def OAI.Erdos3.FixedDensity.finsetIndicator line 20
  3. theorem OAI.Erdos3.FixedDensity.finsetIndicator_of_mem line 25
  4. theorem OAI.Erdos3.FixedDensity.finsetIndicator_of_not_mem line 31
  5. theorem OAI.Erdos3.FixedDensity.mean_finsetIndicator line 36
  6. theorem OAI.Erdos3.FixedDensity.mean_empty line 44
  7. theorem OAI.Erdos3.FixedDensity.mean_const line 49
  8. theorem OAI.Erdos3.FixedDensity.mean_zero line 54
  9. theorem OAI.Erdos3.FixedDensity.mean_add line 58
  10. theorem OAI.Erdos3.FixedDensity.mean_sub line 62
  11. theorem OAI.Erdos3.FixedDensity.mean_smul line 66
  12. theorem OAI.Erdos3.FixedDensity.mean_nonneg line 70
  13. theorem OAI.Erdos3.FixedDensity.mean_mono line 75
  14. theorem OAI.Erdos3.FixedDensity.mean_le_of_le_const line 81
  15. theorem OAI.Erdos3.FixedDensity.const_le_mean line 86
  16. def OAI.Erdos3.FixedDensity.mean₂ line 91
  17. theorem OAI.Erdos3.FixedDensity.mean₂_comm line 95
  18. def OAI.Erdos3.FixedDensity.cyclicAPTerm line 110
  19. def OAI.Erdos3.FixedDensity.cyclicAPProduct line 113
  20. def OAI.Erdos3.FixedDensity.cyclicAPCount line 117
  21. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_nonneg line 121
  22. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_nonneg line 126
  23. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_const line 136
  24. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_smul line 140
  25. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_const line 148
  26. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_smul line 152
  27. theorem OAI.Erdos3.FixedDensity.cyclicAPProduct_mono line 158
  28. theorem OAI.Erdos3.FixedDensity.cyclicAPCount_mono line 166
  29. theorem OAI.Erdos3.FixedDensity.mean_finset_sum line 186
  30. theorem OAI.Erdos3.FixedDensity.one_sub_sum_le_prod_one_sub line 196
  31. theorem OAI.Erdos3.FixedDensity.prod_one_sub_le_orderedPair_bonferroni line 222
  32. theorem OAI.Erdos3.FixedDensity.mean_prod_type line 279
  33. theorem OAI.Erdos3.FixedDensity.mean_fin_cons line 287
  34. theorem OAI.Erdos3.FixedDensity.prod_mean line 307
  35. def OAI.Erdos3.FixedDensity.conditionalMean line 328
  36. theorem OAI.Erdos3.FixedDensity.conditionalMean_eq_of_part_eq line 334
  37. theorem OAI.Erdos3.FixedDensity.conditionalMean_eq_of_mem_part line 342
  38. theorem OAI.Erdos3.FixedDensity.conditionalMean_nonneg line 353
  39. theorem OAI.Erdos3.FixedDensity.conditionalMean_add line 360
  40. theorem OAI.Erdos3.FixedDensity.conditionalMean_sub line 368
  41. theorem OAI.Erdos3.FixedDensity.conditionalMean_smul line 376
  42. theorem OAI.Erdos3.FixedDensity.conditionalMean_le_one line 384
  43. theorem OAI.Erdos3.FixedDensity.conditionalMean_const line 394
  44. theorem OAI.Erdos3.FixedDensity.conditionalMean_idem line 403
  45. theorem OAI.Erdos3.FixedDensity.sum_conditionalMean_on_part line 420
  46. theorem OAI.Erdos3.FixedDensity.sum_conditionalMean line 435
  47. theorem OAI.Erdos3.FixedDensity.mean_conditionalMean line 460
  48. theorem OAI.Erdos3.FixedDensity.conditionalMean_sq_le line 469
  49. def OAI.Erdos3.FixedDensity.partitionEnergy line 481
  50. theorem OAI.Erdos3.FixedDensity.partitionEnergy_nonneg line 487
  51. theorem OAI.Erdos3.FixedDensity.partitionEnergy_le_mean_sq line 494
  52. theorem OAI.Erdos3.FixedDensity.partitionEnergy_le_one line 506
  53. abbrev OAI.Erdos3.FixedDensity.FacePartition line 527
  54. theorem OAI.Erdos3.FixedDensity.FacePartition.ext_of_part_eq line 534
  55. theorem OAI.Erdos3.FixedDensity.FacePartition.part_subset_of_le line 552
  56. theorem OAI.Erdos3.FixedDensity.FacePartition.le_iff_part_subset line 562
  57. def OAI.Erdos3.FixedDensity.FacePartition.indiscrete line 572
  58. def OAI.Erdos3.FixedDensity.FacePartition.discrete line 575
  59. theorem OAI.Erdos3.FixedDensity.FacePartition.part_indiscrete line 579
  60. theorem OAI.Erdos3.FixedDensity.FacePartition.part_discrete line 591
  61. def OAI.Erdos3.FixedDensity.FacePartition.complexity line 598
  62. def OAI.Erdos3.FixedDensity.FacePartition.representative line 601
  63. theorem OAI.Erdos3.FixedDensity.FacePartition.representative_mem line 605
  64. theorem OAI.Erdos3.FixedDensity.FacePartition.part_representative line 610
  65. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_antitone line 615
  66. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_le_card line 620
  67. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_discrete line 625
  68. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_indiscrete line 630
  69. def OAI.Erdos3.FixedDensity.FacePartition.join line 654
  70. theorem OAI.Erdos3.FixedDensity.FacePartition.join_le_left line 657
  71. theorem OAI.Erdos3.FixedDensity.FacePartition.join_le_right line 661
  72. theorem OAI.Erdos3.FixedDensity.FacePartition.le_join_iff line 665
  73. theorem OAI.Erdos3.FixedDensity.FacePartition.part_join line 670
  74. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_join_le line 682
  75. def OAI.Erdos3.FixedDensity.FacePartition.joinFinset line 699
  76. theorem OAI.Erdos3.FixedDensity.FacePartition.joinFinset_empty line 705
  77. theorem OAI.Erdos3.FixedDensity.FacePartition.joinFinset_insert line 711
  78. theorem OAI.Erdos3.FixedDensity.FacePartition.joinFinset_le_of_mem line 717
  79. theorem OAI.Erdos3.FixedDensity.FacePartition.le_joinFinset_iff line 723
  80. theorem OAI.Erdos3.FixedDensity.FacePartition.mem_part_joinFinset_iff line 729
  81. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_joinFinset_le line 744
  82. def OAI.Erdos3.FixedDensity.FacePartition.generatedBy line 768
  83. theorem OAI.Erdos3.FixedDensity.FacePartition.mem_part_generatedBy_iff line 772
  84. theorem OAI.Erdos3.FixedDensity.FacePartition.generatedBy_antitone line 809
  85. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_generatedBy_le line 818
  86. theorem OAI.Erdos3.FixedDensity.FacePartition.generatedBy_empty line 823
  87. theorem OAI.Erdos3.FixedDensity.FacePartition.generatedBy_union line 831
  88. theorem OAI.Erdos3.FixedDensity.FacePartition.generatedBy_insert line 852
  89. abbrev OAI.Erdos3.FixedDensity.FacePartition.atomSetoid line 862
  90. theorem OAI.Erdos3.FixedDensity.FacePartition.atomSetoid_rel line 866
  91. def OAI.Erdos3.FixedDensity.FacePartition.pullbackSetoid line 870
  92. instance OAI.Erdos3.FixedDensity.FacePartition.instDecidableRelPullbackSetoid line 878
  93. def OAI.Erdos3.FixedDensity.FacePartition.pullback line 886
  94. theorem OAI.Erdos3.FixedDensity.FacePartition.mem_part_pullback_iff line 891
  95. theorem OAI.Erdos3.FixedDensity.FacePartition.mem_part_pullback_iff_image_mem line 904
  96. theorem OAI.Erdos3.FixedDensity.FacePartition.part_pullback_eq_filter line 922
  97. theorem OAI.Erdos3.FixedDensity.FacePartition.pullback_mono line 932
  98. theorem OAI.Erdos3.FixedDensity.FacePartition.pullback_id line 943
  99. theorem OAI.Erdos3.FixedDensity.FacePartition.pullback_comp line 950
  100. theorem OAI.Erdos3.FixedDensity.FacePartition.complexity_pullback_le line 962
  101. theorem OAI.Erdos3.FixedDensity.sum_conditionalMean_on_coarser_part line 1016
  102. theorem OAI.Erdos3.FixedDensity.conditionalMean_tower_of_le line 1063
  103. theorem OAI.Erdos3.FixedDensity.conditionalMean_reverse_tower_of_le line 1077
  104. theorem OAI.Erdos3.FixedDensity.conditionalMean_mul_right_of_constant_on_part line 1094
  105. theorem OAI.Erdos3.FixedDensity.conditionalMean_mul_conditionalMean_right line 1112
  106. theorem OAI.Erdos3.FixedDensity.mean_conditionalMean_mul_eq_sq_of_le line 1121
  107. theorem OAI.Erdos3.FixedDensity.partitionEnergy_pythagorean line 1152
  108. theorem OAI.Erdos3.FixedDensity.partitionEnergy_sub_eq_mean_sq line 1197
  109. theorem OAI.Erdos3.FixedDensity.partitionEnergy_mono line 1207
  110. theorem OAI.Erdos3.FixedDensity.partitionEnergy_mem_Icc line 1215
  111. theorem OAI.Erdos3.FixedDensity.partitionEnergy_refinement_bounds line 1223