OAI/Combinatorics/Progressions/Estimates/PreparedScalarStructuralBasePower.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.normalizedSiteCutoffBound line 14
  2. theorem OAI.Erdos3.normalizedSiteCutoffBound_one_le line 17
  3. theorem OAI.Erdos3.exists_normalized_site_cutoff line 20
  4. theorem OAI.Erdos3.exists_normalized_active_ideal_site_approximation line 60
  5. theorem OAI.Erdos3.exists_normalized_active_sliced_ideal_site_approximation line 123
  6. def OAI.Erdos3.idealSiteBuffer line 188
  7. theorem OAI.Erdos3.idealSiteBuffer_spec line 194
  8. theorem OAI.Erdos3.idealSiteBuffer_volume_le_exp line 208
  9. theorem OAI.Erdos3.idealSiteEnvelopeRadius_one_le line 236
  10. theorem OAI.Erdos3.idealSiteBuffer_lip_le_exp line 250
  11. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarStructuralBasePower line 276