OAI/Combinatorics/Progressions/Linear/ProductANOVATensorChoices.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ProductNoSingletonCoordinate line 18
  2. def OAI.Erdos3.productANOVAMomentChoices line 21
  3. theorem OAI.Erdos3.productANOVA_moment_expansion line 25
  4. theorem OAI.Erdos3.productANOVA_term_zero_of_singleton_count line 34
  5. theorem OAI.Erdos3.productANOVA_moment_without_singletons line 53
  6. def OAI.Erdos3.coordinateUnionWeight line 83
  7. theorem OAI.Erdos3.coordinateUnionWeight_nonneg line 86
  8. def OAI.Erdos3.productANOVATensor line 89
  9. theorem OAI.Erdos3.productANOVATensor_zero_of_not_ordered line 98
  10. theorem OAI.Erdos3.productANOVATensor_zero_of_zero_weight line 103
  11. theorem OAI.Erdos3.productANOVATensor_zero_of_repeated line 110
  12. theorem OAI.Erdos3.productANOVATensor_basepoint line 117
  13. theorem OAI.Erdos3.productANOVATensor_weighted_sq line 132
  14. theorem OAI.Erdos3.productANOVATensor_evaluate line 162
  15. theorem OAI.Erdos3.productANOVATensor_sum_evaluate line 177
  16. theorem OAI.Erdos3.productANOVATensor_null_section line 196
  17. theorem OAI.Erdos3.productANOVATensor_moment_expansion line 218
  18. theorem OAI.Erdos3.productANOVATensor_mean_product line 247
  19. theorem OAI.Erdos3.productANOVATensor_mean_zero_of_not_ordered line 260
  20. theorem OAI.Erdos3.productANOVATensor_mean_zero_of_singleton line 272
  21. def OAI.Erdos3.productANOVATensorChoices line 295
  22. theorem OAI.Erdos3.mem_productANOVATensorChoices line 300
  23. theorem OAI.Erdos3.productANOVATensor_moment_admissible line 308
  24. theorem OAI.Erdos3.productANOVATensor_abs_moment_le line 330