OAI/Combinatorics/Progressions/Sampling/AllocatedSlicedGridGeometryBudget.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.allocatedPrincipalSides_inactive line 26
  2. def OAI.Erdos3.VectorPolynomial.allocatedSlicedGridHeightCutoff line 34
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedGrid_cases line 37
  4. theorem OAI.Erdos3.exists_denseSliceThreshold line 91
  5. theorem OAI.Erdos3.principalProfileSize_exp_bounds line 106
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedGridHeightCutoff_exp_bound line 130
  7. theorem OAI.Erdos3.exists_slicedGridParameters line 165
  8. theorem OAI.Erdos3.exists_uniform_slicedGridParameters line 223
  9. theorem OAI.Erdos3.exists_canonicalSlicedGridParameters line 258
  10. theorem OAI.Erdos3.exists_detectedCanonicalGridParameters line 296
  11. theorem OAI.Erdos3.detectedSlice_support_density line 345
  12. theorem OAI.Erdos3.blockTorusFactor_exp_bound line 361
  13. theorem OAI.Erdos3.div_density_pow_exp_bound line 382
  14. theorem OAI.Erdos3.slicedGrid_fourier_geometry_exp_bounds line 392
  15. theorem OAI.Erdos3.slicedGrid_support_exp_bound line 420
  16. def OAI.Erdos3.VectorPolynomial.slicedGridGeometryLog line 450
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedSlicedGrid_geometry_bounds line 465