OAI/Combinatorics/Progressions/Estimates/NativeProductVerticalization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_vertical_correlators line 15
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_unit_vertical_correlators line 134
3. theorem OAI.Erdos3.exists_native_vertical_derivative_models line 236
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_unit_factor_replacement line 306
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_native_two_factor_unit_replacement line 425
6. theorem OAI.Erdos3.exists_native_mixed_of_bounded line 543
7. theorem OAI.Erdos3.NativeUnitRankFamily.withOrbit_observable line 630
8. theorem OAI.Erdos3.exists_native_correlation_of_sliced_unit_products line 635
9. theorem OAI.Erdos3.exists_native_sliced_product_correlation line 676
10. theorem OAI.Erdos3.exists_native_fixed_product_unit_data line 698
11. theorem OAI.Erdos3.exists_native_fixed_product_verticalization line 758
12. def OAI.Erdos3.HasBoundedProductCorrelation line 808
13. theorem OAI.Erdos3.HasBoundedProductCorrelation.mono line 819
14. theorem OAI.Erdos3.NativeRankRelation.CommonData.HasUnitRankInducedCorrelationFamily.combineMixed line 844
15. theorem OAI.Erdos3.exists_native_product_verticalization line 912