status of Taylor series

Stream: general

[Scott Morrison]

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]

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

[Heather Macbeth]

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]

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]

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

[Heather Macbeth]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Heather Macbeth]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Mario taught me this trick (-;

[Mario Carneiro]

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]

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

[Heather Macbeth]

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]

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]

PR!

[Scott Morrison]

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]

that's indeed enumerative

[Heather Macbeth]

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]

Thanks! This is already very helpful.

[Heather Macbeth]

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

[Scott Morrison]

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]

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]

So you could get the analyticity of $\sqrt{1+x}$ from the analyticity of $y^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]

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]

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

[Heather Macbeth]

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

[Thomas Browning]

Are you sure it's not 37?