OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateGeneratedFreezingSuccessor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.NilpotentLieFiltration.frozenMarkedPhysicalExponent line 14
2. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedPhysicalExponent_ge_two line 18
3. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedPhysical_exp_mono line 24
4. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedPhysical_left_bound line 35
5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_frozenMarkedPhysical_right_grid line 61
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.frozenMarkedPhysical_bounds line 130
7. def OAI.Erdos3.RationalFilteredNilmanifold.allocatedRightDictionaryExponent line 189
8. def OAI.Erdos3.RationalFilteredNilmanifold.allocatedCoveredLowerExponent line 192
9. theorem OAI.Erdos3.RationalFilteredNilmanifold.allocatedCoveredLowerExponent_ge_two line 195
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_generatedCovered_nativeReset_degreeRule line 268
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_generatedPhysical_nativeReset_degreeRule line 449
12. def OAI.Erdos3.RationalFilteredNilmanifold.allocatedGeneratedRightDictionary line 577
13. def OAI.Erdos3.RationalFilteredNilmanifold.allocatedGeneratedCoveredLowerDiagram line 590
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_generatedFreezing_nativeReset_degreeRule line 701