Power series representation using multilinear map

Stream: new members

[Daniel Eriksson]

I am working on implementing Laurent series and been struggling to understand the nested function in the last line of the following, taken from Mathlib/Analysis/Analytic/Basic.lean.

structure HasFPowerSeriesOnBall (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E) (r : ℝ≥0∞) :

    Prop where

  r_le : r ≤ p.radius

  r_pos : 0 < r

  hasSum :

    ∀ {y}, y ∈ EMetric.ball (0 : E) r → HasSum (fun n : ℕ => p n fun _ : Fin n => y) (f (x + y))

We use HasSum (sum) (function) which sums over the function index and regard the coefficients as maps from E^n to F, a formal multilinear series p. It seems we construct the object y^n in a power series by a map from Fin n to y.

How does the line

fun n : ℕ => p n fun _ : Fin n => y

make sense?

It seems to be a map from N to Fin n to F, fun _ : Fin n => y is a function from Fin n to F, but do we make sense of multiplication with p n which is an object in F?

[Aaron Liu]

p is a FormalMultilinearSeries 𝕜 E F.
p n is a ContinuousMultilinearMap 𝕜 (fun (i : Fin n) => E) F.
DFunLike.coe (p n) is a (Fin n → E) → F.
(p n) fun _ : Fin n => y is a F.
fun n : ℕ => (p n) fun _ : Fin n => y is a ℕ → F.
Does that make sense?

[Daniel Eriksson]

Cleared up a bit, thanks. I struggle with lines 2-4, especially 4, is fun _ : Fin n of type Fin n -> E?

[Aaron Liu]

y is of type E, so fun (_ : Fin n) => y is of type Fin n → E