Functions on one complex variable

DefinitionHolomorphic functions#

DifferentiableOn 𝕜 f s means that f is differentiable within s at any point of s.

DifferentiableOn.{u_1, u_2, u_3} (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2}
  [AddCommGroup E] [_root_.Module 𝕜 E] [TopologicalSpace E] {F : Type u_3} [AddCommGroup F]
  [_root_.Module 𝕜 F] [TopologicalSpace F] (f : E → F) (s : Set E) : Prop

Sources

• Mathlib documentation: DifferentiableOn
• Source of DifferentiableOn in Mathlib/Analysis/Calculus/FDeriv/Defs.lean
• Mathlib undergraduate list: Single Variable Complex Analysis › Functions on one complex variable
• Mathlib undergraduate list: Multivariable calculus › Differential calculus

MathlibDifferentiableOn

Uses 2 · Used by 19

Statement usesContinuous linear map · Metric space

Used byThe Mean Value Theorem (Freek Wiedijk's 100 theorems) · Analyticity of holomorphic functions · Cauchy integral formula · Liouville theorem · Phragmen-Lindelöf principle · Removable singularity · Schwarz lemma · Characterization of convexity · Mean value theorem (Differentiability) · Change of variables formula · Regularization by convolution · Darboux's theorem (analysis) · Borel–Carathéodory theorem · Hadamard three-lines theorem · Morera's theorem · Akra–Bazzi theorem · Differentiability with respect to the complex variable · Holomorphic stability under uniform convergence · Taylor's theorem with Lagrange form for remainder

TheoremCauchy formulas#

Cauchy integral formula: if f : ℂ → E is continuous on a closed disc of radius R and is complex differentiable at all but countably many points of its interior, then for any w in this interior we have \(\frac{1}{2πi}\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=f(w)\).

Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable.{u}
  {E : Type u} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ}
  {f : ℂ → E} {s : Set ℂ} (hs : s.Countable) (hw : w ∈ Metric.ball c R)
  (hc : ContinuousOn f (Metric.closedBall c R))
  (hd : ∀ x ∈ Metric.ball c R \ s, DifferentiableAt ℂ f x) :
  (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = f w

Sources

• Mathlib documentation: Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable
• Source of Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable in Mathlib/Analysis/Complex/CauchyIntegral.lean
• Mathlib undergraduate list: Single Variable Complex Analysis › Functions on one complex variable

MathlibComplex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable

Uses 21 · Used by 4

Statement usesBall · Bochner integral · Carathéodory's theorem (measure theory) · Cos (extension of trigonometric functions to the complex plane) · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Lebesgue measure (Measures and integral calculus)

Proof usesAffine space · Cardinal · Characteristic zero · Completeness of R · Continuity (Complex-valued series) · Derivative of a composition of functions (Analysis) · Differentiable functions · Divergence theorem · Euclidean domain · Field \(\C\) of complex numbers · Homeomorphisms · Logarithm · Product of vector spaces · The Binomial Theorem

Used byAnalyticity of holomorphic functions · Cauchy integral formula · Liouville theorem · Removable singularity

• Analyticity of a holomorphic function
• Principle of isolated zeros
• Principle of analytic continuation
• Maximum principle

TheoremHolomorphic stability under uniform convergence#

A locally uniform limit of holomorphic functions on an open domain of the complex plane is holomorphic (the derivatives converge locally uniformly to that of the limit, which is proved as TendstoLocallyUniformlyOn.deriv).

TendstoLocallyUniformlyOn.differentiableOn.{u_1, u_2} {E : Type u_1} {ι : Type u_2}
  [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {φ : Filter ι} {F : ι → ℂ → E} {f : ℂ → E}
  [CompleteSpace E] [φ.NeBot] (hf : TendstoLocallyUniformlyOn F f φ U)
  (hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : DifferentiableOn ℂ f U

Sources

• Mathlib documentation: TendstoLocallyUniformlyOn.differentiableOn
• Source of TendstoLocallyUniformlyOn.differentiableOn in Mathlib/Analysis/Complex/LocallyUniformLimit.lean
• Mathlib undergraduate list: Single Variable Complex Analysis › Functions on one complex variable

MathlibTendstoLocallyUniformlyOn.differentiableOn

Uses 18

Statement usesCompleteness · Complex number · Holomorphic functions · Normed vector space over a normed field

Proof usesBall · Bochner integral · Carathéodory's theorem (measure theory) · Characteristic zero · Cos (extension of trigonometric functions to the complex plane) · Derivative at a point · Differentiable function between normed vector spaces · Differentials (linear tangent functions) · Euclidean domain · Extreme value theorem · Field \(\C\) of complex numbers · Lebesgue measure (Measures and integral calculus) · Ordered ring · Topological ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.