The Taylor series of an entire function converges to it

Stream: Is there code for X?

[Michael Stoll]

I would like to use the fact that the Taylor series (at zero, say) of an entire function f : ℂ → ℂ converges everywhere to f:

import Mathlib

open BigOperators in
lemma taylorSeries_of_entire {f : ℂ → ℂ} (hf : Differentiable ℂ f) (z : ℂ) :
    ∑' n : ℕ, (n.factorial : ℂ)⁻¹ * iteratedDeriv n f 0 * z ^ n = f z := sorry

Using Differentiable.hasFPowerSeriesOnBall, I can get to

HasSum (fun n ↦ (cauchyPowerSeries f 0 (↑R) n) fun x ↦ z) (f z)

but my problem now is that I need to relate cauchyPowerSeries f 0 (↑R) (where R is some suitable radius) with the Taylor series. Unfortunately,
@loogle cauchyPowerSeries, iteratedDeriv

[loogle]

:shrug: nothing found

[Michael Stoll]

there does not seem to be API relating the two. Any ideas how to proceed here?

[Michael Stoll]

I see "TODO: add a version for higher derivatives." in the docs for docs#Complex.deriv_eq_smul_circleIntegral, so maybe it is time to tackle this?

[Michael Stoll]

I can reduce my statement to

import Mathlib

namespace Complex
open Real

lemma iteratedDeriv_eq_smul_circleIntegral {R : ℝ} {c : ℂ} {f : ℂ → ℂ} (hR : 0 < R)
    (hf : Differentiable ℂ f) (n : ℕ) :
    iteratedDeriv n f c =
      ((2 * π * I)⁻¹ * n.factorial) • ∮ (z : ℂ) in C(c, R), (z - c) ^ (-(n + 1 : ℤ)) • f z := by
  sorry

I guess the "TODO" mentioned above requires the first "TODO: add a version for w ∈ Metric.ball c R".
@Yury G. Kudryashov I think you wrote docs#Complex.deriv_eq_smul_circleIntegral originally. Did you have thoughts on how to deal with these TODOs?

[Yury G. Kudryashov]

I can have a look in 3h

[Michael Stoll]

I'll be in bed by then, but I'm looking forward to seeing whatever you might have tomorrow morning!

[Junyan Xu]

import Mathlib.Analysis.Calculus.FDeriv.Analytic

open ENNReal Nat

universe u v

variable {𝕜 : Type*} {E : Type u} {F : Type v} [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F)

noncomputable section

lemma Fin.snoc_zero {α : Type*} (p : Fin 0 → α) (x : α) :
    Fin.snoc p x = fun _ ↦ x := by
  ext y
  have : Subsingleton (Fin (0 + 1)) := Fin.subsingleton_one
  simp [Subsingleton.elim y (Fin.last 0)]

lemma Finset.piecewise_same {α : Type*} {δ : α → Sort*} (s : Finset α)
    (f : (i : α) → δ i) [(j : α) → Decidable (j ∈ s)] :
    s.piecewise f f = f := by
  ext i; by_cases h : i ∈ s <;> simp [h]

namespace FormalMultilinearSeries

-- This series appears in `HasFPowerSeriesOnBall.fderiv`
def derivSeries : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F) :=
  (continuousMultilinearCurryFin1 𝕜 E F : (E[×1]→L[𝕜] F) →L[𝕜] E →L[𝕜] F)
    |>.compFormalMultilinearSeries (p.changeOriginSeries 1)

theorem derivSeries_apply_diag (n : ℕ) (x : E) :
    derivSeries p n (fun _ ↦ x) x = (n + 1) • p (n + 1) fun _ ↦ x := by
  simp [derivSeries, changeOriginSeries]
  convert Finset.sum_const _
  · rw [Fin.snoc_zero, changeOriginSeriesTerm_apply, Finset.piecewise_same, add_comm]
  erw [← Fintype.card, Fintype.card_subtype, ← Finset.powersetCard_eq_filter,
    Finset.card_powersetCard, ← Fintype.card, Fintype.card_fin,
    eq_comm, add_comm, choose_succ_self_right]

end FormalMultilinearSeries

namespace HasFPowerSeriesOnBall
open FormalMultilinearSeries

variable {f : E → F} {x : E} {r : ℝ≥0∞} (h : HasFPowerSeriesOnBall f p x r) (y : E) {p}
-- assumption h could be replaced by HasFPowerSeriesAt

theorem iteratedFDeriv_zero_apply_diag :
    iteratedFDeriv 𝕜 0 f x (fun _ ↦ y) = p 0 (fun _ ↦ y) := by
  convert (h.hasSum <| EMetric.mem_ball_self h.r_pos).tsum_eq.symm
  · rw [iteratedFDeriv_zero_apply, add_zero]
  rw [tsum_eq_single 0]; · exact congr(p 0 $(Subsingleton.elim _ _))
  intro n hn; haveI := NeZero.mk hn; exact (p n).map_zero

private theorem factorial_smul' : ∀ {F : Type max u v} [NormedAddCommGroup F]
    [NormedSpace 𝕜 F] [CompleteSpace F] {p : FormalMultilinearSeries 𝕜 E F}
    {f : E → F}, HasFPowerSeriesOnBall f p x r →
    n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) := by
  induction' n with n ih <;> intro F _ _ _ p f h
  · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
  rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
    ← ContinuousLinearMap.smul_apply, derivSeries, ih h.fderiv,
    iteratedFDeriv_succ_apply_right]
  rfl

variable [CompleteSpace F]

theorem factorial_smul (n : ℕ) :
    n ! • p n (fun _ ↦ y) = iteratedFDeriv 𝕜 n f x (fun _ ↦ y) := by
  cases n
  · rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]
  erw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
    ← ContinuousLinearMap.smul_apply, factorial_smul'.{_,u,v} _ h.fderiv,
    iteratedFDeriv_succ_apply_right]
  rfl

theorem HasFPowerSeriesOnBall.hasSum_iteratedFDeriv [CharZero 𝕜]
    (h : HasFPowerSeriesOnBall f p x r) {y : E} (hy : y ∈ EMetric.ball 0 r) :
    HasSum (fun n ↦ (1 / n ! : 𝕜) • iteratedFDeriv 𝕜 n f x fun _ ↦ y) (f (x + y)) := by
  convert h.hasSum hy with n
  rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul, mul_one_div_cancel, one_smul]
  rw [Nat.cast_ne_zero]; apply Nat.factorial_ne_zero

/- We can't quite show
  `HasFPowerSeriesOnBall f (fun n ↦ (1 / n !) • iteratedFDeriv 𝕜 n f x) x r`
  because `r_le` requires bounding the norm of a multilinear map using values on
  the diagonal, so some polarization identity would be required. -/

end HasFPowerSeriesOnBall

[Junyan Xu]

Combining the above with docs#iteratedDeriv_eq_iteratedFDeriv, docs#ContinuousMultilinearMap.map_smul_univ, and docs#Differentiable.hasFPowerSeriesOnBall should get you there.

[Yury G. Kudryashov]

Thank you!

[Michael Stoll]

@Junyan Xu thanks! I'll see how far I get with this, but it looks good.

[Michael Stoll]

With what you have provided, I now have

namespace Complex

open BigOperators Nat

variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]

lemma taylorSeries_on_ball {f : ℂ → E} {r : NNReal} (hr : 0 < r)
    (hf : DifferentiableOn ℂ f (Metric.closedBall c r)) {z : ℂ} (hz : z ∈ Metric.ball c r) :
    ∑' n : ℕ, (1 / n ! : ℂ) • (z - c) ^ n • iteratedDeriv n f c = f z := by
  have hz' : z - c ∈ EMetric.ball 0 r
  · rw [Metric.emetric_ball_nnreal]
    exact mem_ball_zero_iff.mpr hz
  have H := ((hf.hasFPowerSeriesOnBall hr).hasSum_iteratedFDeriv hz').tsum_eq
  simp only [add_sub_cancel'_right] at H
  convert H using 4 with n
  simpa only [iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, mul_one, Finset.prod_const,
    Finset.card_fin]
    using ((iteratedFDeriv ℂ n f c).map_smul_univ (fun _ ↦ z - c) (fun _ ↦ 1)).symm

and variants for Differentiable/ functions ℂ → ℂ. Thanks again!

[Michael Stoll]

I will add this to the "Auxiliary.lean" file here for the time being, where I collect all the missing API lemmas I need, to be turned into Mathlib PRs eventually.

[Junyan Xu]

I think it's possible to extract a result that is true in arbitrary characteristics; even though it's harder to prove and currently left as a sorry, it will make it easy to prove HasPowerSeriesOnBall f (fun n ↦ (1 / n!) • iteratedFDeriv 𝕜 n f x) x r in the char zero case without resorting to a polarization identity, and without needing to prove the permutation invariance of iteratedDeriv (it follows as a consequence of the result for analytic functions, but it's more generally true for ContDiff functions). Once this is proved I'll make a PR.

[Michael Stoll]

#10087 for the above and the application to holomorphic functions.

[Junyan Xu]

Thanks! Three initial comments:

• I think your original formulation using (n !)⁻¹ is better because it's the simp normal form due to docs#one_div; I used 1 / n ! mainly because I didn't read your goal carefully :sweat_smile:. docs#taylorCoeffWithin also uses (n !)⁻¹, but that file is restricted to the reals, and doesn't state anything about limits or HasSum, only bounds on remainders.

• There are also docs#ftaylorSeries which basically reorders the arguments of docs#iteratedFDeriv without incorporating the (n !)⁻¹ factor, and docs#HasFTaylorSeriesUpTo follows the same vein. docs#Polynomial.taylor has coefficients given by docs#Polynomial.hasseDeriv, which has the (k !)⁻¹ built into the denominator of n.choose k (you could consider it a version of docs#FormalMultilinearSeries.changeOrigin).
  Although your PR is not about any of these defs with "taylor" in the name, I think your choice of using "taylor" to name the lemmas is acceptable.

• I'll still try to refactor your PR through this intermediate result, but that could be a separate PR and could be merged before or after yours.

[Yury G. Kudryashov]

Note that we have 2 incompatible types of "Taylor series" in Mathlib:

• the series of n-th derivatives, as in docs#HasFTaylorSeriesUpTo
• the series that converges to the function, as in docs#AnalyticAt

Some day, we should separate these 2 notions into 2 separate type synonyms, but for now you have to be careful when you go from one series to another and back again.

[Yury G. Kudryashov]

BTW, I think that the first kind should be refactored into Jet and have ∀ i : Fin n, ContinuousMultilinearMap .. instead of ∀ i : Nat, _ as its data.

[Yury G. Kudryashov]

This way we won't have unused data in the definition of HasFTaylorSeriesUpTo

[Michael Stoll]

I think the docstring "Formal Taylor series associated to a function within a set." of docs#ftaylorSeries is not correct, as there is no set involved.

If docs#taylorCoeffWithin were not restricted to the reals and within a set, it would make sense to use it. But I have no intention in getting lost in rabbit holes fixing this part of Mathlib :smile:

I'll change 1 / n ! to (n !)⁻¹ and would appreciate your reviews on the PR.

[Michael Stoll]

Michael Stoll said:

But I have no intention in getting lost in rabbit holes fixing this part of Mathlib :smile:

(I think @Yury G. Kudryashov has some plans in this direction, however.)

[Junyan Xu]

Yury G. Kudryashov said:

BTW, I think that the first kind should be refactored into Jet and have ∀ i : Fin n, ContinuousMultilinearMap .. instead of ∀ i : Nat, _ as its data.

Using Nat allows to treat smooth functions and finitely differentiable functions together; maybe that's the main reason why it's used.

[Michael Stoll]

Michael Stoll said:

I think the docstring "Formal Taylor series associated to a function within a set." of docs#ftaylorSeries is not correct, as there is no set involved.

I fixed the docstring in the PR.

[Yury G. Kudryashov]

Junyan Xu said:

Yury G. Kudryashov said:

BTW, I think that the first kind should be refactored into Jet and have ∀ i : Fin n, ContinuousMultilinearMap .. instead of ∀ i : Nat, _ as its data.

Using Nat allows to treat smooth functions and finitely differentiable functions together; maybe that's the main reason why it's used.

We can use EFin (n : ENat) := {k : Nat // k < n} as the index type.

[Yury G. Kudryashov]

But I didn't think all the details through, so it's possible that using functions from Nat is easier.

[Vasilii Nesterov]

Junyan Xu said:

I think it's possible to extract a result that is true in arbitrary characteristics; even though it's harder to prove and currently left as a sorry, it will make it easy to prove HasPowerSeriesOnBall f (fun n ↦ (1 / n!) • iteratedFDeriv 𝕜 n f x) x r in the char zero case without resorting to a polarization identity, and without needing to prove the permutation invariance of iteratedDeriv (it follows as a consequence of the result for analytic functions, but it's more generally true for ContDiff functions). Once this is proved I'll make a PR.

Hi there! Am I correct that it hasn’t been PRd yet and that we still don’t have a HasPowerSeriesOnBall result for the Taylor series? If so, I’d like to work on it and would be grateful if someone could update me on the current status. Should I just fill the sorries in this branch?

[Junyan Xu]

I had the impression that this has been subsumed by @Sébastien Gouëzel's work, but I need to check.

[Sébastien Gouëzel]

We have the fact that the iterated derivative of an analytic map is given by the symmetrization of the coefficient of the power series, in docs#HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum_of_completeSpace. From this, the result you're interested it should follow readily, although I don't think it is in mathlib in this form yet.