OAI/Combinatorics/SumProduct/Alignment/PolynomialDephasing01.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialDephasing.norm_phase_sub_one_le line 17
  2. theorem OAI.PolynomialDephasing.norm_phase_sub_le line 26
  3. theorem OAI.PolynomialDephasing.monomial_phase_variation line 35
  4. theorem OAI.PolynomialDephasing.weighted_mean_large_prefix line 62
  5. def OAI.PolynomialDephasing.fourierCoefficient line 121
  6. theorem OAI.PolynomialDephasing.norm_fourierCoefficient_le_one line 124
  7. theorem OAI.PolynomialDephasing.fourier_expansion line 137
  8. theorem OAI.PolynomialDephasing.stdAddChar_int_phase line 147
  9. theorem OAI.PolynomialDephasing.stdAddChar_mul_nat_phase line 154
  10. theorem OAI.PolynomialDephasing.rational_monomial_phase line 162
  11. theorem OAI.PolynomialDephasing.periodic_weight_large_frequency line 174
  12. theorem OAI.PolynomialDephasing.remove_rational_monomial line 209
  13. def OAI.WeylCoefficients.lowerWithFrequency line 262
  14. theorem OAI.WeylCoefficients.lowerWithFrequency_degree line 265
  15. theorem OAI.WeylCoefficients.lowerWithFrequency_coeff line 277
  16. theorem OAI.WeylCoefficients.remove_leading_coefficient line 285
  17. theorem OAI.WeylCoefficients.prefix_error_transfer line 329
  18. def OAI.WeylCoefficients.CoefficientInverse line 346
  19. theorem OAI.WeylCoefficients.coefficient_inverse_zero line 354
  20. theorem OAI.WeylCoefficients.coefficient_inverse_one line 360
  21. theorem OAI.WeylCoefficients.coefficient_inverse_succ line 374
  22. theorem OAI.WeylCoefficients.coefficient_inverse line 460