OAI/Combinatorics/Progressions/Estimates/FiniteFiberTsum.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_eq_zero_of_not_mem_image line 13
2. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_support_subset_image line 20
3. theorem OAI.Erdos3.FiniteProbabilityWeights.fiberMean_hasFiniteSupport line 26
4. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_fiber_factor_sum_image line 30
5. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_fiber_factor_summable line 43
6. theorem OAI.Erdos3.FiniteProbabilityWeights.complexMean_fiber_factor_tsum line 49