Is it possible to derive this formalpower series and avoid

Stream: lean4

[SHAO YU]

import Mathlib

open Nat
open Real
open Finset
open Finsupp
open BigOperators
open PowerSeries
open MeasureTheory


variable {R : Type*}
open Nat
open Real

--variable (n : ℕ )
variable (x : ℝ )


noncomputable def  c ( n:ℕ): ℝ :=  ((2*n).choose n  )
noncomputable def f := PowerSeries.mk c
noncomputable def fsum : PowerSeries ℝ := f



lemma Step9 (x:ℝ  ):  ∫ a in (0:ℝ)..x , (∑' (n:ℕ ),((2*n).choose n  :ℝ ) *a^n) = ∑' (n:ℕ ),((2*n).choose n  :ℝ ) *(1/(n+1)) *x^(n+1):=by

Is it possible to derive this formal powerseries and avoid the summable?

[Ruben Van de Velde]

Please make sure your code is a #mwe including imports

[SHAO YU]

Ruben Van de Velde said:

Please make sure your code is a #mwe including imports

sorry ,I forgot it. Then I have updated it and add some my tries,thanks!

[Kevin Buzzard]

I doubt this result is true as stated. The series won't converge for a random value of x so the integral will become meaningless and lean will assign it a junk value. Do you really want to mix power series (a concept from algebra) and integrals (a concept from analysis)? What are you actually trying to do? Perhaps a concrete question would be "do you care about x=37 or is x supposed to be a formal variable"?

[Damiano Testa]

Some of my students tried using docs#PowerSeries to represent analytic functions. I wonder if it would be useful to write some comment in the doc-string of PowerSeries that refers to the more analytically oriented part of the library.

[Yakov Pechersky]

To the analytical end, we have docs#FormalMultilinearSeries. But I am not aware of any API glue between PowerSeries and these, not documentation explaining how to interconvert.

[Damiano Testa]

I agree and I think that the missing glue is precisely the reason for adding something in the doc-string to say: "If you want to work with analytic/convergent power series, steer away from PowerSeries and look at FormalMultilinearSeries instead".

[SHAO YU]

Thanks,I konw.I just want to tran the math processes in the paper by lean,but I failed,I cant find the tactics of
"integral" or "deriv' to deal with "tsum".Thanks!
c98ff69e1968640f0814d5e83334590.jpg