Complex-valued series

DefinitionRadius of convergence#

The radius of a formal multilinear series is the largest r such that the sum Σ ‖pₙ‖ ‖y‖ⁿ converges for all ‖y‖ < r. This implies that Σ pₙ yⁿ converges for all ‖y‖ < r, but these definitions are not equivalent in general.

FormalMultilinearSeries.radius.{u_1, u_3, u_4} {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) : ENNReal
Sources
MathlibFormalMultilinearSeries.radius
Uses 4 · Used by 12
Statement usesContinuous function · Finite set · Multilinear map · Normed vector space over a normed field
Used byAnalytic function · Approximation by convolution · Smooth immersion · Smooth map between manifolds · Smooth or analytic manifold (with boundary and corners) · (smooth) vector bundle · Cauchy–Hadamard theorem · Taylor's theorem with integral form for remainder (Differential calculus) · Continuity (Complex-valued series) · Differentiability with respect to the complex variable · Taylor's theorem with integral form for remainder (Taylor-like theorems) · Taylor's theorem with Lagrange form for remainder

TheoremContinuity (Complex-valued series)#

If a function admits a power series expansion on a ball, then it is continuous there.

HasFPowerSeriesOnBall.continuousOn.{u_1, u_2, u_3} {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3}
  [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal}
  (hf : HasFPowerSeriesOnBall f p x r) : ContinuousOn f (Metric.eball x r)
Sources
MathlibHasFPowerSeriesOnBall.continuousOn
Uses 8 · Used by 2
Statement usesInfinite sum · Radius of convergence
Proof usesBall · Field \(\R\) of real numbers · Order topology · Ordered ring · Topological ring · Topology on a normed vector space
Used byPrinciple of isolated zeros · Cauchy formulas

TheoremDifferentiability with respect to the complex variable#

Mathlib states this as HasFPowerSeriesOnBall.differentiableOn.

HasFPowerSeriesOnBall.differentiableOn.{u, v, u_1} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
  {E : Type u} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type v} [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E}
  [CompleteSpace F] (h : HasFPowerSeriesOnBall f p x r) : DifferentiableOn 𝕜 f (Metric.eball x r)
Sources
MathlibHasFPowerSeriesOnBall.differentiableOn
Uses 8
Statement usesCompleteness · Holomorphic functions · Infinite sum · Radius of convergence
Proof usesAnalytic function · Differentiable function between normed vector spaces · Norm of a continuous linear map · Topology on a normed vector space

DefinitionComplex exponential#

The complex exponential function, defined via its Taylor series

Complex.exp (z : ℂ) : ℂ
Sources
MathlibComplex.exp
Uses 4 · Used by 7
Statement usesComplex number · Field \(\R\) of real numbers · Finite set · Order
Used byExponential · Hyperbolic trigonometric functions · Characteristic function · Complex roots of unity · Primitive complex roots of unity · Cos (extension of trigonometric functions to the complex plane) · Sin (extension of trigonometric functions to the complex plane)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.