Hartogs extension theorem

TheoremHolomorphic functions on open subsets of ℂⁿ have continuous derivative#✓fully proved

Let \(n \in \mathbb{N}\), let \(s\) be an open subset of \(\mathbb{C}^n\) and let \(f : \mathbb{C}^n \to \mathbb{C}\) be complex differentiable at every point of \(s\). Then the complex derivative \(x \mapsto Df(x)\), with values in the complex linear maps \(\mathbb{C}^n \to \mathbb{C}\), is continuous on \(s\). Here \(\mathbb{C}^n\) carries the Euclidean norm.

theorem continuousOn_fderiv_of_differentiableOn
    {n : ℕ} {s : Set (EuclideanSpace ℂ (Fin n))}
    {f : EuclideanSpace ℂ (Fin n) → ℂ} (hs : IsOpen s)
    (hf : DifferentiableOn ℂ f s) : ContinuousOn (fderiv ℂ f) s

Used by 1

Used byHartogs extension theorem

DefinitionThe Wirtinger derivative with respect to z̄#✓fully proved

For \(f : \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\), the Wirtinger derivative of \(f\) at \(z\) is \(\frac{\partial f}{\partial \bar z}(z) = \frac{1}{2}\bigl(Df(z)(1) + i\,Df(z)(i)\bigr)\), where \(Df(z)\) is the real derivative of \(f\) at \(z\), taken to be \(0\) when \(f\) is not real differentiable at \(z\). When \(f\) is real differentiable at \(z\), this equals \(\frac{1}{2}\bigl(\frac{\partial f}{\partial x}(z) + i\,\frac{\partial f}{\partial y}(z)\bigr)\).

noncomputable def barDeriv (f : ℂ → ℂ) (z : ℂ) : ℂ :=
  (2 : ℂ)⁻¹ * (fderiv ℝ f z 1 + Complex.I * fderiv ℝ f z Complex.I)

Used by 4

Used byVanishing of the Wirtinger derivative at points of complex differentiability · Cauchy–Riemann criterion for complex differentiability · Solving the ∂̄-equation for compactly supported C¹ data · Hartogs extension theorem

TheoremVanishing of the Wirtinger derivative at points of complex differentiability#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\). If \(f\) is complex differentiable at \(z\), then the Wirtinger derivative \(\partial f / \partial \bar z\) of \(f\) vanishes at \(z\).

theorem barDeriv_eq_zero_of_differentiableAt
    {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℂ f z) : barDeriv f z = 0

Uses 1

Statement usesThe Wirtinger derivative with respect to z̄

TheoremCauchy–Riemann criterion for complex differentiability#✓fully proved

Let \(f : \mathbb{C} \to \mathbb{C}\) and \(z \in \mathbb{C}\). If \(f\) is real differentiable at \(z\) and its Wirtinger derivative \(\partial f / \partial \bar z\) vanishes at \(z\), then \(f\) is complex differentiable at \(z\).

theorem differentiableAt_of_barDeriv_eq_zero
    {f : ℂ → ℂ} {z : ℂ} (hf : DifferentiableAt ℝ f z)
    (hbar : barDeriv f z = 0) : DifferentiableAt ℂ f z

Uses 1 · Used by 1

Statement usesThe Wirtinger derivative with respect to z̄

Used byHartogs extension theorem

TheoremSolving the ∂̄-equation for compactly supported C¹ data#✓fully proved

Let \(g : \mathbb{C} \to \mathbb{C}\) be real differentiable on all of \(\mathbb{C}\), with continuous real derivative and compact support. Then there is a function \(u : \mathbb{C} \to \mathbb{C}\), real differentiable on all of \(\mathbb{C}\), whose Wirtinger derivative satisfies \(\frac{\partial u}{\partial \bar z}(z) = g(z)\) for every \(z \in \mathbb{C}\).

theorem exists_differentiable_barDeriv_eq_of_hasCompactSupport
    {g : ℂ → ℂ} (hg : Differentiable ℝ g) (hDg : Continuous (fderiv ℝ g))
    (hgc : HasCompactSupport g) :
    ∃ u : ℂ → ℂ, Differentiable ℝ u ∧ ∀ z, barDeriv u z = g z

Uses 1

Statement usesThe Wirtinger derivative with respect to z̄

TheoremHartogs extension theorem#✓fully proved

Let \(n \ge 2\), let \(U \subseteq \mathbb{C}^n\) be open and connected, and let \(K \subseteq U\) be compact with \(U \setminus K\) connected. Then for every function \(f : \mathbb{C}^n \to \mathbb{C}\) that is holomorphic on \(U \setminus K\) there is a function \(F : \mathbb{C}^n \to \mathbb{C}\) that is holomorphic on \(U\) and agrees with \(f\) on \(U \setminus K\). Here \(\mathbb{C}^n\) carries the Euclidean norm.

Proof: The compactly supported Cauchy–Green equation in one coordinate, combined with a smooth cutoff and one-variable identity continuation.

theorem hartogs_extension
    {n : ℕ} (hn : 2 ≤ n)
    {U : Set (EuclideanSpace ℂ (Fin n))} (hU_open : IsOpen U) (hU_conn : IsConnected U)
    {K : Set (EuclideanSpace ℂ (Fin n))} (hK_compact : IsCompact K) (hKU : K ⊆ U)
    (hUK_conn : IsConnected (U \ K))
    {f : EuclideanSpace ℂ (Fin n) → ℂ} (hf : DifferentiableOn ℂ f (U \ K)) :
    ∃ F : EuclideanSpace ℂ (Fin n) → ℂ, DifferentiableOn ℂ F U ∧ Set.EqOn F f (U \ K)

Sources

• Hartogs extension phenomenon, F. Hartogs, Math. Ann. 62 (1906); see Hörmander, An Introduction to Complex Analysis in Several Variables; Lean is ℂⁿ n ≥ 2 finite-dimensional form via EuclideanSpace ℂ (Fin n) with U open connected K compact U\K connected.

Uses 3

Proof usesThe Wirtinger derivative with respect to z̄ · Holomorphic functions on open subsets of ℂⁿ have continuous derivative · Cauchy–Riemann criterion for complex differentiability

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.