OAI/Combinatorics/Progressions/Linear/ProductANOVAEnergyOrder.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.alternating_powerset_sum_zero line 16
2. def OAI.Erdos3.productANOVA line 32
3. theorem OAI.Erdos3.productANOVA_inclusion_exclusion line 35
4. theorem OAI.Erdos3.productANOVA_depends line 56
5. theorem OAI.Erdos3.productConditionalMean_ANOVA line 66
6. theorem OAI.Erdos3.productANOVA_selfadjoint line 93
7. theorem OAI.Erdos3.productANOVA_pairing_self line 114
8. theorem OAI.Erdos3.productANOVA_idempotent line 161
9. theorem OAI.Erdos3.productANOVA_mul_blocks line 190
10. theorem OAI.Erdos3.productANOVA_orthogonal_of_not_subset line 233
11. theorem OAI.Erdos3.productANOVA_orthogonal line 239
12. def OAI.Erdos3.productANOVATruncation line 247
13. def OAI.Erdos3.productANOVAEnergy line 250
14. theorem OAI.Erdos3.productANOVAEnergy_nonneg line 253
15. theorem OAI.Erdos3.productANOVAEnergy_pairing line 257
16. theorem OAI.Erdos3.productANOVAEnergy_square line 263
17. theorem OAI.Erdos3.ProductDependsOn.prod line 285
18. theorem OAI.Erdos3.productMean_mul_zero_of_conditionalMean_zero line 295
19. theorem OAI.Erdos3.productANOVA_unique_coordinate_zero line 303
20. theorem OAI.Erdos3.productANOVA_abs_le line 347
21. theorem OAI.Erdos3.productANOVA_weighted_cap line 362
22. theorem OAI.Erdos3.productANOVA_sectionAverage line 389
23. theorem OAI.Erdos3.productANOVA_disjoint_section line 401
24. theorem OAI.Erdos3.productANOVAEnergy_le_mean_sq line 432
25. theorem OAI.Erdos3.productANOVA_reconstruct line 459
26. theorem OAI.Erdos3.productANOVATruncation_of_depends line 463
27. theorem OAI.Erdos3.productANOVA_conditional_commute line 481
28. theorem OAI.Erdos3.productANOVA_of_depends_not_subset line 491
29. theorem OAI.Erdos3.productANOVAEnergy_of_depends_filter line 500
30. theorem OAI.Erdos3.productANOVA_energy_le_lp line 524
31. theorem OAI.Erdos3.productANOVAEnergy_mono line 545
32. theorem OAI.Erdos3.productANOVAEnergy_le_level line 551