HasPowerSeries

Stream: mathlib4

[Yongxi Lin (Aaron)]

Is it a good idea to have APIs for HasPowerSeries (the analogue of HasFPowerSeries for one dimensional domain)? I want to state in lean that we have an entire function $f:\mathbb{C}\rightarrow\mathbb{C}$ such that $\forall z\in \mathbb{C}, f(z)=\sum_{n=0}^\infty a_nz^n$ for some sequence of complex numbers $a_n$ and I found theorems related to HasFPowerSeries hard to use.

[Weiyi Wang]

Do you have a proposed definition? I once had a similar idea but it was vague and I never figured out what exactly I wanted

[Yongxi Lin (Aaron)]

Two possible definitions:

import Mathlib

variable {𝕜 E : Type*} {f : 𝕜 → E} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E]
  [NormedSpace 𝕜 E]

def seq_FormalMultilinearSeries (a : ℕ → E) : FormalMultilinearSeries 𝕜 𝕜 E :=
  fun n => ⟨⟨fun l => (∏ i, l i) • a n, sorry, sorry⟩, by fun_prop⟩

def HasPowerSeriesOnBall (f : 𝕜 → E) (a : ℕ → E) (x : 𝕜) (r : ENNReal) : Prop :=
  HasFPowerSeriesOnBall f (seq_FormalMultilinearSeries a) x r

def HasPowerSeriesOnBall' (f : 𝕜 → E) (a : ℕ → E) (x : 𝕜) (r : ENNReal) : Prop :=
  ∀ {y}, y ∈ EMetric.ball (0 : 𝕜) r → HasSum (fun n => y ^ n • (a n)) (f (x + y))

/- A function `f : 𝕜 → E` has a power series representation `f z = ∑ aₙzⁿ`. -/
variable {a : ℕ → E} (hf : HasPowerSeriesOnBall' f a x ⊤)