Complex analysis

TheoremCauchy integral formula#

Cauchy integral formula: if f : ℂ → E is complex differentiable on an open disc and is continuous on its closure, then for any w in this open ball we have \(\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)\).

DiffContOnCl.circleIntegral_sub_inv_smul.{u} {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E} (h : DiffContOnCl ℂ f (Metric.ball c R))
  (hw : w ∈ Metric.ball c R) :
  ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f w
Sources
MathlibDiffContOnCl.circleIntegral_sub_inv_smul
Uses 8 · Used by 3
Statement usesBall · Bochner integral · Carathéodory's theorem (measure theory) · Cos (extension of trigonometric functions to the complex plane) · Differentials (linear tangent functions) · Holomorphic functions · Lebesgue measure (Measures and integral calculus)
Proof usesCauchy formulas
Used byMaximum modulus principle · Phragmen-Lindelöf principle · Schwarz lemma

TheoremLiouville theorem#

Liouville's theorem: a complex differentiable bounded function f : E → F is a constant.

Differentiable.apply_eq_apply_of_bounded.{u, v} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : E → F}
  (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) (z w : E) : f z = f w
Sources
MathlibDifferentiable.apply_eq_apply_of_bounded
Uses 8 · Used by 1
Statement usesComplex number · Differentiable functions · Normed vector space over a normed field
Proof usesCauchy formulas · Completion of an abelian topological group · Derivative at a point · Higher-order derivatives of functions · Holomorphic functions
Used by\(\C\) is algebraically closed

TheoremMaximum modulus principle#

Maximum modulus principle: if f : E → F is complex differentiable in a neighborhood of c and the norm ‖f z‖ has a local maximum at c, then f is locally constant in a neighborhood of c.

Complex.eventually_eq_of_isLocalMax_norm.{u, v} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℂ E] {F : Type v} [NormedAddCommGroup F] [NormedSpace ℂ F] [StrictConvexSpace ℝ F]
  {f : E → F} {c : E} (hd : ∀ᶠ (z : E) in nhds c, DifferentiableAt ℂ f z)
  (hc : IsLocalMax (norm ∘ f) c) : ∀ᶠ (y : E) in nhds c, f y = f c
Sources
MathlibComplex.eventually_eq_of_isLocalMax_norm
Uses 9 · Used by 1
Statement usesComplex number · Differentiable function between normed vector spaces · Normed vector space over a normed field
Proof usesAffine function · Cauchy integral formula · Completion of an abelian topological group · Euclidean affine space · Lipschitz continuity · The Triangle Inequality
Used byOpen mapping theorem (complex analysis)

TheoremPrinciple of isolated zeros#

The principle of isolated zeros for an analytic function, local version: if a function is analytic at z₀, then either it is identically zero in a neighborhood of z₀, or it does not vanish in a punctured neighborhood of z₀.

AnalyticAt.eventually_eq_zero_or_eventually_ne_zero.{u_1, u_2} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E}
  {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) :
  (∀ᶠ (z : 𝕜) in nhds z₀, f z = 0) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ 0
Sources
MathlibAnalyticAt.eventually_eq_zero_or_eventually_ne_zero
Uses 6 · Used by 1
Statement usesAnalytic function
Proof usesAffine space · Continuity (Complex-valued series) · Differentials (linear tangent functions) · Hausdorff space · Norm of a continuous linear map
Used byPrinciple of analytic continuation

TheoremPrinciple of analytic continuation#

The identity principle for analytic functions, global version: if two functions are analytic on a connected set U and coincide at points which accumulate to a point z₀ ∈ U, then they coincide globally in U. For higher-dimensional versions requiring that the functions coincide in a neighborhood of z₀, see AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq.

AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq.{u_1, u_2} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E}
  {z₀ : 𝕜} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U) (hU : IsPreconnected U)
  (h₀ : z₀ ∈ U) (hfg : ∃ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = g z) : Set.EqOn f g U
Sources
MathlibAnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq
Uses 3 · Used by 1
Statement usesAnalytic function
Proof usesPrinciple of isolated zeros · Topology of a metric space
Used byOpen mapping theorem (complex analysis)

TheoremAnalyticity of holomorphic functions#

If f : ℂ → E is complex differentiable on some set s, then it is analytic at any point z such that s ∈ 𝓝 z (equivalently, z ∈ interior s).

DifferentiableOn.analyticAt.{u} {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E]
  [CompleteSpace E] {s : Set ℂ} {f : ℂ → E} {z : ℂ} (hd : DifferentiableOn ℂ f s)
  (hz : s ∈ nhds z) : AnalyticAt ℂ f z
Sources
MathlibDifferentiableOn.analyticAt
Uses 5 · Used by 2
Statement usesAnalytic function · Complex number · Holomorphic functions · Inner product space, over \(R\) or \(C\)
Proof usesCauchy formulas
Used byMorera's theorem · Open mapping theorem (complex analysis)

TheoremSchwarz lemma#

The Schwarz Lemma. Let f : E → F be a complex analytic on an open ball with center at the origin. If f sends this ball to the closed ball with center 0 of the same radius and f 0 = 0, then for any point z of this disk we have ‖f z‖ ≤ ‖z‖.

Complex.norm_le_norm_of_mapsTo_ball.{u_1, u_2} {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [NormedAddCommGroup F] [NormedSpace ℂ F] {R : ℝ} {f : E → F} {z : E}
  (hd : DifferentiableOn ℂ f (Metric.ball 0 R))
  (h_maps : Set.MapsTo f (Metric.ball 0 R) (Metric.closedBall 0 R)) (h₀ : f 0 = 0) (hz : ‖z‖ < R) :
  ‖f z‖ ≤ ‖z‖
Sources
MathlibComplex.norm_le_norm_of_mapsTo_ball
Uses 9
Statement usesBall · Complex number · Holomorphic functions · Normed vector space over a normed field
Proof usesAffine function · Cauchy integral formula · Hahn-Banach theorem · Lipschitz continuity · Removable singularity

TheoremRemovable singularity#

Removable singularity theorem: if s is a punctured neighborhood of c : ℂ, a function f : ℂ → E is complex differentiable on s, and \(f(z) - f(c)=o((z-c)^{-1})\), then f redefined to be equal to limUnder (𝓝[≠] c) f at c is complex differentiable on {c} ∪ s.

Complex.differentiableOn_update_limUnder_insert_of_isLittleO.{u} {E : Type u} [NormedAddCommGroup E]
  [NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ} {c : ℂ} (hc : s ∈ nhdsWithin c {c}ᶜ)
  (hd : DifferentiableOn ℂ f s)
  (ho : (fun z => f z - f c) =o[nhdsWithin c {c}ᶜ] fun z => (z - c)⁻¹) :
  DifferentiableOn ℂ (Function.update f c ((nhdsWithin c {c}ᶜ).limUnder f)) (insert c s)
Sources
MathlibComplex.differentiableOn_update_limUnder_insert_of_isLittleO
Uses 7 · Used by 2
Statement usesCompleteness · Complex number · Euclidean affine space · Holomorphic functions · Normed vector space over a normed field
Proof usesAnalytic function · Cauchy formulas
Used bySchwarz lemma · Borel–Carathéodory theorem

TheoremPhragmen-Lindelöf principle#

Phragmen-Lindelöf principle in a strip U = {z : ℂ | a < im z < b}. Let f : ℂ → E be a function such that

  • f is differentiable on U and is continuous on its closure;
  • ‖f z‖ is bounded from above by A * exp(B * exp(c * |re z|)) on U for some c < π / (b - a);
  • ‖f z‖ is bounded from above by a constant C on the boundary of U.

Then ‖f z‖ is bounded by the same constant on the closed strip {z : ℂ | a ≤ im z ≤ b}. Moreover, it suffices to verify the second assumption only for sufficiently large values of |re z|.

PhragmenLindelof.horizontal_strip.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  {a b C : ℝ} {f : ℂ → E} {z : ℂ} (hfd : DiffContOnCl ℂ f (Complex.im ⁻¹' Set.Ioo a b))
  (hB :
    ∃ c < Real.pi / (b - a),
      ∃ B,
        f =O[Filter.comap (abs ∘ Complex.re) Filter.atTop ⊓
            Filter.principal (Complex.im ⁻¹' Set.Ioo a b)]
          fun z => Real.exp (B * Real.exp (c * |z.re|)))
  (hle_a : ∀ (z : ℂ), z.im = a → ‖f z‖ ≤ C) (hle_b : ∀ (z : ℂ), z.im = b → ‖f z‖ ≤ C)
  (hza : a ≤ z.im) (hzb : z.im ≤ b) : ‖f z‖ ≤ C
Sources
MathlibPhragmenLindelof.horizontal_strip
Uses 6 · Used by 1
Statement usesClosure · Cos (extension of trigonometric functions to the complex plane) · Exponential · Holomorphic functions · Inner product space, over \(R\) or \(C\)
Proof usesCauchy integral formula
Used byHadamard three-lines theorem

TheoremFundamental theorem of algebra#

Fundamental theorem of algebra: the field ℂ of complex numbers is algebraically closed.

Complex.isAlgClosed : IsAlgClosed ℂ
Sources
MathlibComplex.isAlgClosed
Uses 3 · Used by 4
Statement usesAlgebraically closed field · Field \(\C\) of complex numbers
Proof uses\(\C\) is algebraically closed
Used byInsolvability of General Higher Degree Equations (Abel-Ruffini Theorem) · Dirichlet’s Theorem · Gauss–Lucas theorem · Gelfand–Mazur theorem

TheoremFirst Main Theorem of Value Distribution Theory#

First part of the First Main Theorem, quantitative version: If f is meromorphic on the complex plane, then the difference between the characteristic functions of f and f⁻¹ is bounded by an explicit constant.

ValueDistribution.characteristic_sub_characteristic_inv_le {f : ℂ → ℂ} {R : ℝ}
  (hf : Meromorphic f) :
  |ValueDistribution.characteristic f ⊤ R - ValueDistribution.characteristic f⁻¹ ⊤ R| ≤
    max |Real.log ‖f 0‖| |Real.log ‖meromorphicTrailingCoeffAt f 0‖|
Sources
MathlibValueDistribution.characteristic_sub_characteristic_inv_le
Uses 8
Statement usesAnalytic function · Bochner integral · Carathéodory's theorem (measure theory) · Compactness in terms of filters · Cos (extension of trigonometric functions to the complex plane) · Lebesgue measure (Measures and integral calculus) · Logarithm
Proof usesCompleteness of R

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.