def ConvergesLocallyUniformlyOn (F : ℕ → ℂ → ℂ) (f : ℂ → ℂ) (S : Set ℂ) : Prop

def ConvergesNormallyOn (f : ℕ → ℂ → ℂ) (S : Set ℂ) : Prop

def ConvergesLocallyNormallyOn (f : ℕ → ℂ → ℂ) (S : Set ℂ) : Prop

theorem weierstrass_m_test_deriv_normally_convergent {f : ℕ → ℂ → ℂ} {S : Set ℂ} (hS : IsOpen S) (hf_holo : ∀ (n : ℕ), DifferentiableOn ℂ (f n) S) (hf_conv : ConvergesLocallyNormallyOn f S) : ConvergesLocallyNormallyOn (fun (n : ℕ) (z : ℂ) => deriv (f n) z) S

theorem weierstrass_m_test_deriv {f : ℕ → ℂ → ℂ} {S : Set ℂ} (hS : IsOpen S) (hf_holo : ∀ (n : ℕ), DifferentiableOn ℂ (f n) S) (hf_conv : ConvergesLocallyNormallyOn f S) : ConvergesLocallyNormallyOn (fun (n : ℕ) (z : ℂ) => deriv (f n) z) S ∧ ∀ z ∈ S, HasDerivAt (fun (z : ℂ) => ∑' (n : ℕ), f n z) (∑' (n : ℕ), deriv (f n) z) z

structure ParameterizedCurve : Type

• toFun : ℝ → ℂ
• a : ℝ
• b : ℝ
• hab : self.a ≤ self.b
• continuous_on : ContinuousOn self.toFun (Set.Icc self.a self.b)

@[implicit_reducible]

instance instCoeFunParameterizedCurveForallRealComplex : CoeFun ParameterizedCurve fun (x : ParameterizedCurve) => ℝ → ℂ

def ParameterizedCurve.IsClosed (γ : ParameterizedCurve) : Prop

def ParameterizedCurve.IsSimple (γ : ParameterizedCurve) : Prop

noncomputable def contourIntegral (f : ℂ → ℂ) (γ : ParameterizedCurve) : ℂ

theorem contourIntegral_reparam_invariance (f : ℂ → ℂ) (γ₁ γ₂ : ParameterizedCurve) (φ φ' : ℝ → ℝ) (hcomp : ∀ t ∈ Set.Icc γ₂.a γ₂.b, γ₂.toFun t = γ₁.toFun (φ t)) (hφa : φ γ₂.a = γ₁.a) (hφb : φ γ₂.b = γ₁.b) (hφ_deriv : ∀ t ∈ Set.uIcc γ₂.a γ₂.b, HasDerivAt φ (φ' t) t) (hφ'_cont : ContinuousOn φ' (Set.uIcc γ₂.a γ₂.b)) (hchain : ∀ t ∈ Set.Icc γ₂.a γ₂.b, deriv γ₂.toFun t = ↑(φ' t) * deriv γ₁.toFun (φ t)) (hg_cont : ContinuousOn (fun (u : ℝ) => f (γ₁.toFun u) * deriv γ₁.toFun u) (φ '' Set.uIcc γ₂.a γ₂.b)) : contourIntegral f γ₂ = contourIntegral f γ₁

theorem locallyUniformLimit_holomorphic {ι : Type u_1} {φ : Filter ι} [φ.NeBot] {F : ι → ℂ → ℂ} {f : ℂ → ℂ} {U : Set ℂ} (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : DifferentiableOn ℂ f U

theorem locallyUniformLimit_deriv_converges {ι : Type u_1} {φ : Filter ι} {F : ι → ℂ → ℂ} {f : ℂ → ℂ} {U : Set ℂ} (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) : TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U

theorem locallyUniformLimit_zero_free {ι : Type u_1} {φ : Filter ι} [φ.NeBot] {F : ι → ℂ → ℂ} {f : ℂ → ℂ} {U : Set ℂ} (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) (hUc : IsPreconnected U) (hFnz : ∀ᶠ (n : ι) in φ, ∀ z ∈ U, F n z ≠ 0) (hfnz : ∃ z ∈ U, f z ≠ 0) (z : ℂ) : z ∈ U → f z ≠ 0

theorem locallyUniformLimit_holomorphic_and_deriv_and_zeroFree {ι : Type u_1} {φ : Filter ι} [φ.NeBot] {F : ι → ℂ → ℂ} {f : ℂ → ℂ} {U : Set ℂ} (hf : TendstoLocallyUniformlyOn F f φ U) (hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U) (hU : IsOpen U) (hUc : IsPreconnected U) (hFnz : ∀ᶠ (n : ι) in φ, ∀ z ∈ U, F n z ≠ 0) (hfnz : ∃ z ∈ U, f z ≠ 0) : DifferentiableOn ℂ f U ∧ TendstoLocallyUniformlyOn (deriv ∘ F) (deriv f) φ U ∧ ∀ z ∈ U, f z ≠ 0

def ParameterizedCurve.image (γ : ParameterizedCurve) : Set ℂ

opaque ParameterizedCurve.curveInterior (γ : ParameterizedCurve) : Set ℂ

theorem ParameterizedCurve.curveInterior_disjoint_image (γ : ParameterizedCurve) : Disjoint γ.curveInterior γ.image

def ParameterizedCurve.ContainedIn (γ : ParameterizedCurve) (U : Set ℂ) : Prop

theorem cauchy_theorem (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f U) (γ : ParameterizedCurve) (hγ_simple : γ.IsSimple) (hγ_closed : γ.IsClosed) (hγ_contained : γ.ContainedIn U) : contourIntegral f γ = 0

theorem complex_ftc_contour (γ : ParameterizedCurve) {Ω : Set ℂ} {f : ℂ → ℂ} (hΩ : IsOpen Ω) (hγ_range : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t ∈ Ω) (hf : DifferentiableOn ℂ f Ω) (hγ_diff : ∀ t ∈ Set.uIcc γ.a γ.b, HasDerivAt γ.toFun (deriv γ.toFun t) t) (hint : IntervalIntegrable (fun (t : ℝ) => deriv f (γ.toFun t) * deriv γ.toFun t) MeasureTheory.volume γ.a γ.b) : contourIntegral (deriv f) γ = f (γ.toFun γ.b) - f (γ.toFun γ.a)

noncomputable def complexResidue (f : ℂ → ℂ) (z₀ : ℂ) : ℂ

theorem cauchy_residue_formula (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : MeromorphicOn f U) (γ : ParameterizedCurve) (hγ_closed : γ.IsClosed) (hγ_simple : γ.IsSimple) (hγ_in_U : γ.ContainedIn U) (poles : Finset ℂ) (hpoles_in_interior : ∀ z ∈ poles, z ∈ γ.curveInterior) (hpoles_off_curve : ∀ z ∈ poles, z ∉ γ.image) (hf_analytic : ∀ z ∈ U, z ∉ poles → AnalyticAt ℂ f z) : contourIntegral f γ = 2 * ↑Real.pi * Complex.I * ∑ z ∈ poles, complexResidue f z

theorem cauchy_residue_circle (f : ℂ → ℂ) (a : ℂ) (R : ℝ) (hR : 0 < R) (hf : DifferentiableOn ℂ f (Metric.closedBall a R)) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(a, R), (fun (w : ℂ) => f w / (w - a)) z = f a

theorem complexResidue_div_sub_eq (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f U) (a : ℂ) (ha : a ∈ U) : complexResidue (fun (w : ℂ) => f w / (w - a)) a = f a

theorem meromorphicOn_div_sub (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f U) (a : ℂ) (_ha : a ∈ U) : MeromorphicOn (fun (w : ℂ) => f w / (w - a)) U

theorem analyticAt_div_sub (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f U) (a z : ℂ) (hz : z ∈ U) (hza : z ≠ a) : AnalyticAt ℂ (fun (w : ℂ) => f w / (w - a)) z

theorem cauchy_integral_formula_general (U : Set ℂ) (hU : IsOpen U) (f : ℂ → ℂ) (hf : DifferentiableOn ℂ f U) (γ : ParameterizedCurve) (hγ_simple : γ.IsSimple) (hγ_closed : γ.IsClosed) (hγ_contained : γ.ContainedIn U) (a : ℂ) (ha : a ∈ γ.curveInterior) : f a = (2 * ↑Real.pi * Complex.I)⁻¹ * contourIntegral (fun (w : ℂ) => f w / (w - a)) γ

theorem liouville_theorem (f : ℂ → ℂ) (hf : Differentiable ℂ f) (hb : Bornology.IsBounded (Set.range f)) : ∃ (c : ℂ), ∀ (z : ℂ), f z = c

theorem morera_theorem {f : ℂ → ℂ} {U : Set ℂ} (hU : IsOpen U) (hf_cont : ContinuousOn f U) (hf_conservative : Complex.IsConservativeOn f U) : DifferentiableOn ℂ f U