OAI/Combinatorics/Progressions/Geometry/CertifiedFullChartRecoveredTerminal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample_floor_coeff_sum line 20
2. theorem OAI.Erdos3.VectorPolynomial.canonicalCoefficientSample_floor_coeff_separate line 36
3. theorem OAI.Erdos3.monomialScale_mapDomain_embedding line 54
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_long_coeff line 77
5. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_tag_degree line 132
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_frozen_top_range line 141
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_certified_frozen_top_range line 197
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFrozenFullChart_certified_top_range line 280
9. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.allocatedRecovered_terminal_mem_fast_of_certificate line 342
10. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.allocatedRecovered_terminal_mem_symbolPointwiseSubalgebra_of_certificate line 391
11. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.StageBounds.allocatedRecovered_terminal_mem_symbolPointwiseSubalgebra line 441