Iterated Laurent coefficients

Fubini's theorem writes a torus integral with the first circle integrated first. Consequently Laurent coefficients can be computed one coordinate at a time.

Main results

torusIntegral_succ_inner is Fubini for the first circle of a coordinate torus. multivariableLaurentCoeff_succ identifies the multivariable coefficient with an iterated one-variable coefficient in the remaining coordinates.

theorem SeveralComplexVariables.torusIntegral_succ_inner {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (Fin (n + 1) → ℂ) → F} {c : Fin (n + 1) → ℂ} {r : Fin (n + 1) → ℝ} (hf : TorusIntegrable f c r) : torusIntegral f c r = ∯ (y : Fin n → ℂ) in T(c ∘ Fin.succ, r ∘ Fin.succ), ∮ (x : ℂ) in C(c 0, r 0), f (Fin.cons x y)

A torus integral can be evaluated by first integrating the first coordinate circle.

theorem SeveralComplexVariables.multivariableLaurentCoeff_succ {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : (Fin (n + 1) → ℂ) → F} {r : Fin (n + 1) → ℝ} (hr : ∀ (i : Fin (n + 1)), 0 < r i) (hf : Continuous fun (θ : Fin (n + 1) → ℝ) => f (torusMap 0 r θ)) (m : Fin (n + 1) → ℤ) : multivariableLaurentCoeff f r m = multivariableLaurentCoeff (fun (y : Fin n → ℂ) => circleLaurentCoeff (fun (x : ℂ) => f (Fin.cons x y)) (r 0) (m 0)) (r ∘ Fin.succ) (m ∘ Fin.succ)

A multivariable Laurent coefficient is obtained by taking a circle coefficient first.