OAI/Combinatorics/Progressions/Estimates/GlobalMarkedOuterNormalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.nonempty_globalMarkedNativeFactors line 39
3. theorem OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors.middle_values line 51
4. theorem OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors.middle_coefficients_mem_first line 59
5. theorem OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors.chart_coefficients_mem_first line 69
6. theorem OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors.product_values line 79
7. theorem OAI.Erdos3.NilpotentLieFiltration.exists_globalMarkedNativeFactors_of_outer_lifts line 107
8. theorem OAI.Erdos3.NilpotentLieFiltration.exists_controlled_globalMarkedNativeFactors line 137