OAI/Combinatorics/Progressions/Sampling/AllocatedWeightedGridMixture.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.allocatedLayerInteger_moderate_jet_blocks line 23
2. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridJet_blocks line 66
3. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridJetPMF_blocks line 115
4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalGridJetPMF_principal line 167
5. def OAI.Erdos3.VectorPolynomial.allocatedFrozenPrincipalJet line 218
6. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenGrid_marked_principal_mixture line 225
7. theorem OAI.Erdos3.VectorPolynomial.allocatedFrozenGrid_separated_principal_mixture line 251
8. theorem OAI.Erdos3.VectorPolynomial.allocatedGrid_marked_principal_mixture_of_law line 300
9. theorem OAI.Erdos3.VectorPolynomial.allocatedGrid_separated_principal_mixture_of_law line 329