OAI/Combinatorics/Progressions/Polynomial/OrdinaryPhasePairFunctionalBounds.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.OrdinaryPolynomialPhase.polynomial_eq_constant line 12
  2. def OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient line 19
  3. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_apply line 24
  4. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_injective line 27
  5. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_eq_zero_iff line 35
  6. theorem OAI.Erdos3.OrdinaryPolynomialPhase.lie_eq_zero line 43
  7. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_lie line 51
  8. def OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficientLie line 59
  9. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficientLie_apply line 66
  10. theorem OAI.Erdos3.OrdinaryPolynomialPhase.mem_top line 71
  11. theorem OAI.Erdos3.OrdinaryPolynomialPhase.top_layer_eq_top line 81
  12. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_centralRationalElement line 86
  13. theorem OAI.Erdos3.OrdinaryPolynomialPhase.eq_constantCoefficient_smul_central line 91
  14. theorem OAI.Erdos3.OrdinaryPolynomialPhase.frequency_eq_constantCoefficient line 97
  15. theorem OAI.Erdos3.OrdinaryPolynomialPhase.projection_filtered line 107
  16. def OAI.Erdos3.OrdinaryPolynomialPhase.gradedProjection line 119
  17. theorem OAI.Erdos3.OrdinaryPolynomialPhase.gradedProjection_image_eq_bot line 127
  18. theorem OAI.Erdos3.OrdinaryPolynomialPhase.gradedProjection_eq_zero line 147
  19. def OAI.Erdos3.OrdinaryPolynomialPhase.projectedScalarFunctional line 173
  20. theorem OAI.Erdos3.OrdinaryPolynomialPhase.projectedScalarFunctional_lie line 177
  21. theorem OAI.Erdos3.OrdinaryPolynomialPhase.controlledFactorization_approximation line 183
  22. theorem OAI.Erdos3.OrdinaryPolynomialPhase.controlledFactorization_approximation_of_normalized_frequency line 229
  23. def OAI.Erdos3.OrdinaryPolynomialPhase.constantBasisIndex line 257
  24. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantBasisIndex_unique line 260
  25. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantBasisIndex_grade line 268
  26. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_eq_basis_coord line 272
  27. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_eq_basis_repr line 276
  28. theorem OAI.Erdos3.OrdinaryPolynomialPhase.realify_constantCoefficient_eq_basis_coord line 281
  29. theorem OAI.Erdos3.OrdinaryPolynomialPhase.realify_constantCoefficient_eq_basis_repr line 293
  30. theorem OAI.Erdos3.OrdinaryPolynomialPhase.constantCoefficient_coordinate_ofCoordinates line 300
  31. def OAI.Erdos3.OrdinaryPolynomialPhase.pairScalarFunctional line 320
  32. theorem OAI.Erdos3.OrdinaryPolynomialPhase.pairScalarFunctional_basis_logHeight line 327