OAI/Combinatorics/Progressions/Sampling/AllocatedSupportedSlicedGridMarginal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalJointPMF line 37
2. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalGrid_joint_law line 50
3. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalGrid_joint_mass line 90
4. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalGrid_joint_scaled_mass line 98
5. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedJointGrid_site_approximation line 143
6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridJetPMF_restrict_join line 218
7. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalJointPMF_grid_marginal line 237
8. theorem OAI.Erdos3.VectorPolynomial.allocatedSupportedSlicedPhysicalJointPMF_grid_mean line 266