OAI/Combinatorics/Progressions/Estimates/NativeLocalPivotVerticalPartners.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exp_scaled_norm_le_one line 12
2. theorem OAI.Erdos3.finite_double_normalization line 19
3. theorem OAI.Erdos3.finite_remove_normalization line 38
4. theorem OAI.Erdos3.weighted_fixed_choices line 63
5. theorem OAI.Erdos3.exists_weighted_native_vertical_partners line 111
6. theorem OAI.Erdos3.norm_expect_scaled_product line 202
7. theorem OAI.Erdos3.exists_localPivot_weighted_native_vertical_partners line 210