OAI/Combinatorics/Progressions/Linear/ProductANOVALpBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.productANOVATensor_energy line 18
2. theorem OAI.Erdos3.productANOVATensor_l2 line 44
3. theorem OAI.Erdos3.productANOVATensor_unfixed_section line 51
4. theorem OAI.Erdos3.productANOVATensor_section_bound line 72
5. theorem OAI.Erdos3.productANOVATensor_uniform_sections line 125
6. theorem OAI.Erdos3.productANOVATensor_hypergraph_bound line 158
7. theorem OAI.Erdos3.productANOVATensor_abs_hypergraph_bound line 179
8. theorem OAI.Erdos3.productANOVATensor_grouped_bound line 213
9. theorem OAI.Erdos3.productANOVA_moment_bound line 262
10. theorem OAI.Erdos3.productANOVA_lp_bound line 294