OAI/Combinatorics/Progressions/Dynamics/CompatibleReducedFastReset.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.reducedResetParameter line 11
2. theorem OAI.Erdos3.reducedResetParameter_nonneg line 14
3. theorem OAI.Erdos3.le_reducedResetParameter line 19
4. theorem OAI.Erdos3.reducedResetParameter_controls line 26
5. theorem OAI.Erdos3.exists_reduced_reset_budget line 44
6. def OAI.Erdos3.NilpotentLieFiltration.ControlledReducedFastResetSpec line 72
7. def OAI.Erdos3.NilpotentLieFiltration.ReducedFastResetSpec line 124
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_reduced_fast_reset line 183
9. theorem OAI.Erdos3.NilpotentLieFiltration.exists_reduced_fast_reset line 255
10. def OAI.Erdos3.NilpotentLieFiltration.CompatibleReducedFastResetSpec line 305
11. theorem OAI.Erdos3.NilpotentLieFiltration.exists_compatible_reduced_fast_reset line 350