30 Functions of a complex variable

TheoremBorel–Carathéodory theorem#

Borel-Carathéodory theorem.

If f is analytic on the open ball ‖z‖ < R and satisfies (f z).re ≤ M for all such z, then ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖) for all ‖z‖ < R.

Complex.borelCaratheodory {f : ℂ → ℂ} {M R : ℝ} {z : ℂ} (hM : 0 < M)
  (hf : DifferentiableOn ℂ f (Metric.ball 0 R))
  (hf₁ : Set.MapsTo f (Metric.ball 0 R) {z | z.re ≤ M}) (hR : 0 < R) (hz : z ∈ Metric.ball 0 R) :
  ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
Sources
MathlibComplex.borelCaratheodory
Uses 5
Statement usesBall · Complex number · Holomorphic functions
Proof usesRemovable singularity · The Triangle Inequality

TheoremCauchy–Hadamard theorem#

The Cauchy-Hadamard theorem for formal multilinear series: The inverse of the radius is equal to \(\limsup_{n\to\infty} \sqrt[n]{‖p n‖}\).

FormalMultilinearSeries.radius_inv_eq_limsup.{u_1, u_2, u_3} {𝕜 : Type u_1}
  [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3}
  [NormedAddCommGroup F] [NormedSpace 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) :
  p.radius⁻¹ = Filter.limsup (fun n => ↑(‖p n‖₊ ^ (1 / ↑n))) Filter.atTop
Sources
MathlibFormalMultilinearSeries.radius_inv_eq_limsup
Uses 4
Statement usesRadius of convergence
Proof usesField \(\R\) of real numbers · Ordered ring · Topology on a normed vector space

TheoremGauss–Lucas theorem#

Mathlib records this with 2 declarations.

Polynomial.rootSet_derivative_subset_convexHull_rootSet: Gauss-Lucas Theorem: if \(P\) is a nonconstant polynomial with complex coefficients, then all zeros of \(P'\) belong to the convex hull of the set of zeros of \(P\).

See also eq_centerMass_of_eval_derivative_eq_zero for a version that provides explicit coefficients of the convex combination.

Polynomial.rootSet_derivative_subset_convexHull_rootSet {P : Polynomial ℂ} (h₀ : 0 < P.degree) :
  (Polynomial.derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)

Polynomial.eq_centerMass_of_eval_derivative_eq_zero: Gauss-Lucas Theorem: if \(P\) is a nonconstant polynomial with complex coefficients, then all zeros of \(P'\) belong to the convex hull of the set of zeros of \(P\).

This version provides explicit formulas for the coefficients of the convex combination. See also rootSet_derivative_subset_convexHull_rootSet below.

Polynomial.eq_centerMass_of_eval_derivative_eq_zero {P : Polynomial ℂ} {z : ℂ} (hP : 0 < P.degree)
  (hz : Polynomial.eval z (Polynomial.derivative P) = 0) :
  z = P.roots.toFinset.centerMass (P.derivRootWeight z) id
Sources
MathlibPolynomial.rootSet_derivative_subset_convexHull_rootSet · Polynomial.eq_centerMass_of_eval_derivative_eq_zero
Uses 6
Statement usesConvex hull of a subset of an affine real space · Field \(\C\) of complex numbers · Inner product space, over \(R\) or \(C\) · Polynomial derivative · Roots of a polynomial
Proof usesFundamental theorem of algebra

TheoremHadamard three-lines theorem#

Hadamard three-line theorem: If f is a bounded function, continuous on the closed strip re ⁻¹' [l, u] and differentiable on open strip re ⁻¹' (l, u), then for M(x) := sup ((norm ∘ f) '' re ⁻¹' {x}) we have that for all z in the closed strip re ⁻¹' [a,b] the inequality ‖f(z)‖ ≤ M(0) ^ (1 - ((z.re - l) / (u - l))) * M(1) ^ ((z.re - l) / (u - l)) holds.

Complex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {l u : ℝ} (hul : l < u) {f : ℂ → E} {z : ℂ}
  (hz : z ∈ Complex.HadamardThreeLines.verticalClosedStrip l u)
  (hd : DiffContOnCl ℂ f (Complex.HadamardThreeLines.verticalStrip l u))
  (hB : BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip l u)) :
  ‖f z‖ ≤ ‖Complex.HadamardThreeLines.interpStrip' f l u z‖
Sources
MathlibComplex.HadamardThreeLines.norm_le_interpStrip_of_mem_verticalClosedStrip
Uses 6
Statement usesClosure · Complex number · Holomorphic functions · Inner product space, over \(R\) or \(C\)
Proof usesCharacteristic p · Phragmen-Lindelöf principle

TheoremMellin inversion theorem#

The inverse Mellin transform of the Mellin transform applied to x > 0 is x.

mellinInv_mellin_eq.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E]
  (σ : ℝ) (f : ℝ → E) {x : ℝ} (hx : 0 < x) (hf : MellinConvergent f ↑σ)
  (hFf : Complex.VerticalIntegrable (mellin f) σ MeasureTheory.volume) (hfx : ContinuousAt f x) :
  mellinInv σ (mellin f) x = f x
Sources
MathlibmellinInv_mellin_eq
Uses 9
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Cos (extension of trigonometric functions to the complex plane) · Lebesgue measure (Measures and integral calculus)
Proof usesChange of variables formula · Derivative at a point · Fourier theorem · Inverse trigonometric functions · Logarithm

TheoremMorera's theorem#

Mathlib states this as Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn.

Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn.{u_1} {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {U : Set ℂ}
  (hU : IsOpen U) : Complex.IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U
Sources
MathlibComplex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn
Uses 9
Statement usesBochner integral · Carathéodory's theorem (measure theory) · Complex number · Holomorphic functions · Lebesgue measure (Measures and integral calculus)
Proof usesAnalyticity of holomorphic functions · Derivative at a point · Fundamental Theorem of Integral Calculus · The Triangle Inequality

TheoremOpen mapping theorem (complex analysis)#

The open mapping theorem for holomorphic functions, global version: if a function g : E → ℂ is analytic on a connected set U, then either it is constant on U, or it is open on U (in the sense that it maps any open set contained in U to an open set in ℂ).

AnalyticOnNhd.is_constant_or_isOpen.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E]
  {U : Set E} {g : E → ℂ} (hg : AnalyticOnNhd ℂ g U) (hU : IsPreconnected U) :
  (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)
Sources
MathlibAnalyticOnNhd.is_constant_or_isOpen
Uses 8
Statement usesAnalytic function · Complex number · Inner product space, over \(R\) or \(C\)
Proof usesAnalyticity of holomorphic functions · Convex subsets · Extreme value theorem · Maximum modulus principle · Principle of analytic continuation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.