PowerSeriesComposition.lean

theorem alternating_mul_one_add_X
    (A : Type*) [CommRing A] :
    (PowerSeries.mk fun n : ℕ => (-1 : A) ^ n) *
        (1 + PowerSeries.X : PowerSeries A) = 1 := by
  have h :=
    congrArg (PowerSeries.evalNegHom (A := A))
      (PowerSeries.mk_one_mul_one_sub_eq_one A)
  have hmk' :
      PowerSeries.evalNegHom (PowerSeries.mk (1 : ℕ → A)) =
        PowerSeries.mk fun n : ℕ => (-1 : A) ^ n := by
    ext n
    simp [PowerSeries.evalNegHom, PowerSeries.rescale_mk]
  simpa [hmk', sub_eq_add_neg] using h

theorem eq_zero_of_derivative_mul_one_add_X_eq_self
    (A : Type*) [CommRing A] [IsAddTorsionFree A] {f : PowerSeries A}
    (hD :
      PowerSeries.derivative f * (1 + PowerSeries.X : PowerSeries A) = f)
    (hc : PowerSeries.constantCoeff f = 0) :
    f = 0

theorem eq_one_add_X_of_derivative_mul_one_add_X_eq_self
    (A : Type*) [CommRing A] [IsAddTorsionFree A] {f : PowerSeries A}
    (hD :
      PowerSeries.derivative f * (1 + PowerSeries.X : PowerSeries A) = f)
    (hc : PowerSeries.constantCoeff f = 1) :
    f = 1 + PowerSeries.X

theorem eq_X_of_derivative_eq_one
    (A : Type*) [CommRing A] [IsAddTorsionFree A] {f : PowerSeries A}
    (hD : PowerSeries.derivative f = 1)
    (hc : PowerSeries.constantCoeff f = 0) :
    f = PowerSeries.X

theorem exp_subst_log_eq_one_add_X
    (A : Type*) [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] :
    PowerSeries.subst (PowerSeries.log A) (PowerSeries.exp A) =
      (1 + PowerSeries.X : PowerSeries A)

theorem log_subst_exp_sub_one_eq_X
    (A : Type*) [CommRing A] [Algebra ℚ A] [IsAddTorsionFree A] :
    PowerSeries.subst ((PowerSeries.exp A) - 1) (PowerSeries.log A) =
      (PowerSeries.X : PowerSeries A)