OAI/Combinatorics/Progressions/Linear/ProductANOVAWeightedLp.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.productANOVA_moment_comparison line 16
2. theorem OAI.Erdos3.productANOVA_moment_bound_of_sections line 74
3. theorem OAI.Erdos3.productANOVA_lp_bound_of_sections line 92
4. theorem OAI.Erdos3.productANOVA_weighted_lp_of_sections line 117