OAI/Combinatorics/Progressions/Estimates/WeightedTranslationShearExponential.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.scalarDirectionalDerivative_direction_add line 15
  2. theorem OAI.Erdos3.scalarDirectionalDerivative_direction_smul line 20
  3. theorem OAI.Erdos3.scalarDirectionalDerivative_direction_zero line 25
  4. theorem OAI.Erdos3.scalarDirectionalDerivative_commute line 29
  5. structure OAI.Erdos3.PolynomialTranslationLie line 40
  6. def OAI.Erdos3.PolynomialTranslationLie.toProd line 46
  7. instance OAI.Erdos3.PolynomialTranslationLie.(instance at line 52) line 52
  8. instance OAI.Erdos3.PolynomialTranslationLie.(instance at line 53) line 53
  9. def OAI.Erdos3.PolynomialTranslationLie.toProdl line 56
  10. theorem OAI.Erdos3.PolynomialTranslationLie.base_zero line 60
  11. theorem OAI.Erdos3.PolynomialTranslationLie.polynomial_zero line 62
  12. theorem OAI.Erdos3.PolynomialTranslationLie.base_add line 64
  13. theorem OAI.Erdos3.PolynomialTranslationLie.polynomial_add line 66
  14. theorem OAI.Erdos3.PolynomialTranslationLie.base_smul line 68
  15. theorem OAI.Erdos3.PolynomialTranslationLie.polynomial_smul line 70
  16. instance OAI.Erdos3.PolynomialTranslationLie.(instance at line 72) line 72
  17. theorem OAI.Erdos3.PolynomialTranslationLie.base_lie line 76
  18. theorem OAI.Erdos3.PolynomialTranslationLie.polynomial_lie line 77
  19. instance OAI.Erdos3.PolynomialTranslationLie.(instance at line 80) line 80
  20. instance OAI.Erdos3.PolynomialTranslationLie.(instance at line 96) line 96
  21. theorem OAI.Erdos3.scalarDirectionalDerivative_weight_drop line 113
  22. def OAI.Erdos3.PolynomialTranslationLie.weightedLayer line 127
  23. theorem OAI.Erdos3.PolynomialTranslationLie.mem_weightedLayer line 140
  24. theorem OAI.Erdos3.PolynomialTranslationLie.weightedLayer_antitone line 145
  25. theorem OAI.Erdos3.PolynomialTranslationLie.weightedLayer_lie_mem line 149
  26. theorem OAI.Erdos3.PolynomialTranslationLie.weightedLayer_terminal line 160
  27. def OAI.Erdos3.PolynomialTranslationLie.weightedSubalgebra line 170
  28. theorem OAI.Erdos3.PolynomialTranslationLie.mem_weightedSubalgebra line 175
  29. def OAI.Erdos3.PolynomialTranslationLie.weightedFiltration line 178
  30. def OAI.Erdos3.PolynomialTranslationLie.weightedCoordinates line 191
  31. theorem OAI.Erdos3.PolynomialTranslationLie.weightedCoordinates_injective line 197
  32. theorem OAI.Erdos3.PolynomialTranslationLie.weightedSubalgebra_finite line 205
  33. theorem OAI.Erdos3.PolynomialTranslationLie.weightedSubalgebra_finrank_le line 210
  34. theorem OAI.Erdos3.PolynomialTranslationLie.weightedSubalgebra_nilpotent line 223
  35. def OAI.Erdos3.PolynomialTranslationLie.shearWeight line 240
  36. def OAI.Erdos3.PolynomialTranslationLie.shearDerivation line 242
  37. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_X_inl line 247
  38. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_X_inr line 251
  39. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_rename line 254
  40. def OAI.Erdos3.PolynomialTranslationLie.shearDerivationHom line 264
  41. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivationHom_injective line 282
  42. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_mem_drop line 296
  43. def OAI.Erdos3.PolynomialTranslationLie.weightedShearEmbedding line 311
  44. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearEmbedding_injective line 320
  45. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearEmbedding_filtered line 326
  46. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearEmbedding_apply_drop line 332
  47. theorem OAI.Erdos3.PolynomialTranslationLie.shearWeight_le line 353
  48. def OAI.Erdos3.PolynomialTranslationLie.weightedShearGroupHom line 360
  49. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearGroupHom_apply line 365
  50. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearGroupHom_injective line 369
  51. def OAI.Erdos3.PolynomialTranslationLie.weightedShearRealGroupHom line 377
  52. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearRealGroupHom_apply line 384
  53. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearRealEmbedding_injective line 390
  54. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearRealGroupHom_injective line 396
  55. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearRealGroupHom_rational line 404
  56. def OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding line 426
  57. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_tmul line 431
  58. theorem OAI.Erdos3.PolynomialTranslationLie.realShearEmbedding_shape line 436
  59. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_pow_X_inr line 490
  60. theorem OAI.Erdos3.PolynomialTranslationLie.shearDerivation_pow_X_inl line 502
  61. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearExp_X_inr line 511
  62. theorem OAI.Erdos3.PolynomialTranslationLie.weightedShearExp_X_inl line 529