OAI/Combinatorics/Progressions/Fourier/QuadraticLocalFrequency.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.affineBasisCoefficient line 15
  2. def OAI.Erdos3.affineBasisConstant line 19
  3. theorem OAI.Erdos3.affine_basis_coordinate_sum line 23
  4. theorem OAI.Erdos3.affine_basis_change line 32
  5. theorem OAI.Erdos3.affineBasisCoefficient_mem line 41
  6. theorem OAI.Erdos3.affineBasisConstant_mem line 47
  7. theorem OAI.Erdos3.positiveUnivariate_affine_basis_change line 54
  8. theorem OAI.Erdos3.exists_local_affine_scalar_chart line 75
  9. theorem OAI.Erdos3.exists_quadratic_local_frequency line 108