AnalyticOn.hasFPowerSeriesOnBall

Stream: Is there code for X?

[Vasilii Nesterov]

Am I correct in thinking that something like

lemma AnalyticOn.hasFPowerSeriesOnBall {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {s : Set 𝕜} (h : AnalyticOn 𝕜 f s) :
    let p := FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial);
    s ⊆ EMetric.ball x p.radius → HasFPowerSeriesOnBall f p x p.radius := by
  sorry

(mirroring docs#AnalyticAt.hasFPowerSeriesAt) is not in Mathlib and cannot be easily derived from what is already there?

[Sébastien Gouëzel]

This one is not true: HasFPowerSeriesOnBall f p x p.radius talks about all the values of f on the ball, while h only says something on s.

[Vasilii Nesterov]

You're right. This should be correct:

lemma AnalyticOn.hasFPowerSeriesOnBall {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} {r : ENNReal} (h : AnalyticOn 𝕜 f (EMetric.ball x r)) :
    let p := FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial);
    r ≤ p.radius → HasFPowerSeriesOnBall f p x r := by
  sorry

[Sébastien Gouëzel]

Unfortunately, this one is still wrong, but for a more subtle reason. Take 𝕜 = ℚ_p. This is a totally disconnected space. The function f equal to 1 on the closed ball of radius 1, and to 0 elsewhere, is locally constant. In particular, it is analytic. But it does not coincide globally with its power zeries at 0.

[David Loeffler]

It's false for the reals as well, right? Something like 1 / (1 + x^2) would be a counterexample. It's really a very special property of the complexes that this does work.

[Sébastien Gouëzel]

No, it's true for the reals because he assumes r ≤ p.radius.

[David Loeffler]

You're right that my counterexample doesn't work, but I think it's still false for $\mathbb{R}$, doesn't $f(y) = \exp(-1/y^2)$ give a counterexample? The Taylor series at 0 has infinite radius of convergence, but its sum is not f.

[Sébastien Gouëzel]

Yes, but the function is not analytic at 0.

[Sébastien Gouëzel]

The proof is the following. Considering f minus the power series associated to p, it suffices to show that an analytic function on B 0 r with all derivatives at 0 equal to 0 vanishes on the whole ball B 0 r. It's true on a neighborhood of 0 by analyticity, and then by connectedness you propagate this to the whole ball.