OAI/Probability/BinarySweep/SparseBounds/FewSparseBases.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Sparse.few_eta_good line 10
2. lemma OAI.BinaryCoordinateSweeps.Sparse.few_vertex_base line 32
3. lemma OAI.BinaryCoordinateSweeps.Sparse.few_line_base line 49
4. lemma OAI.BinaryCoordinateSweeps.Sparse.adaptive_count_small line 67
5. lemma OAI.BinaryCoordinateSweeps.grid_log_upper line 96
6. lemma OAI.BinaryCoordinateSweeps.few_axis_eta_large line 108
7. lemma OAI.BinaryCoordinateSweeps.outside_card_add_one_le line 127
8. lemma OAI.BinaryCoordinateSweeps.few_cutoff_bounds line 135