OAI/Combinatorics/Progressions/FixedDensity/HypergraphBundleRelativeCounting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleProduct_pullback_eq_of_subset_of_projection_eq line 17
2. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_pullback_eq_of_subset_of_projection_eq line 31
3. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.eraseEdge_bundleCount_pullback line 45
4. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_lowerOrder_closed line 58
5. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.duplicateOutside_lowerOrder_order_lt line 85
6. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.card_duplicateOutside_lowerOrder_le line 96
7. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.exists_edge_card_eq_order line 116
8. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.count_le_one_add_error_mul_main line 135
9. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pow_card_edges_le_bundleMainProduct_of_edges line 149
10. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.pow_card_edges_le_selected_mul_maximalRemainder line 172
11. theorem OAI.Erdos3.FixedDensity.HypergraphBundle.bundleCount_eq_bundleMainProduct_of_order_zero line 225
12. def OAI.Erdos3.FixedDensity.HasTaoBundleCountingStep line 284
13. theorem OAI.Erdos3.FixedDensity.abs_bundleCount_pullback_sub_bundleMainProduct_le_envelope line 308