OAI/Combinatorics/Progressions/Polynomial/DetectedTranslationPhaseDegree.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.weightedSupportDrop_pderiv line 15
  2. theorem OAI.Erdos3.translationDirectionalDerivative_mem_weightedSupportDrop line 34
  3. theorem OAI.Erdos3.translationDirectionalDerivative_pow_mem_weightedSupportDrop line 55
  4. theorem OAI.Erdos3.translationDirectionalSeries_mem_weightedSupportDrop line 68
  5. theorem OAI.Erdos3.translationDirectionalDerivative_mem_weightedSupportLE line 80
  6. theorem OAI.Erdos3.translationDirectionalSeries_mem_weightedSupportLE line 89
  7. theorem OAI.Erdos3.translationDirectionalSeries_mem_weightedSupportLT line 98
  8. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_base_abs_le_one line 120
  9. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_polynomial_mass_le_one line 129
  10. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_base_integer line 136
  11. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_base_real_grid line 147
  12. theorem OAI.Erdos3.PolynomialTranslationLie.weightedBasis_polynomial_real_grid line 155
  13. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupPolynomial line 183
  14. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial line 189
  15. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial line 194
  16. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupPolynomial_eq_logGroup line 200
  17. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_eq_logMixed line 206
  18. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupPolynomial_specialize line 212
  19. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_eval line 221
  20. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_eq_logCoordinate line 229
  21. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_eq_scalarSymbol line 245
  22. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_specialize line 258
  23. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_eval line 268
  24. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_coeff line 277
  25. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_normalized_mass line 297
  26. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_coefficientGrid line 312
  27. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_mass_of_slow line 336
  28. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_mass_of_slow line 353
  29. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupPolynomials_grid_of_symbol line 366
  30. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_isWeightedHomogeneous line 399
  31. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_weightedSupportLE line 410
  32. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_totalDegree line 418
  33. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_scaled_totalDegree line 436
  34. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_totalDegree line 444
  35. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseCoordinatePolynomial_scaled_totalDegree line 457
  36. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationPhasePolynomial_scaled_weightedSupportLE line 465