OAI/Combinatorics/Progressions/Estimates/SharedFreeRoundingThreshold.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_native_full_coefficient_corrections line 24
2. theorem OAI.Erdos3.NativeRankRelation.CommonData.native_full_scaled_correction line 67
3. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_uniform_native_full_scaled_corrections line 97
4. def OAI.Erdos3.sharedLogCoefficientTuple line 133
5. theorem OAI.Erdos3.sharedLogCoefficientTuple_mem_common line 142
6. theorem OAI.Erdos3.NativeRankRelation.CommonData.native_shared_scaled_correction line 174
7. theorem OAI.Erdos3.sharedLogCoefficientTuple_annihilator_decomposition line 221
8. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_uniform_shared_refinement line 273
9. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_correlation_refined_basis line 399
10. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_correlation_refined_annihilator line 422
11. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_controlled_shared_free_refinement line 497
12. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_real_correlation_refined_equations line 569
13. def OAI.Erdos3.sharedFreeEquationInputBudget line 620
14. theorem OAI.Erdos3.sharedFreeEquationInputBudget_bounds line 625
15. theorem OAI.Erdos3.NativeRankRelation.CommonData.exists_controlled_shared_free_equations line 672
16. theorem OAI.Erdos3.sharedFree_rounding_small line 773
17. def OAI.Erdos3.sharedFreeRecoveryThreshold line 817
18. theorem OAI.Erdos3.sharedFreeRecoveryThreshold_spec line 821