OAI/Combinatorics/Progressions/Estimates/AllocatedCenteredNarrowPrescribedMarginal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_narrow_prescribed_marginal line 12
2. theorem OAI.Erdos3.centeredFiniteMarginal_siteLaw_excessMass_le_of_uniform line 122
3. theorem OAI.Erdos3.VectorPolynomial.allocatedCenteredJointFiniteLaw_weight_measurable line 155
4. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_narrow_normalized_approximation line 187
5. def OAI.Erdos3.VectorPolynomial.AllocatedCenteredNarrowPrescribedMarginalStatement line 321
6. def OAI.Erdos3.VectorPolynomial.AllocatedCenteredNarrowPrescribedMarginalPointwiseStatement line 396
7. def OAI.Erdos3.VectorPolynomial.AllocatedCenteredNarrowPrescribedMarginalOneCenterStatement line 471
8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_centered_narrow_prescribed_marginal_oneCenter line 546
9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_centered_narrow_prescribed_marginal_pointwise line 579
10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_centered_narrow_prescribed_marginal line 601