Zulip Chat Archive

Stream: general

Topic: status of Taylor series


Scott Morrison (Feb 24 2021 at 03:48):

I would like to know that for ε > 0, the Taylor series for (x+ε)^{1/2} centered at x=1/2 converges uniformly on [0,1]. How far off stating/proving this are we? (I suspect a long way?)

Heather Macbeth (Feb 24 2021 at 03:50):

Maybe that wouldn't be so bad, actually? There's docs#has_fpower_series_on_ball.tendsto_locally_uniformly_on'

Heather Macbeth (Feb 24 2021 at 04:00):

You'd bound the growth of the coefficents of the Taylor series, then use a theorem like docs#formal_multilinear_series.le_radius_of_bound to get the radius of convergence.

Heather Macbeth (Feb 24 2021 at 04:05):

Perhaps a tricky point is to show that the random power series you write down for (x+ε)^{1/2} (involving the Catalan numbers, IIRC?) indeed converges to the square root function. That would follow from Mertens' theorem, but I don't think that's in mathlib.

Scott Morrison (Feb 24 2021 at 05:15):

I see! That's better than I'd realised.

Heather Macbeth (Feb 24 2021 at 05:16):

What do you need it for, btw? Maybe there's a hack for your use case.

Scott Morrison (Feb 24 2021 at 05:17):

Using Merten's theorem would require some messy calculation about the convolution of the power stores with itself, though.

Scott Morrison (Feb 24 2021 at 05:18):

I was thinking about Stone-Weierstrauss. I made a start on using Bernstein polynomials for this, and got a bit bored. :-) Pedersen in Analysis Now has a slick proof that uses the above fact.

Heather Macbeth (Feb 24 2021 at 05:19):

That would be great! Both in itself, and as a big missing ingredient for Fourier series.

Heather Macbeth (Feb 24 2021 at 09:02):

Speaking of this, how do you even define the Catalan numbers? I got the error

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r ℕ (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)

when I tried

import algebra.big_operators

open_locale big_operators
open finset

def catalan :   
| 0 := 1
| (n + 1) :=  i in range n.succ, catalan i * catalan (n - i)

Johan Commelin (Feb 24 2021 at 09:05):

@Heather Macbeth you need to "cheat" by summing over fin n.succ and adding a have := i.2 in the summand.

Johan Commelin (Feb 24 2021 at 09:06):

See for example https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/witt_vector/witt_polynomial.lean#L201

Johan Commelin (Feb 24 2021 at 09:06):

Afterwards, you can write an "equation lemma" that shows it's equal to what you would want to write (namely a sum over range)

Johan Commelin (Feb 24 2021 at 09:07):

Mario taught me this trick (-;

Mario Carneiro (Feb 24 2021 at 09:09):

Actually in this case you need i.2 but also a proof that n - i < n + 1 (this doesn't require any assumptions though)

Kevin Buzzard (Feb 24 2021 at 09:10):

Yes, the problem here is a bit harder than the Witt vector one

Heather Macbeth (Feb 24 2021 at 09:11):

def catalan :   
| 0       := 1
| (n + 1) :=  i : fin n.succ, have _ := i.2, have _ := nat.lt_succ_iff.mpr (n.sub_le i),
             catalan i * catalan (n - i)

Kevin Buzzard (Feb 24 2021 at 09:11):

Presumably you just add the proof of this to the local context too because the default tactic used to get rid of these assumptions is assumption

Kevin Buzzard (Feb 24 2021 at 09:12):

PR!

Scott Morrison (Feb 24 2021 at 09:13):

Then someone can start on the (in)famous exercise in Stanley's Enumerative Combinatorics showing that 66 different things are counted by the Catalan numbers...

Mario Carneiro (Feb 24 2021 at 09:21):

that's indeed enumerative

Heather Macbeth (Feb 24 2021 at 09:27):

No ... someone else (not me) can skip straight to Scott's terrible lemma,

variables (A : Type*) [ring A] [algebra  A]

/-- Maclaurin series for `sqrt (1 + x)` -/
def sqrt_one_plus : power_series A :=
power_series.mk $ λ n, algebra_map  A ((-1) ^ (n + 1) * (n + 1) * (catalan n) / (4 ^ n * (2 * n - 1)))

lemma sqrt_one_plus_sq : sqrt_one_plus A * sqrt_one_plus A = 1 + power_series.X := sorry

Scott Morrison (Feb 24 2021 at 09:30):

Thanks! This is already very helpful.

Heather Macbeth (Feb 24 2021 at 09:31):

Frankly I think the Bernstein polynomial approach will be more efficient ;-)

Scott Morrison (Feb 24 2021 at 09:34):

I guess with some complex analysis it becomes softer. Ideally you don't want to have to know anything about the actual coefficients of this power series, but just rely on knowing that it is analytic on a big enough domain.

Heather Macbeth (Feb 24 2021 at 09:44):

Sébastien actually proved the inverse function theorem for analytic functions a few weeks ago,
docs#formal_multilinear_series.radius_right_inv_pos_of_radius_pos

Heather Macbeth (Feb 24 2021 at 09:46):

So you could get the analyticity of 1+x\sqrt{1+x} from the analyticity of y21y^2-1. (I think.). But if I understand correctly there's no explicit bound obtained on the radius of convergence of the inverse.

Joseph Myers (Feb 25 2021 at 02:34):

Scott Morrison said:

Then someone can start on the (in)famous exercise in Stanley's Enumerative Combinatorics showing that 66 different things are counted by the Catalan numbers...

His more recent book "Catalan Numbers" (CUP, 2015) extends that to 214 things.

Johan Commelin (Feb 25 2021 at 03:46):

What is the next number in the sequence 66, 214, ... ?

Heather Macbeth (Feb 25 2021 at 03:53):

676 apparently!
https://oeis.org/A000287

Thomas Browning (Feb 25 2021 at 05:47):

Are you sure it's not 37?


Last updated: Dec 20 2023 at 11:08 UTC