OAI/Combinatorics/Progressions/Probability/RandomCoefficientMassComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.product_image_comparison_of_ae_fiber_bounds line 12
2. theorem OAI.Erdos3.product_image_comparison_of_fiber_bounds line 34
3. theorem OAI.Erdos3.postprocessed_image_comparison_of_ae_fiber_bounds line 44
4. theorem OAI.Erdos3.retained_image_comparison_of_fiber_bounds line 56
5. theorem OAI.Erdos3.coefficientArraySampler_mass_c2_error line 79
6. theorem OAI.Erdos3.coefficient_array_mass_comparison line 130
7. theorem OAI.Erdos3.random_coefficient_array_mass_comparison line 197