Taylor's theorem

Stream: maths

[Johan Commelin]

How far are we from https://en.wikipedia.org/wiki/Taylor%27s_theorem#Statement_of_the_theorem ?
It looks to me like we have everything to do this efficiently, right?

[Patrick Massot]

Yes, that's why it's in the trivial targets list

[Moritz Doll]

Since there seems to be no one actively working on this, I will do it (hopefully this week).

[Moritz Doll]

#15087 this is not pretty.

[Yakov Pechersky]

Is it any better if you use eval on docs#polynomial.taylor?

[Yakov Pechersky]

That is, make a function that gives the first n coeffs and feed that to a polynomial, then use the polynomial api?

[Moritz Doll]

I don't use anything related to polynomials, but for the API it might be better to use that.

[Wrenna Robson]

It feels to me that the Taylor sum should be define in terms of polynomials.

[Wrenna Robson]

https://math.stackexchange.com/a/758239

[Wrenna Robson]

There is a deep link between the Taylor sum and its error, and the theory of polynomial interpolants.

[Wrenna Robson]

We don't, I think, have Newton interpolation (and it might be a slight pain to do because it implies an ordering on your nodes).

[Wrenna Robson]

Indeed I'm not sure we have any analytic content to do with interpolants. But it should ideally unify with the Taylor approach...

[Heather Macbeth]

Maybe we should define docs#iterated_deriv to be a docs#power_series? I think @Yury G. Kudryashov has thought about this.

[Violeta Hernández]

It's quite odd that the Taylor polynomial isn't a polynomial

[Moritz Doll]

This has now been fixed, I have also added the Cauchy form of the remainder.

[Wrenna Robson]

I think the polynomial form should include the point about which you're taking the Taylor form

[Wrenna Robson]

Currently you include that in the evaluation

[Wrenna Robson]

and that doesn't make me happy I'm afraid

[Moritz Doll]

To be honest I am more bothered with getting the cont_diff assumption to be as sharp as possible, rewriting definition for the Taylor series is very easy.

[Yao Liu]

The most general assumption (for Lagrange remainder) must be that the (n+1)st derivative exists in the interior, and the n-th derivative (hence all lower derivatives) is continuous on the closed interval [a,b]. That's the Mean Value Theorem when n=0.

[Yao Liu]

The definition of Taylor polynomial only assumes n derivatives at that single point, which is ok for Peano remainder?

[Yao Liu]

How far is Complex Analysis coming along? I think Taylor series should be part of complex function theory, where you get something about the radius of convergence.

[Vincent Beffara]

We do have analyticity of holomorphic functions (e.g. docs#differentiable_on.has_fpower_series_on_ball) but the coefficients are given by Cauchy integrals rather than derivatives (docs#has_sum_cauchy_power_series_integral). Connecting the two is a matter of differentiation of parametric integrals, which have been meaning to do for a few weeks, but then it could also be done instead by showing that the Taylor polynomial can be obtained by truncation of the series and identifying the coefficients.

[Vincent Beffara]

BTW might it be more in the spirit of mathlib to first define the Taylor series at a point (as a term of type formal_multilinear_series) and to state Taylor's theorem as "under such and such differentiability assumptions, the truncation of the series matches the function up to this error term"? (Treating the higher order terms in the series as junk values.)

[Moritz Doll]

Yao Liu said:

The definition of Taylor polynomial only assumes n derivatives at that single point, which is ok for Peano remainder?

On the other end, the integral form of the remainder requires that the (n+1)st derivative be Lebesgue-integrable, or equivalently that the nth derivative is absolutely continuous (iirc). That's closer to being "n-times continuously differentiable" while in some sense is as sharp as possible.

I leave these two version for later PRs (and maybe to someone else).

[Moritz Doll]

@Vincent Beffara There is docs#has_ftaylor_series_up_to_on but the continuity of the highest derivative has to be in the interior only, so that is no good.

[Moritz Doll]

One could make the assumption has_ftaylor_series_up_to_on n f (set.Icc x0 x1) and has_ftaylor_series_up_to_on (n+1) f (set.Ioo x0 x1),
but that also feels not satisfactory.

[Moritz Doll]

@Patrick Massot what are your thoughts on this?

[Moritz Doll]

maybe we need two separate definitions: one using iterated_deriv and one using iterated_deriv_within? Then it would be easy to prove everything for taylor_sum_within and under the assumptions of the theorems one also has that taylor_sum_within = taylor_sum (because iterated_deriv_within = iterated_deriv at every point)

[Moritz Doll]

Wrenna Robson said:

I think the polynomial form should include the point about which you're taking the Taylor form

fixed that

[Moritz Doll]

the definition of the sum is now a bit useless, but before removing it, we should settle on a good name for taylor_polynomial. I was thinking that it should be something like taylor_poly_within or taylor_within and similarly rename taylor_coeff to taylor_coeff_within.

[Wrenna Robson]

What does the within signify?

[Moritz Doll]

that it is using deriv_within and not deriv

[Moritz Doll]

I suspect that one needs both variants in the end, but I have no good understanding how the calculus library works, so I might be very wrong.

[Yury G. Kudryashov]

I wanted to use formalization of Taylor's theorem to golf a lemma about real.log but all estimates in Analysis.Calculus.Taylor assume that x is to the right of a.

[Yury G. Kudryashov]

IMHO, this should be changed, but possibly after the port.

[Tomaz Gomes]

Was this solved? I am with the exact same problem, I wanted to use the theorem with x < a. Could you find a workaround, @Yury G. Kudryashov ?

[Yury G. Kudryashov]

Apply existing lemmas to -f(-x)?

[Yury G. Kudryashov]

Probably, the whole file should be rewritten.

[Yury G. Kudryashov]

We may want to have something similar to docs#intervalIntegral.FTCFilter to handle left/right/full nhds simultaneously.

[Yury G. Kudryashov]

Or have 3 versions of each lemma.

[Tomaz Gomes]

Yury G. Kudryashov said:

Apply existing lemmas to -f(-x)?

does not work in my case :( https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Exp.20bounded.20by.20Taylor's.20polynomial/near/402034060

[Bhavik Mehta]

I also came across this in the exponential ramsey project - here's the versions (in Lean 3) that I ended up making. This stuff is mostly but not completely ported, I can probably port and make PRs for it tonight if this kind of generality is what would be useful to you both?

[Patrick Massot]

Having more version of Taylor stuff seems worthwhile in any case.

[Bhavik Mehta]

True! Although I'm not completely certain that these versions are "better" than what's currently there, since I don't know this corner of the library well enough...

[Tomaz Gomes]

Bhavik Mehta said:

I also came across this in the exponential ramsey project - here's the versions (in Lean 3) that I ended up making. This stuff is mostly but not completely ported, I can probably port and make PRs for it tonight if this kind of generality is what would be useful to you both?

Yes! That would be super useful for me

[Yury G. Kudryashov]

I'm going to rewrite the file about Taylor series so that it works for maps between normed spaces.