Taylor series

Stream: Is there code for X?

[Vincent Beffara]

Is there somewhere in mathlib the statement that an analytic function is locally the sum of its Taylor series?

[Sebastien Gouezel]

I don't think so. We have that an analytic function is the sum of some series, but no identification between the coefficients and the n-th derivative divided by n!. One reason for this is that it's not true in general (it's wrong in nonzero characteristic...), but having it over reals or complexes would definitely be desirable.

[Vincent Beffara]

Now I can prove this:

variables {p : formal_multilinear_series ℂ ℂ ℂ} {f : ℂ → ℂ} {w : ℂ} {n : ℕ}

example (hp : has_fpower_series_at f p w) : deriv^[n] f w = n.factorial * p.coeff n

But the proof is ugly and slow and would benefit from some refactoring and generalization.

[Vincent Beffara]

And btw, it was the las missing step in the proof of

lemma analytic_continuation (hU1 : is_open U) (hU2 : is_preconnected U) (hw : w ∈ U)
  (hf1 : analytic_on ℂ f U) (hf2 : ∃ᶠ z in 𝓝[≠] w, f z = 0) :
  eq_on f 0 U

[Sebastien Gouezel]

Yes, it's definitely not the right statement (but sill useful to have :-). The right statement works in any dimension, and shows very nicely where the factorial comes from. It reads as follows: if you have an analytic function f around x, with power series coefficients p n (so, p n is an n multilinear map, but not symmetric in general since this is not always possible in nonzero characteristic), then the n-th Fréchet derivative of f is an n-multilinear function given by $D^n f (x; v_1, \dotsc, v_n) = \sum_{\sigma \in S_n} p_n (v_{\sigma(1)}, \dotsc, v_{\sigma(n)})$.

When you are in dimension 1, you can identify multilinear maps with scalars, and the statement becomes $Df^n(x) = \sum_{\sigma \in S_n} p_n = n! \cdot p_n$.

[Sebastien Gouezel]

I am not saying that you shouldn't PR your version, by the way: the general case will probably be very ugly to prove, and it shouldn't hold you back!

[Vincent Beffara]

Indeed the statement is the wrong one. But in the end I found a nicer proof that does not use the series expansion at all so I am in less of a hurry:

lemma is_open_set_of_eventually_nhds_within [α : Type*] [topological_space α] [t1_space α]
  {p : α → Prop} : is_open {x | ∀ᶠ y in 𝓝[≠] x, p y} :=
begin
  simp only [is_open_iff_mem_nhds, eventually_nhds_within_iff, _root_.eventually_nhds_iff],
  rintro z ⟨t, ht1, ht2, ht3⟩,
  refine filter.mem_of_superset (ht2 z ht3) (λ a ha, _),
  by_cases a = z,
  { subst h; exact ⟨t, ht1, ht2, ht3⟩ },
  { refine ⟨t ∩ {z}ᶜ, _, _, _⟩,
    { exact λ x ⟨hx1, hx2⟩ hx3, ht1 x hx1 hx2 },
    { exact λ x ⟨hx1, hx2⟩, filter.inter_mem (ht2 x hx1) (is_open_compl_singleton.mem_nhds hx2) },
    { exact ⟨ha, h⟩ } },
end

lemma uniqueness' (hU1 : is_open U) (hU2 : is_preconnected U)
  (hf1 : analytic_on 𝕜 f U) (hw : w ∈ U) (hf2 : ∃ᶠ z in 𝓝[≠] w, f z = 0) :
  eq_on f 0 U :=
begin
  replace hf2 := (hf1 w hw).frequently_zero_iff_eventually_zero.mp hf2,
  by_contra,
  simp only [eq_on, not_forall, exists_prop] at h,
  obtain ⟨x, hx1, hx2⟩ := h,

  let u := { z | f =ᶠ[𝓝 z] 0 },
  have hu : is_open u := is_open_set_of_eventually_nhds,
  have hu' : (U ∩ u).nonempty := ⟨w, hw, hf2⟩,

  let v := { z | ∀ᶠ w in 𝓝[≠] z, f w ≠ 0 },
  have hv : is_open v := by apply is_open_set_of_eventually_nhds_within,
  have hv' : (U ∩ v).nonempty,
    from ⟨x, hx1, ((hf1 x hx1).continuous_at.eventually_ne hx2).filter_mono nhds_within_le_nhds⟩,

  have huv : U ⊆ u ∪ v := λ z hz, (hf1 z hz).eventually_eq_zero_or_eventually_ne_zero,
  have huv' : u ∩ v = ∅,
    by { ext z,
      simp only [mem_inter_eq, mem_empty_eq, iff_false, not_and],
      exact λ h, (h.filter_mono nhds_within_le_nhds).frequently },

  simpa [huv'] using hU2 u v hu hv huv hu' hv'
end