OAI/Combinatorics/Progressions/Estimates/AntisymmetricPartitionApproximation.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.NativeAntisymmetricOrbitFactors line 16
2. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.middle_values line 78
3. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.middle_top_frequency line 90
4. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.middle_bracket_frequency line 97
5. theorem OAI.Erdos3.exists_antisymmetric_coefficient_control line 122
6. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.eval_factors line 199
7. theorem OAI.Erdos3.NativeAntisymmetricOrbitFactors.top_layer_invariant line 214
8. def OAI.Erdos3.NativeAntisymmetricOrbitFactors.mono line 243
9. theorem OAI.Erdos3.exists_antisymmetric_outer_bounds line 292
10. theorem OAI.Erdos3.exists_antisymmetric_local_control line 383
11. structure OAI.Erdos3.NativeAntisymmetricFrozenDescent line 460
12. def OAI.Erdos3.NativeAntisymmetricFrozenDescent.mono line 511
13. theorem OAI.Erdos3.NativeAntisymmetricFrozenDescent.exists_diagonal_niltest line 523
14. theorem OAI.Erdos3.RationalFilteredNilmanifold.observable_frozen_right_eq line 547
15. structure OAI.Erdos3.NativeAntisymmetricLocalModels line 562
16. theorem OAI.Erdos3.exists_antisymmetric_local_models line 576
17. theorem OAI.Erdos3.NativeAntisymmetricLocalModels.select_partition line 658
18. theorem OAI.Erdos3.exists_antisymmetric_partition_approximation line 745