OAI/Combinatorics/Progressions/Estimates/NormalizedCommonFamily.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.CoefficientCorrectionSpec line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_coefficient_correction_bound line 40
3. def OAI.Erdos3.NativeNormalizedSquareSpec line 92
4. theorem OAI.Erdos3.exists_native_normalized_square line 117
5. theorem OAI.Erdos3.exists_synchronizedSquare_budget line 151
6. def OAI.Erdos3.NilpotentLieFiltration.SynchronizedSquareBoundSpec line 167
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_synchronizedSquare_bound line 200
8. theorem OAI.Erdos3.NilpotentLieFiltration.synchronized_normalized_coefficient_common_derivative line 246
9. def OAI.Erdos3.NilpotentLieFiltration.NormalizedCommonFamilySpec line 301
10. theorem OAI.Erdos3.NilpotentLieFiltration.exists_normalized_common_family line 349