OAI/Combinatorics/Progressions/Estimates/FiniteFiberVolumeBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.integral_indicator_fiber line 15
2. theorem OAI.Erdos3.product_measureReal_eq_integral_fiber line 25
3. theorem OAI.Erdos3.product_probability_le_bad_set_add line 36
4. theorem OAI.Erdos3.product_measureReal_eq_integral_fiber_of_finite line 78
5. theorem OAI.Erdos3.product_measureReal_le_of_fiber_bound line 92