OAI/Combinatorics/Progressions/Sampling/AllocatedExternalCandidateNativeFrozenScore.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenScore line 77
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientCandidate_score_eq_frozen line 84
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenScore_ge_of_error line 104
4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientScoredProblem line 136
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredScoredAssembly_mark_on_slice line 168
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_refilteredQuotientScored line 193
7. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredLocalCoordinates line 331
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredLocalCoordinates_value line 340
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenObservable_error_of_native_freezing line 398
10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozen_mark_on_slice line 439
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenScore_ge_of_native_freezing line 473