OAI/Combinatorics/Progressions/Geometry/DetectedTranslationLogCoordinates.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate line 18
  2. theorem OAI.Erdos3.NilpotentLieFiltration.coeff_realSymbolCoordinate line 23
  3. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_coeff_of_ne line 31
  4. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_coeff_symbol line 37
  5. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_isWeightedHomogeneous line 44
  6. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_coeff_zero line 51
  7. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_constantCoeff line 56
  8. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_slow_coefficients line 60
  9. theorem OAI.Erdos3.NilpotentLieFiltration.realSymbolCoordinate_rational_coefficients line 69
  10. def OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate line 90
  11. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate_coeff line 97
  12. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate_eval line 105
  13. def OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial line 122
  14. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_specialize line 128
  15. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_orbit line 136
  16. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_native line 145
  17. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate_degree line 158
  18. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate_constant line 172
  19. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_realified line 179
  20. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationLogCoordinate_symbol line 193
  21. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_symbol line 204
  22. theorem OAI.Erdos3.PolynomialTranslationLie.translationPolynomial_ext_eval line 221
  23. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_mul line 238
  24. theorem OAI.Erdos3.PolynomialTranslationLie.nativeTranslationGroupPolynomial_factorization line 251
  25. theorem OAI.Erdos3.realifyFunctional_basis_coord line 274
  26. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_eq_sum_realSymbolCoordinates line 289
  27. theorem OAI.Erdos3.NilpotentLieFiltration.scalarSymbolPolynomial_joint_grid line 313
  28. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinatePolynomial line 354
  29. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_eq_canonical line 360
  30. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_homogeneous line 370
  31. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_constant line 380
  32. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogFunctional line 389
  33. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_eq_scalar line 402
  34. def OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogProjectionMatrix line 422
  35. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogFunctional_basis line 425
  36. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_eq_sum line 436
  37. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_slow_coefficients line 447
  38. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_joint_grid line 462
  39. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_rational_coefficients line 475
  40. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_exists_coefficient_grid line 488
  41. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogCoordinate_common_coefficient_grid line 503
  42. theorem OAI.Erdos3.PolynomialTranslationLie.exists_detectedTranslationLogCoordinate_common_grid line 516
  43. theorem OAI.Erdos3.PolynomialTranslationLie.detectedTranslationLogProjectionMatrix_height line 534