class HasPositivity (α : Type u_1) [AddCommGroup α] [Module ℝ α] : Type u_1

A typeclass abstracting a notion of positivity on a real vector space: a predicate IsPositive closed under addition and positive scaling, with nonzero positive elements.

• IsPositive : α → Prop
• pos_add (a b : α) : IsPositive a → IsPositive b → IsPositive (a + b)
• pos_smul_pos (r : ℝ) (a : α) : 0 < r → IsPositive a → IsPositive (r • a)
• pos_nonzero (a : α) : IsPositive a → a ≠ 0

structure AlmostComplexStr {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] : Type u_2

An almost complex structure on the vector field space $VF$: an endomorphism $J : VF \to VF$ satisfying $J^2 = -\mathrm{id}$ (expressed dually as $\iota_{J(JX)} \alpha = -\iota_X \alpha$ on all $1$-forms $\alpha$).

• J : VF → VF
• sq_neg_id (X : VF) (α : Ω 1) : DifferentialFormSpace.ι (self.J (self.J X)) α = -DifferentialFormSpace.ι X α

structure IsCompatibleACS {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) : Prop

$J$ is compatible with the symplectic form $\omega$: $\omega(Ju, Jv) = \omega(u, v)$ (preservation) and the taming map $v \mapsto \omega(Jv, \cdot)$ is injective.

• preserves (u v : VF) : DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.ι (J.J v) S.ω) = DifferentialFormSpace.ι u (DifferentialFormSpace.ι v S.ω)
• taming : Function.Injective fun (v : VF) => DifferentialFormSpace.ι (J.J v) S.ω

structure IsTaming {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hp : HasPositivity (Ω 0)] (S : SymplecticManifold Ω VF) (J : AlmostComplexStr) : Prop

$J$ tames $\omega$: for any $X \neq Y$, $\omega(JX, \iota_X \omega - \iota_Y \omega)$ is positive, expressing a strict positivity condition $\omega(\cdot, J\cdot) > 0$.

• taming (X Y : VF) : X ≠ Y → HasPositivity.IsPositive (DifferentialFormSpace.ι (J.J X) (DifferentialFormSpace.ι X S.ω - DifferentialFormSpace.ι Y S.ω))

structure CompatibleTriple {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max u_1 u_2)

A compatible triple $(\omega, J, g)$ on a symplectic manifold: a compatible almost complex structure $J$ together with the induced Riemannian metric $g(\cdot, \cdot) = \omega(\cdot, J\cdot)$.

• J : AlmostComplexStr
• compat : IsCompatibleACS S self.J
• g : Ω 2

theorem polar_decomp_compatible_acs {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [ht : HasTangentSpaces Ω VF] (S : SymplecticManifold Ω VF) : ∃ (J : AlmostComplexStr), IsCompatibleACS S J

Existence of compatible almost complex structures. Every symplectic manifold $(M, \omega)$ admits an almost complex structure $J$ compatible with $\omega$, constructed pointwise via polar decomposition and assembled into a global field.

class IsContractible (S : Type u_1) : Type (max u_1 (u_2 + 1))

A typeclass witnessing that $S$ is contractible: it embeds into an ambient real vector space and admits a basepoint together with a normalization retraction, providing the data to build straight-line homotopies between any element and the basepoint.

• point : S
• AmbientSpace : Type u_2
• ambientAddCommGroup : AddCommGroup (AmbientSpace S)
• ambientModule : Module ℝ (AmbientSpace S)
• embed : S → AmbientSpace S
• normalize : AmbientSpace S → S
• normalize_embed (s : S) : normalize (embed s) = s

noncomputable def IsContractible.retraction {S : Type u_1} [hc : IsContractible S] (t : ↑(Set.Icc 0 1)) (s : S) : S

The retraction at time $t \in [0, 1]$: the convex combination $(1 - t)\,\mathrm{embed}(s) + t\,\mathrm{embed}(\star)$ pulled back via normalize.

structure IsContinuousPath {S : Type u} (γ : ↑(Set.Icc 0 1) → S) : Type (u + 1)

Witness that $\gamma : [0, 1] \to S$ is a continuous path: it is obtained by normalizing a linear interpolation between two points in an ambient real vector space.

• AmbientSpace : Type u
• ambientAddCommGroup : AddCommGroup self.AmbientSpace
• ambientModule : Module ℝ self.AmbientSpace
• start : self.AmbientSpace
• stop : self.AmbientSpace
• normalize : self.AmbientSpace → S
• path_eq (t : ↑(Set.Icc 0 1)) : γ t = self.normalize ((1 - ↑t) • self.start + ↑t • self.stop)

def CompatibleACS {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type u_2

The space of almost complex structures compatible with the symplectic manifold $S$.

def CompatibleComplexStructureSpace {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (ω : LinearMap.BilinForm ℝ V) : Type u_1

The space of linear complex structures $J : V \to V$ compatible with a symplectic form $\omega$ on a finite-dimensional real vector space $V$.

theorem compRight_injective_of_symplectic {V : Type u_1} [AddCommGroup V] [Module ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) {J₁ J₂ : V →ₗ[ℝ] V} (h : ω.compRight J₁ = ω.compRight J₂) : J₁ = J₂

Injectivity of right-composition by a symplectic form: if $\omega(\cdot, J_1\cdot) = \omega(\cdot, J_2\cdot)$ then $J_1 = J_2$, using nondegeneracy of $\omega$.

theorem polar_decomposition_compatible_J {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) : ∃ (polar : LinearMap.BilinForm ℝ V → V →ₗ[ℝ] V), (∀ (g : LinearMap.BilinForm ℝ V), SymplecticLinearAlgebra.IsCompatibleComplexStr ω (polar g)) ∧ ∀ (J : V →ₗ[ℝ] V), SymplecticLinearAlgebra.IsCompatibleComplexStr ω J → polar (ω.compRight J) = J

Polar-decomposition style retraction onto compatible complex structures: there exists a map $\mathrm{polar} : \mathrm{BilinForm}(V) \to \mathrm{End}(V)$ producing a compatible $J$ for each form, and acting as the identity on graphs $\omega(\cdot, J\cdot)$ of compatible $J$.

noncomputable def polar_decomp_path {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) (J₀ J₁ : CompatibleComplexStructureSpace ω) : ↑(Set.Icc 0 1) → CompatibleComplexStructureSpace ω

The path of compatible complex structures from $J_0$ to $J_1$ obtained by linearly interpolating the graphs $\omega(\cdot, J_i\cdot)$ and applying the polar retraction.

theorem polar_decomp_path_zero {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) (J₀ J₁ : CompatibleComplexStructureSpace ω) : polar_decomp_path hω J₀ J₁ ⟨0, ⋯⟩ = J₀

The polar interpolation path starts at $J_0$: $\mathrm{path}(0) = J_0$.

theorem polar_decomp_path_one {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) (J₀ J₁ : CompatibleComplexStructureSpace ω) : polar_decomp_path hω J₀ J₁ ⟨1, ⋯⟩ = J₁

The polar interpolation path ends at $J_1$: $\mathrm{path}(1) = J_1$.

noncomputable def polar_decomp_path_continuous {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) (J₀ J₁ : CompatibleComplexStructureSpace ω) : IsContinuousPath (polar_decomp_path hω J₀ J₁)

The polar interpolation path is continuous: it factors as straight-line interpolation in the ambient bilinear-form space composed with the normalize map.

noncomputable def fiberwise_acs_contractible {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {ω : LinearMap.BilinForm ℝ V} (hω : SymplecticLinearAlgebra.IsSymplecticForm ω) : IsContractible (CompatibleComplexStructureSpace ω)

The fiberwise statement: at each point, the space of linear complex structures compatible with the symplectic form $\omega$ is contractible (via the polar decomposition retraction).

noncomputable def sections_principle_axiom {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [ht : HasTangentSpaces Ω VF] (S : SymplecticManifold Ω VF) : ((x : HasTangentSpaces.M Ω VF) → IsContractible (CompatibleComplexStructureSpace (HasTangentSpaces.eval₂ x S.ω))) → IsContractible (CompatibleACS S)

Sections principle (axiomatized): if each fiber of compatible complex structures is contractible, then the global space of compatible almost complex structures is contractible. This is the standard sections-of-a-contractible-fibration argument.

@[reducible]

noncomputable def compatible_acs_contractible_DFS {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [ht : HasTangentSpaces Ω VF] (S : SymplecticManifold Ω VF) : IsContractible (CompatibleACS S)

Contractibility of the space of compatible almost complex structures for a symplectic manifold $(M, \omega)$: combining fiberwise contractibility with the sections principle.

theorem compatible_forms_convex_closed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S₀ S₁ : SymplecticManifold Ω VF) (t : ℝ) : DifferentialFormSpace.d VF ((1 - t) • S₀.ω + t • S₁.ω) = 0

The convex combination $(1 - t)\omega_0 + t\omega_1$ of two closed symplectic forms is closed: $d\omega_t = 0$.

theorem compatible_forms_convex_compat {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) (S₀ S₁ : SymplecticManifold Ω VF) (h₀ : IsCompatibleACS S₀ J) (h₁ : IsCompatibleACS S₁ J) (t : ℝ) (u v : VF) : DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.ι (J.J v) ((1 - t) • S₀.ω + t • S₁.ω)) = DifferentialFormSpace.ι u (DifferentialFormSpace.ι v ((1 - t) • S₀.ω + t • S₁.ω))

$J$-compatibility is preserved under convex combinations of symplectic forms: $\omega_t(Ju, Jv) = \omega_t(u, v)$ whenever each $\omega_i$ is $J$-compatible.

theorem ι_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι X (-α) = -DifferentialFormSpace.ι X α

Interior product commutes with negation: $\iota_X(-\alpha) = -\iota_X\alpha$.

theorem ι_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) {p : ℕ} (α β : Ω (p + 1)) : DifferentialFormSpace.ι X (α - β) = DifferentialFormSpace.ι X α - DifferentialFormSpace.ι X β

Interior product distributes over subtraction: $\iota_X(\alpha - \beta) = \iota_X\alpha - \iota_X\beta$.

theorem compatible_forms_convex_nondeg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hp : HasPositivity (Ω 0)] (J : AlmostComplexStr) (S₀ S₁ : SymplecticManifold Ω VF) (ht₀ : IsTaming S₀ J) (ht₁ : IsTaming S₁ J) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X ((1 - t) • S₀.ω + t • S₁.ω)

Convexity (nondegeneracy part): if $J$ tames both $\omega_0$ and $\omega_1$, then the convex combination $\omega_t = (1 - t)\omega_0 + t\omega_1$ is nondegenerate for $t \in [0, 1]$.

theorem compatible_forms_convex_taming {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hp : HasPositivity (Ω 0)] (J : AlmostComplexStr) (S₀ S₁ : SymplecticManifold Ω VF) (ht₀ : IsTaming S₀ J) (ht₁ : IsTaming S₁ J) (t : ℝ) (ht : t ∈ Set.Icc 0 1) : IsTaming { ω := (1 - t) • S₀.ω + t • S₁.ω, closed := ⋯, nondegenerate := ⋯ } J

Convexity (taming preserved): the convex combination $\omega_t = (1 - t)\omega_0 + t\omega_1$ remains tamed by $J$, witnessing that the space of $J$-tamed symplectic forms is convex.

theorem DFSMorphism.pullback_zero' {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_X : ℕ → Type u_3} {VF_X : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_X : DifferentialFormSpace Ω_X VF_X] (i : DFSMorphism Ω_X VF_X Ω_M VF_M) {p : ℕ} : i.pullback 0 = 0

The pullback of the zero form is zero: $i^* 0 = 0$.

theorem DFSMorphism.pullback_closed' {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_X : ℕ → Type u_3} {VF_X : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_X : DifferentialFormSpace Ω_X VF_X] (i : DFSMorphism Ω_X VF_X Ω_M VF_M) {p : ℕ} (α : Ω_M p) (hclosed : DifferentialFormSpace.d VF_M α = 0) : DifferentialFormSpace.d VF_X (i.pullback α) = 0

Pullback preserves closedness: if $d\alpha = 0$ then $d(i^*\alpha) = 0$.

theorem DFSMorphism.pullback_sub' {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_X : ℕ → Type u_3} {VF_X : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_X : DifferentialFormSpace Ω_X VF_X] (i : DFSMorphism Ω_X VF_X Ω_M VF_M) {p : ℕ} (α β : Ω_M p) : i.pullback (α - β) = i.pullback α - i.pullback β

Pullback distributes over subtraction: $i^*(\alpha - \beta) = i^*\alpha - i^*\beta$.

def acs_submanifold_symplectic_DFS {Ω_M : ℕ → Type u_1} {VF_M : Type u_2} {Ω_X : ℕ → Type u_3} {VF_X : Type u_4} [inst_M : DifferentialFormSpace Ω_M VF_M] [inst_X : DifferentialFormSpace Ω_X VF_X] [hp_M : HasPositivity (Ω_M 0)] [hp_X : HasPositivity (Ω_X 0)] (S : SymplecticManifold Ω_M VF_M) (J : AlmostComplexStr) (_hcompat : IsCompatibleACS S J) (htame : IsTaming S J) (i : DFSMorphism Ω_X VF_X Ω_M VF_M) (push : VF_X → VF_M) (push_inj : Function.Injective push) (j_inv : ∀ (v : VF_X), ∃ (w : VF_X), push w = J.J (push v)) (naturality : ∀ (v : VF_X) {p : ℕ} (α : Ω_M (p + 1)), DifferentialFormSpace.ι v (i.pullback α) = i.pullback (DifferentialFormSpace.ι (push v) α)) (pullback_pos : ∀ (f : Ω_M 0), HasPositivity.IsPositive f → HasPositivity.IsPositive (i.pullback f)) : SymplecticManifold Ω_X VF_X

Almost-complex submanifold $\implies$ symplectic. Given a tamed pair $(M, \omega, J)$ and an immersion $i : X \hookrightarrow M$ whose pushforward is $J$-invariant, the pullback $i^*\omega$ is a symplectic form on $X$, exhibiting $X$ as a symplectic submanifold.

structure AlmostComplexStructure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_1 u_3)

An almost complex structure on a smooth manifold $M$ in Mathlib formalism: a smooth field of fiberwise endomorphisms $J_x : T_xM \to T_xM$ with $J_x^2 = -\mathrm{id}$.

• J (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x
• sq_neg (x : M) (v : TangentSpace I x) : (self.J x) ((self.J x) v) = -v

structure PointwiseSymplecticForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_1 u_3)

A pointwise symplectic form on $M$: a field of skew-symmetric, nondegenerate bilinear forms $\omega_x : T_xM \times T_xM \to \mathbb{R}$ (closedness is not yet imposed).

• form (x : M) : TangentSpace I x →ₗ[ℝ] TangentSpace I x →ₗ[ℝ] ℝ
• skew (x : M) (u v : TangentSpace I x) : ((self.form x) u) v = -((self.form x) v) u
• nondeg (x : M) (u : TangentSpace I x) : (∀ (v : TangentSpace I x), ((self.form x) u) v = 0) → u = 0

structure IsCompatibleACS_Mathlib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] (ω : PointwiseSymplecticForm I M) (J : AlmostComplexStructure I M) : Prop

$J$ is compatible with the pointwise symplectic form $\omega$ in Mathlib formalism: $\omega(Ju, Jv) = \omega(u, v)$ and $\omega(v, Jv) > 0$ for $v \neq 0$ (taming/positivity).

• preserves (x : M) (u v : TangentSpace I x) : ((ω.form x) ((J.J x) u)) ((J.J x) v) = ((ω.form x) u) v
• taming (x : M) (v : TangentSpace I x) : v ≠ 0 → ((ω.form x) v) ((J.J x) v) > 0

def CompatibleACSSpace_Mathlib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] (ω : PointwiseSymplecticForm I M) : Type (max u_1 u_3)

The space of almost complex structures on $M$ compatible with the pointwise symplectic form $\omega$ (Mathlib version).

theorem pointwise_form_is_symplectic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (ω : PointwiseSymplecticForm I M) (x : M) : SymplecticLinearAlgebra.IsSymplecticForm (ω.form x)

At each point $x \in M$, the value $\omega_x$ of a pointwise symplectic form is a linear symplectic form on the tangent space $T_xM$.

@[reducible]

noncomputable def fiberwise_acs_contractible_Mathlib {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [hfd : FiniteDimensional ℝ E] (ω : PointwiseSymplecticForm I M) (x : M) : IsContractible (CompatibleComplexStructureSpace (ω.form x))

Fiberwise contractibility in Mathlib formalism: at each $x \in M$, the space of linear complex structures compatible with $\omega_x$ is contractible.

theorem sections_principle_Mathlib {E : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [hfd : FiniteDimensional ℝ E] {H : Type u_5} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_6} [TopologicalSpace M] [ChartedSpace H M] (ω : PointwiseSymplecticForm I M) [TopologicalSpace (CompatibleACSSpace_Mathlib I M ω)] (h_fiber_contractible : (x : M) → IsContractible (CompatibleComplexStructureSpace (ω.form x))) : ∃ (J₀ : CompatibleACSSpace_Mathlib I M ω) (h : ↑(Set.Icc 0 1) → CompatibleACSSpace_Mathlib I M ω → CompatibleACSSpace_Mathlib I M ω), (∀ (s : CompatibleACSSpace_Mathlib I M ω), h ⟨0, ⋯⟩ s = s) ∧ (∀ (s : CompatibleACSSpace_Mathlib I M ω), h ⟨1, ⋯⟩ s = J₀) ∧ (∀ (t : ↑(Set.Icc 0 1)), h t J₀ = J₀) ∧ Continuous (Function.uncurry h)

Sections principle (Mathlib version): assuming each fiber of compatible complex structures is contractible, there exist a basepoint $J_0$ and a continuous deformation retract $h_t$ of the space of compatible almost complex structures onto $J_0$.

theorem acs_submanifold_symplectic {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (ω : PointwiseSymplecticForm I M) (J : AlmostComplexStructure I M) (hcompat : IsCompatibleACS_Mathlib I M ω J) (x : M) (W : Submodule ℝ (TangentSpace I x)) (hJ_inv : ∀ v ∈ W, (J.J x) v ∈ W) (v : TangentSpace I x) : v ∈ W → v ≠ 0 → ∃ w ∈ W, ((ω.form x) v) w ≠ 0

Almost-complex subspace is symplectic (Mathlib version): a $J$-invariant subspace $W \subseteq T_xM$ inherits a nondegenerate restriction of $\omega$, since for any $v \in W$ with $v \neq 0$, the partner $Jv$ also lies in $W$ and $\omega(v, Jv) > 0$.

structure Integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (J : AlmostComplexStructure I M) (N : (x : M) → TangentSpace I x → TangentSpace I x → TangentSpace I x) : Prop

Integrability of $J$: the Nijenhuis tensor $N_J$ vanishes identically. By the Newlander-Nirenberg theorem this is equivalent to $J$ coming from a genuine complex structure.

• vanishes (x : M) (u v : TangentSpace I x) : N x u v = 0