OAI/Combinatorics/Progressions/Sampling/ActualMarkedFiniteScoreComparison.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Erdos3.RationalFilteredNilmanifold.MarkedFiniteScoreFreezing line 19
2. theorem OAI.Erdos3.RationalFilteredNilmanifold.BoundedCellMarkedPolynomialFreezing.exists_finite_score_freezing line 51
3. def OAI.Erdos3.RationalFilteredNilmanifold.MarkedFiniteScoreFreezing.value line 88
4. theorem OAI.Erdos3.RationalFilteredNilmanifold.MarkedFiniteScoreFreezing.norm_score_sub_le line 94
5. theorem OAI.Erdos3.RationalFilteredNilmanifold.MarkedFiniteScoreFreezing.exists_external_restored_scores line 117
6. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_external_marked_frozen_restored_scores line 162