Contour integrals and antiderivatives

TheoremFundamental theorem of contour integration#●ready to prove

Let \(U \subseteq \mathbb{C}\) be open and let \(F, f : \mathbb{C} \to \mathbb{C}\) be such that \(F\) is complex-differentiable at every \(z \in U\) with \(F'(z) = f(z)\). Let \(\gamma : [0, 1] \to \mathbb{C}\) be a path from \(a\) to \(b\) whose image lies in \(U\) and which is continuously differentiable on \([0, 1]\), with derivative \(\gamma'\) (one-sided at the endpoints). If \(t \mapsto f(\gamma(t))\,\gamma'(t)\) is integrable on \([0, 1]\), then \(\int_\gamma f(z)\,dz = F(b) - F(a)\), where \(\int_\gamma f(z)\,dz = \int_0^1 f(\gamma(t))\,\gamma'(t)\,dt\).

theorem_wanted contourIntegral_of_hasDerivAt
    {F f : ℂ → ℂ} {a b : ℂ} {γ : Path a b} {U : Set ℂ}
    (hU : IsOpen U) (hγU : Set.range γ ⊆ U)
    (hF : ∀ z ∈ U, HasDerivAt F (f z) z)
    (hγ : ContDiffOn ℝ 1 γ.extend (Set.Icc 0 1))
    (h_int : CurveIntegrable (fun z => f z • ContinuousLinearMap.id ℂ ℂ) γ) :
    curveIntegral (fun z => f z • ContinuousLinearMap.id ℂ ℂ) γ = F b - F a

Sources

• L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4, §1.1 to §1.3 (line integrals).

TheoremML estimate for contour integrals#●ready to prove

Let \(f : \mathbb{C} \to \mathbb{C}\) and let \(\gamma : [0, 1] \to \mathbb{C}\) be a path from \(a\) to \(b\) which is continuously differentiable on \([0, 1]\), with derivative \(\gamma'\) (one-sided at the endpoints). Let \(M\) and \(L\) be real numbers with \(|f(\gamma(t))| \le M\) and \(|\gamma'(t)| \le L\) for every \(t \in [0, 1]\). If \(t \mapsto f(\gamma(t))\,\gamma'(t)\) is integrable on \([0, 1]\), then \(\left|\int_\gamma f(z)\,dz\right| \le ML\), where \(\int_\gamma f(z)\,dz = \int_0^1 f(\gamma(t))\,\gamma'(t)\,dt\).

The parameter interval has length one, so \(L\) bounds the length of \(\gamma\).

theorem_wanted norm_contourIntegral_le
    {f : ℂ → ℂ} {a b : ℂ} {γ : Path a b} {M L : ℝ}
    (hγ : ContDiffOn ℝ 1 γ.extend (Set.Icc 0 1))
    (hf : ∀ t ∈ Set.Icc (0 : ℝ) 1, ‖f (γ.extend t)‖ ≤ M)
    (hγ' : ∀ t ∈ Set.Icc (0 : ℝ) 1, ‖derivWithin γ.extend (Set.Icc 0 1) t‖ ≤ L)
    (h_int : CurveIntegrable (fun z => f z • ContinuousLinearMap.id ℂ ℂ) γ) :
    ‖curveIntegral (fun z => f z • ContinuousLinearMap.id ℂ ℂ) γ‖ ≤ M * L

Sources

• L. V. Ahlfors, Complex Analysis, 3rd ed., Ch. 4, §1.1 to §1.3 (line integrals).

TheoremThe reciprocal function has no antiderivative on an annulus#●ready to prove

Let \(U = \{z \in \mathbb{C} : 1 < |z| < 2\}\). There is no function \(F : \mathbb{C} \to \mathbb{C}\) that is complex differentiable at every \(z \in U\) with \(F'(z) = 1/z\).

public theorem_wanted not_exists_hasDerivAt_inv_on_annulus (U : Set ℂ)
  (hU : U = {z : ℂ | 1 < norm z ∧ norm z < 2}) :
  ¬ ∃ F : ℂ → ℂ, ∀ z ∈ U, HasDerivAt F (1 / z) z

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Functions of a complex variable; General properties of functions of one complex variable), problem ma_proofbench_l1_67.

3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.