OAI/Combinatorics/Progressions/Probability/RawWeightCellMixture.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.FiniteProbabilityWeights.embedded_cell_mixtureline 11 - theorem
OAI.Erdos3.FiniteProbabilityWeights.embedded_cell_mixture_errorline 32 - theorem
OAI.Erdos3.FiniteProbabilityWeights.ofPositiveWeights_lowWeightFibers_massline 58 - theorem
OAI.Erdos3.FiniteProbabilityWeights.embedded_lowWeight_cell_mixture_errorline 68