OAI/Combinatorics/Progressions/Probability/MixedCoveredDensityMass.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.VectorPolynomial.coveredJetArray_density_lawline 29 - def
OAI.Erdos3.VectorPolynomial.mixedCoveredJetRawReferenceline 80 - theorem
OAI.Erdos3.VectorPolynomial.mixedCoveredJet_density_lawline 91 - theorem
OAI.Erdos3.VectorPolynomial.mixedCoveredJet_normalized_density_lawline 111 - theorem
OAI.Erdos3.VectorPolynomial.mixedCoveredJet_normalized_lintegralline 126