OAI/Combinatorics/Progressions/Sampling/JointSamplerProductivity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.FiniteProbabilityWeights.productive_mass_lower_bound line 15
2. theorem OAI.Erdos3.exists_productive_sampler_center line 40
3. theorem OAI.Erdos3.exists_productive_injective_center line 73
4. theorem OAI.Erdos3.exists_productive_injective_center_of_complex_marginals line 115
5. theorem OAI.Erdos3.integral_productive_sampler_mass line 153
6. theorem OAI.Erdos3.integral_productive_injective_mass line 178
7. theorem OAI.Erdos3.integral_productive_injective_mass_of_complex_marginals line 235