OAI/Combinatorics/Progressions/Estimates/ProductMeanPullback.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.productMean_reindex line 14
  2. theorem OAI.Erdos3.productComplexMean_reindex line 25
  3. def OAI.Erdos3.productSubtypePoint line 46
  4. theorem OAI.Erdos3.productSubtypePoint_apply_mem line 49
  5. theorem OAI.Erdos3.productSubtypePoint_restrict line 53
  6. theorem OAI.Erdos3.ProductDependsOn.subtypePoint line 58
  7. theorem OAI.Erdos3.productFiberIndicator_subtype line 79
  8. theorem OAI.Erdos3.productFiberIndicator_sum_subtype line 94
  9. theorem OAI.Erdos3.productFiberIndicator_partition line 99
  10. theorem OAI.Erdos3.productFiberMass_sum_subtype line 104
  11. theorem OAI.Erdos3.productMean_restrict line 124
  12. theorem OAI.Erdos3.productMean_of_depends line 159
  13. abbrev OAI.Erdos3.productTupleIndexEquiv line 179
  14. def OAI.Erdos3.productTuplePoint line 187
  15. theorem OAI.Erdos3.productTuplePoint_apply line 193
  16. theorem OAI.Erdos3.ProductDependsOn.tuplePoint line 202
  17. theorem OAI.Erdos3.productMean_tuple line 221
  18. theorem OAI.Erdos3.productMean_pullback line 250