OAI/Combinatorics/Progressions/Estimates/InheritedTaggedQuotientPrecenterMasks.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.topQuotient line 46
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.topQuotient_orbit line 70
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.topQuotient_value line 74
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.topQuotient_score line 84
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.topQuotient_score_eq line 97
6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.topQuotientProblem line 164
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.topQuotientProblem_ambientScore line 181
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_topQuotient line 189
9. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenObservable line 288
10. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientObservable line 296
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientCandidate_score line 324
12. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientProblem line 344
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredAssembly_mark_on_slice line 365
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_refilteredQuotient line 389
15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredFrozenObservable_recovery_of_coveredDiagram line 517
16. def OAI.Erdos3.VectorPolynomial.taggedRefilteredQuotientOperator line 621
17. theorem OAI.Erdos3.VectorPolynomial.taggedRefilteredQuotientOperator_nonexpansive line 631
18. theorem OAI.Erdos3.VectorPolynomial.taggedRefilteredQuotientOperator_approx_on line 642
19. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientObservable_eq_taggedOperator line 705
20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.refilteredQuotientObservable_approx_on line 717
21. def OAI.Erdos3.VectorPolynomial.inheritedTaggedQuotientFamily line 772
22. def OAI.Erdos3.VectorPolynomial.inheritedTaggedQuotientCenters line 776
23. theorem OAI.Erdos3.VectorPolynomial.inheritedTaggedQuotient_original_index_approx line 780
24. theorem OAI.Erdos3.VectorPolynomial.inheritedTaggedQuotient_approx_on_original_bin line 791
25. theorem OAI.Erdos3.VectorPolynomial.inheritedTaggedQuotient_selected_score_lower line 803