OAI/Combinatorics/Progressions/Estimates/TranslationMajorCorrelationDecomposition.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.realPolynomialMass_weightedHomogeneousComponent_le line 14
  2. theorem OAI.Erdos3.realPolynomialMass_specializeMajorParameters_zero_le line 29
  3. theorem OAI.Erdos3.reducedMajorZeroSlice_mass_le line 41
  4. theorem OAI.Erdos3.positiveWeightedSupport_totalDegree_le line 56
  5. theorem OAI.Erdos3.specializeMajorParameters_zero_totalDegree_le line 65
  6. theorem OAI.Erdos3.reducedMajorZeroSlice_totalDegree_le line 74
  7. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationNormalizedBase line 101
  8. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationNormalizedPhase line 106
  9. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationNormalizedBase_eval line 112
  10. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationNormalizedPhase_eval line 123
  11. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval_normalized_left line 138
  12. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslation_rational_right line 154
  13. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslation_normalized_decomposition line 203
  14. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslation_normalized_weighted_decomposition line 297
  15. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_decomposition line 434