Normal convergence of Laurent coefficient families

Inner and outer coefficient tori bound the two halves of each coordinate series by geometric sequences. Their finite products give summable local majorants.

Main results

exists_local_laurent_majorant produces a geometric bound from inner and outer tori. summable_norm_multivariableLaurent is absolute summability of the terms. hasSumLocallyUniformlyOn_multivariableLaurent_of_pointwise upgrades a pointwise summable expansion to locally uniform convergence.

theorem SeveralComplexVariables.exists_local_laurent_majorant {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsPreconnected U) (hR : IsReinhardt U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {r : Fin n → ℝ} (hr : ∀ (i : Fin n), 0 < r i) (hrU : (fun (i : Fin n) => ↑(r i)) ∈ U) {z : Fin n → ℂ} (hz : z ∈ U) : ∃ N ∈ nhds z, N ⊆ U ∧ ∃ (B : (Fin n → ℤ) → ℝ), Summable B ∧ ∀ (m : Fin n → ℤ), ∀ w ∈ N, ‖multivariableLaurentTerm (multivariableLaurentCoeff f r) m w‖ ≤ B m

Every point has a neighborhood on which the Laurent terms admit a summable majorant.

theorem SeveralComplexVariables.summable_norm_multivariableLaurent {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsPreconnected U) (hR : IsReinhardt U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {r : Fin n → ℝ} (hr : ∀ (i : Fin n), 0 < r i) (hrU : (fun (i : Fin n) => ↑(r i)) ∈ U) {z : Fin n → ℂ} (hz : z ∈ U) : Summable fun (m : Fin n → ℤ) => ‖multivariableLaurentTerm (multivariableLaurentCoeff f r) m z‖

The Laurent expansion family is absolutely summable at every point of the domain.

theorem SeveralComplexVariables.hasSumLocallyUniformlyOn_multivariableLaurent_of_pointwise {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] [CompleteSpace F] {U : Set (Fin n → ℂ)} (ho : IsOpen U) (hc : IsPreconnected U) (hR : IsReinhardt U) {f : (Fin n → ℂ) → F} (hf : AnalyticOnNhd ℂ f U) {r : Fin n → ℝ} (hr : ∀ (i : Fin n), 0 < r i) (hrU : (fun (i : Fin n) => ↑(r i)) ∈ U) (hsum : ∀ z ∈ U, HasSum (fun (m : Fin n → ℤ) => multivariableLaurentTerm (multivariableLaurentCoeff f r) m z) (f z)) : HasSumLocallyUniformlyOn (multivariableLaurentTerm (multivariableLaurentCoeff f r)) f U

Pointwise Laurent expansion with torus coefficients automatically converges locally uniformly.