OAI/Combinatorics/Progressions/Sampling/AllocatedExternalCandidateSamplerFamily.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateSides line 19
2. def OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateRootBudget line 22
3. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateRootBudget_eq line 25
4. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateRootBudget_nonneg line 31
5. def OAI.Erdos3.VectorPolynomial.allocatedExternalCandidateWidths line 35
6. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler line 49
7. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.sides line 66
8. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.widths line 70
9. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.bases line 74
10. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.Path line 78
11. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.Site line 83
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.widths_pos line 88
13. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.law line 94
14. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.physical line 101
15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.physical_eq line 105
16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.law_support line 108
17. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily line 143
18. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.Path line 152
19. abbrev OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.Site line 154
20. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.physical line 156
21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.physical_eq_center line 159
22. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.law line 166
23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.law_eq_center line 170
24. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.weight_measurable line 177
25. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.averagedLaw line 184
26. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.averagedLaw_weight line 189
27. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSamplerFamily.averagedLaw_mean line 194