OAI/Combinatorics/Progressions/Estimates/TerminalControlledFactorization.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.NilpotentLieFiltration.exists_full_fast_quotient_bases line 24
2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_uniform_formal_induction_factorization line 94
3. theorem OAI.Erdos3.NilpotentLieFiltration.exists_formal_stepDrop_subalgebra_factorization line 169
4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_stepDrop_from_formal_state line 262
5. def OAI.Erdos3.NilpotentLieFiltration.FastTerminalFactorization line 396
6. theorem OAI.Erdos3.NilpotentLieFiltration.FastTerminalFactorization.mono line 413
7. def OAI.Erdos3.NilpotentLieFiltration.FastTerminalStateSpec line 425
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_fast_terminalState_bound line 444
9. def OAI.Erdos3.NilpotentLieFiltration.SymbolTerminalFactorization line 525
10. theorem OAI.Erdos3.NilpotentLieFiltration.symbolTerminalFactorization_of_graded line 541
11. theorem OAI.Erdos3.NilpotentLieFiltration.symbolTerminalFactorization_of_native line 578
12. theorem OAI.Erdos3.NilpotentLieFiltration.SymbolTerminalFactorization.mono line 599
13. theorem OAI.Erdos3.NilpotentLieFiltration.native_symbol_slow line 618
14. theorem OAI.Erdos3.NilpotentLieFiltration.native_symbol_grid line 625
15. theorem OAI.Erdos3.NilpotentLieFiltration.SymbolTerminalFactorization.controlled line 642