OAI/Combinatorics/Progressions/Estimates/BaselineNoIncrementTree.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.exists_baseline_marginal_stability line 16
2. theorem OAI.Erdos3.exists_baseline_stable_slice_costs line 61
3. theorem OAI.Erdos3.exists_baseline_comparison_tree line 139
4. theorem OAI.Erdos3.exists_baseline_no_increment_tree line 188