OAI/Combinatorics/Progressions/Probability/AllocatedWindowProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.finset_indicator_eq_card_mul_uniform line 13
2. def OAI.Erdos3.VectorPolynomial.allocatedGridWindowPMF line 41
3. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowFactor_eq_probability line 50
4. theorem OAI.Erdos3.VectorPolynomial.allocatedGridWindowWeight_eq_probability line 65