OAI/Combinatorics/Progressions/Probability/WeightedSupportedComplexMixture.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberComplexMean_zero line 13
2. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberComplexMean_condition_error line 27
3. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_error line 43
4. theorem OAI.Erdos3.FiniteProbabilityWeights.condition_complexMean_fiber_mul line 59
5. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_mul_error line 70
6. theorem OAI.Erdos3.FiniteProbabilityWeights.toPMF_bind_scaled_complexMean line 84
7. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_variable_error line 106
8. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_supported_fiber_weighted_error line 118