OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/GridMinLower.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.OrdinarySmoothRough.grid_min_lower line 28
2. lemma OAI.OrdinarySmoothRough.grid_boundary_bound line 35
3. lemma OAI.OrdinarySmoothRough.large_smooth_above line 64
4. theorem OAI.OrdinarySmoothRough.grid_remainder_density line 78
5. lemma OAI.OrdinarySmoothRough.reciprocal_loss_mono line 96
6. theorem OAI.OrdinarySmoothRough.uniform_sparse_grid_cofactor line 101