Several complex variables

Holomorphic functions on C^n: Hartogs extension and separate analyticity, Weierstrass preparation, complex Hessians.

• Complex Hessian
• Hartogs extension theorem
• Hartogs' theorem on separate analyticity

TheoremWeierstrass preparation theorem#✓fully proved

Let \(E\) be a finite-dimensional normed vector space over \(\mathbb{C}\) and let \(f : E \times \mathbb{C} \to \mathbb{C}\) be analytic at \(0\). Suppose that for some \(d \in \mathbb{N}\) and some \(g : \mathbb{C} \to \mathbb{C}\) analytic at \(0\) with \(g(0) \ne 0\), \(f(0, w) = w^d g(w)\) for all \(w\) in a neighbourhood of \(0\). Then there are functions \(a_0, \dots, a_{d-1} : E \to \mathbb{C}\), each analytic at \(0\) with \(a_j(0) = 0\), a function \(u : E \times \mathbb{C} \to \mathbb{C}\) analytic at \(0\) with \(u(0) \ne 0\), and an open set \(U \subseteq E \times \mathbb{C}\) containing \(0\) such that \(f(z, w) = u(z, w) \bigl(w^d + \sum_{j=0}^{d-1} a_j(z) w^j\bigr)\) for all \((z, w) \in U\).

public theorem weierstrass_preparation
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E]
    {f : E × ℂ → ℂ} (hf : AnalyticAt ℂ f (0 : E × ℂ))
    {d : ℕ} {g : ℂ → ℂ} (hg : AnalyticAt ℂ g (0 : ℂ)) (hg0 : g (0 : ℂ) ≠ 0)
    (h_order : ∀ᶠ w in 𝓝 (0 : ℂ), f ((0 : E), w) = w ^ d * g w) :
    ∃ (a : Fin d → E → ℂ) (u : E × ℂ → ℂ),
      (∀ j, AnalyticAt ℂ (a j) (0 : E)) ∧
      (∀ j, a j (0 : E) = 0) ∧
      AnalyticAt ℂ u (0 : E × ℂ) ∧ u (0 : E × ℂ) ≠ 0 ∧
      ∃ U : Set (E × ℂ), IsOpen U ∧ (0 : E × ℂ) ∈ U ∧
        ∀ p ∈ U, f p = u p * (p.2 ^ d + ∑ j : Fin d, a j p.1 * p.2 ^ (j : ℕ))

Sources

• Weierstrass preparation theorem in several complex variables; see Hörmander; Lean is finite-dimensional E × ℂ product form, order d slice factorization w^d g w, Weierstrass polynomial with vanishing coefficients and unit u, local open U, fixed field ℂ specialization.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.