Newlander–Nirenberg theorem

AbbreviationModel space \(\mathbb{R}^{2n}\) for the Newlander–Nirenberg theorem#✓fully proved

For a natural number \(n\), \(E_n\) is the Euclidean space \(\mathbb{R}^{2n}\), the model space carrying the almost complex structure.

abbrev E (n : ℕ) := EuclideanSpace ℝ (Fin (2 * n))

Used by 4

Used byAlmost complex structure on a subset of \(\mathbb{R}^{2n}\) · Newlander–Nirenberg theorem · Nijenhuis tensor · Vanishing of the Nijenhuis tensor on a set

DefinitionNijenhuis tensor#✓fully proved

Let \(n\) be a natural number, let \(J\) assign to each point \(y \in \mathbb{R}^{2n}\) a real linear map \(J(y) : \mathbb{R}^{2n} \to \mathbb{R}^{2n}\), and let \(V, W : \mathbb{R}^{2n} \to \mathbb{R}^{2n}\) be vector fields. Write \(JV\) for the vector field \(y \mapsto J(y)V(y)\) and \([V, W]\) for the Lie bracket of vector fields. The Nijenhuis tensor of \(J\) at a point \(x \in \mathbb{R}^{2n}\) is

\[N(V, W)(x) = [JV, JW](x) - J(x)[JV, W](x) - J(x)[V, JW](x) - [V, W](x).\]

For an almost complex structure the last term is \(J^2[V, W]\), so this is the usual torsion of \(J\). When \(J\) is an almost complex structure on an open set \(U \subseteq \mathbb{R}^{2n}\), the expression is \(C^\infty(U)\)-bilinear in \(V\) and \(W\) on \(U\): the terms involving the derivatives of \(V\) and \(W\) cancel using \(J^2 = -1\), so the value at a point \(x\) of \(U\) depends only on \(V(x)\), \(W(x)\) and the derivative of \(J\) there.

noncomputable def nijenhuis {n : ℕ} (J : E n → E n →L[ℝ] E n)
    (V W : E n → E n) (x : E n) : E n :=
  VectorField.lieBracket ℝ (fun y ↦ J y (V y)) (fun y ↦ J y (W y)) x
    - J x (VectorField.lieBracket ℝ (fun y ↦ J y (V y)) W x)
    - J x (VectorField.lieBracket ℝ V (fun y ↦ J y (W y)) x)
    - VectorField.lieBracket ℝ V W x

Uses 1 · Used by 1

Statement usesModel space \(\mathbb{R}^{2n}\) for the Newlander–Nirenberg theorem

Used byVanishing of the Nijenhuis tensor on a set

DefinitionAlmost complex structure on a subset of \(\mathbb{R}^{2n}\)#✓fully proved

Let \(n\) be a natural number, let \(U \subseteq \mathbb{R}^{2n}\) and let \(J\) assign to each point \(y \in \mathbb{R}^{2n}\) a real linear map \(J(y) : \mathbb{R}^{2n} \to \mathbb{R}^{2n}\). Then \(J\) is an almost complex structure on \(U\) if \(J\) is \(C^\infty\) on \(U\) and \(J(x)(J(x)v) = -v\) for every \(x \in U\) and every \(v \in \mathbb{R}^{2n}\).

def IsAlmostComplexOn {n : ℕ} (J : E n → E n →L[ℝ] E n) (U : Set (E n)) : Prop :=
  ContDiffOn ℝ ∞ J U ∧ ∀ x ∈ U, ∀ v : E n, J x (J x v) = -v

Uses 1 · Used by 1

Statement usesModel space \(\mathbb{R}^{2n}\) for the Newlander–Nirenberg theorem

Used byNewlander–Nirenberg theorem

DefinitionVanishing of the Nijenhuis tensor on a set#✓fully proved

Let \(n\) be a natural number, let \(U \subseteq \mathbb{R}^{2n}\), let \(J\) assign to each point \(y \in \mathbb{R}^{2n}\) a real linear map \(J(y) : \mathbb{R}^{2n} \to \mathbb{R}^{2n}\), and write \(N\) for the Nijenhuis tensor of \(J\). The Nijenhuis tensor of \(J\) vanishes on \(U\) if \(N(V, W)(x) = 0\) for all \(C^\infty\) vector fields \(V, W : \mathbb{R}^{2n} \to \mathbb{R}^{2n}\) and every \(x \in U\).

The vector fields range over globally smooth fields, which is the textbook hypothesis. Whenever \(U\) is open and \(J\) is an almost complex structure on \(U\) this is equivalent to the pointwise condition: the tensor is bilinear over functions, and constant vector fields already realize every pair of tangent vectors.

def NijenhuisVanishesOn {n : ℕ} (J : E n → E n →L[ℝ] E n) (U : Set (E n)) : Prop :=
  ∀ V W : E n → E n, ContDiff ℝ ∞ V → ContDiff ℝ ∞ W →
    ∀ x ∈ U, nijenhuis J V W x = 0

Uses 2 · Used by 1

Statement usesModel space \(\mathbb{R}^{2n}\) for the Newlander–Nirenberg theorem · Nijenhuis tensor

Used byNewlander–Nirenberg theorem

TheoremNewlander–Nirenberg theorem#●ready to prove

Let \(n\) be a natural number, let \(U \subseteq \mathbb{R}^{2n}\) be open and let \(J\) be an almost complex structure on \(U\) whose Nijenhuis tensor vanishes on \(U\). Then every \(x \in U\) has holomorphic coordinates for \(J\): there are open sets \(S \subseteq \mathbb{R}^{2n}\) and \(T \subseteq \mathbb{C}^n\) with \(x \in S \subseteq U\) and a homeomorphism \(\varphi : S \to T\) such that \(\varphi\) is \(C^\infty\) on \(S\), \(\varphi^{-1}\) is \(C^\infty\) on \(T\) (both as maps of real vector spaces), and for every \(y \in S\) and every \(v \in \mathbb{R}^{2n}\) the real derivative of \(\varphi\) satisfies \(D\varphi(y)(J(y)v) = i \, D\varphi(y)v\).

public theorem_wanted newlander_nirenberg {n : ℕ} {U : Set (E n)} (_hU : IsOpen U)
    (J : E n → E n →L[ℝ] E n) (_hJ : IsAlmostComplexOn J U)
    (_hN : NijenhuisVanishesOn J U) {x : E n} (_hx : x ∈ U) :
    ∃ φ : OpenPartialHomeomorph (E n) (EuclideanSpace ℂ (Fin n)),
      x ∈ φ.source ∧ φ.source ⊆ U ∧
      ContDiffOn ℝ ∞ (φ : E n → EuclideanSpace ℂ (Fin n)) φ.source ∧
      ContDiffOn ℝ ∞ (φ.symm : EuclideanSpace ℂ (Fin n) → E n) φ.target ∧
      ∀ y ∈ φ.source, ∀ v : E n,
        fderiv ℝ (φ : E n → EuclideanSpace ℂ (Fin n)) y (J y v)
          = Complex.I • fderiv ℝ (φ : E n → EuclideanSpace ℂ (Fin n)) y v

Sources

• A. Newlander and L. Nirenberg, Complex analytic coordinates in almost complex manifolds, Annals of Math, 65 (3) 1957, 391-404. Problem newlander_nirenberg of the lean-eval benchmark.

Uses 3

Statement usesModel space \(\mathbb{R}^{2n}\) for the Newlander–Nirenberg theorem · Almost complex structure on a subset of \(\mathbb{R}^{2n}\) · Vanishing of the Nijenhuis tensor on a set

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.