OAI/Combinatorics/Progressions/Estimates/TranslationMajorCorrelationIdentity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolProjection line 25
  2. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolProjection_coord line 34
  3. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift line 41
  4. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_apply line 47
  5. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_log line 55
  6. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_mul line 66
  7. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolProjection_pairOrbitSymbol line 76
  8. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_pairOrbitSymbol line 87
  9. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_value_mem_fast line 95
  10. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_coefficients_mem_fast line 114
  11. theorem OAI.Erdos3.NilpotentLieFiltration.realGradedSymbolPolynomial_constant line 146
  12. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_constant line 156
  13. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_constant line 176
  14. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseFunctional_basis_eq_zero_of_ne line 183
  15. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBaseScalar_isHomogeneous line 190
  16. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coordinate_isHomogeneous line 200
  17. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coefficients_apply_of_degree_ne line 208
  18. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coordinate_totalDegree_le line 215
  19. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationBasePolynomial_coordinate_homogeneousComponent line 222
  20. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval line 248
  21. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval_major_factorization line 258
  22. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationSymbolLift_base_coordinate line 303
  23. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval_base line 326
  24. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval_fast_potential line 361
  25. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationGroupEval_major_identity line 387
  26. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslation_separated_base line 445
  27. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_separated_data line 556
  28. theorem OAI.Erdos3.PolynomialTranslationLie.exists_reduced_majorPolynomial_degree_twisted_correlation_identity line 748