structure SymplecticFormOnMfd {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 symplectic form on a manifold: a smoothly varying nondegenerate antisymmetric bilinear form $\omega_x$ on each tangent space $T_x M$.

• ω (x : M) : TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
• antisymm (x : M) (u v : TangentSpace I x) : ((self.ω x) u) v = -((self.ω x) v) u
• nondegenerate (x : M) (u : TangentSpace I x) : (∀ (v : TangentSpace I x), ((self.ω x) u) v = 0) → u = 0
• closed : True

noncomputable def nijenhuisTensorField {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] [IsManifold I ⊤ M] (Jstr : AlmostComplexStructure I M) (U V : (x : M) → TangentSpace I x) (x : M) : TangentSpace I x

The Nijenhuis tensor field of an almost complex structure $J$: $N_J(U,V) = [JU, JV] - J[U, JV] - J[JU, V] - [U, V]$.

structure IsIntegrableACS {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] [IsManifold I ⊤ M] (Jstr : AlmostComplexStructure I M) : Prop

An almost complex structure is integrable (i.e., a complex structure) when its Nijenhuis tensor vanishes identically.

• nijenhuis_vanishes (U V : (x : M) → TangentSpace I x) (x : M) : nijenhuisTensorField Jstr U V x = 0

structure IsCompatibleMfd {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] [IsManifold I ⊤ M] (ω : SymplecticFormOnMfd I M) (Jstr : AlmostComplexStructure I M) : Prop

$J$ is compatible with $\omega$: $\omega(JU, JV) = \omega(U, V)$ and $\omega(u, Ju) > 0$ for $u \ne 0$ (taming).

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

structure KahlerStructure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] : Type (max u_1 u_4)

A Kähler structure on $M$: a symplectic form $\omega$ and an integrable almost complex structure $J$ that are compatible.

• ω : SymplecticFormOnMfd I M
• J : AlmostComplexStructure I M
• integrable : IsIntegrableACS self.J
• compatible : IsCompatibleMfd self.ω self.J

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

The Nijenhuis tensor of an almost complex structure $J$, packaged as a bilinear vector-field-valued operation $N(U, V)$ that is antisymmetric on $1$-forms.

• N : VF → VF → VF
• antisymm (u v : VF) (α : Ω 1) : DifferentialFormSpace.ι (self.N u v) α = -DifferentialFormSpace.ι (self.N v u) α

structure IsNijenhuisOf {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) : Prop

nij represents the Nijenhuis tensor of $J$, i.e. it equals $[JX, JY] - J[JX, Y] - J[X, JY] - [X, Y]$ as evaluated on $1$-forms.

• nijenhuis_eq (X Y : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (nij.N X Y) α = DifferentialFormSpace.ι (HasLieBracket.bracket Ω (J.J X) (J.J Y)) α - DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω (J.J X) Y)) α - DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω X (J.J Y))) α - DifferentialFormSpace.ι (HasLieBracket.bracket Ω X Y) α
• nijenhuis_eq_J (X Y : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (J.J (nij.N X Y)) α = DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω (J.J X) (J.J Y))) α - DifferentialFormSpace.ι (J.J (J.J (HasLieBracket.bracket Ω (J.J X) Y))) α - DifferentialFormSpace.ι (J.J (J.J (HasLieBracket.bracket Ω X (J.J Y)))) α - DifferentialFormSpace.ι (J.J (HasLieBracket.bracket Ω X Y)) α

structure IsIntegrable {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) : Prop

The almost complex structure $J$ is integrable when its Nijenhuis tensor vanishes when paired with any $1$-form.

• vanishes (u v : VF) (α : Ω 1) : DifferentialFormSpace.ι (nij.N u v) α = 0

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

A symplectic manifold $(M, \omega)$ together with $J$ is Kähler when $J$ is an integrable almost complex structure compatible with $\omega$.

• integrable : ∃ (nij : NijenhuisTensor J), IsNijenhuisOf J nij ∧ IsIntegrable J nij
• compatible : IsCompatibleACS S J

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

The Dolbeault operators $\partial$ and $\bar\partial$ on a complex manifold, satisfying $d = \partial + \bar\partial$, $\partial^2 = 0$, $\bar\partial^2 = 0$.

• del {p : ℕ} : Ω p → Ω (p + 1)
• delbar {p : ℕ} : Ω p → Ω (p + 1)
• decomp {p : ℕ} (α : Ω p) : DifferentialFormSpace.d VF α = self.del α + self.delbar α
• del_sq {p : ℕ} (α : Ω p) : self.del (self.del α) = 0
• delbar_sq {p : ℕ} (α : Ω p) : self.delbar (self.delbar α) = 0
• delbar_add {p : ℕ} (α β : Ω p) : self.delbar (α + β) = self.delbar α + self.delbar β
• delbar_smul {p : ℕ} (r : ℝ) (α : Ω p) : self.delbar (r • α) = r • self.delbar α

class IsStrictlyPlurisubharmonic {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (dol : DolbeaultOps) (φ : Ω 0) : Prop

A function $\varphi$ is strictly plurisubharmonic when the $(1,1)$-form $\partial\bar\partial\varphi$ is nondegenerate as a pairing on vector fields.

• nondeg : Function.Injective fun (X : VF) => DifferentialFormSpace.ι X (dol.del (dol.delbar φ))

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

Interior product distributes over subtraction: $\iota_X(a - b) = \iota_X a - \iota_X b$.

theorem DifferentialFormSpace.d_neg_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (f : Ω 0) : d VF (-f) = -d VF f

The exterior derivative on $0$-forms commutes with negation: $d(-f) = -df$.

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

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

theorem nijenhuis_dual_eq_dForm_20_re_raw {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h : IsNijenhuisOf J nij) (α β : Ω 1) (htype : ∀ (X : VF), DifferentialFormSpace.ι X β = DifferentialFormSpace.ι (J.J X) α) (u v : VF) : DifferentialFormSpace.ι v (DifferentialFormSpace.ι u (DifferentialFormSpace.d VF α)) - DifferentialFormSpace.ι (J.J v) (DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.d VF α)) + DifferentialFormSpace.ι (J.J v) (DifferentialFormSpace.ι u (DifferentialFormSpace.d VF β)) + DifferentialFormSpace.ι v (DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.d VF β)) = DifferentialFormSpace.ι (nij.N u v) α

Raw form of the key identity: a particular combination of $\iota_X\iota_Y(d\alpha)$ and $\iota_X\iota_Y(d\beta)$ equals $\iota_{N(u,v)}\alpha$, expressing $d|_{(2,0)}$ as the Nijenhuis dual.

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

A $(0,1)$-form represented by real and imaginary $1$-forms $(\mathrm{re}, \mathrm{im})$ satisfying the type condition $\iota_X \mathrm{im} = \iota_{JX} \mathrm{re}$.

• re : Ω 1
• im : Ω 1
• type_cond (X : VF) : DifferentialFormSpace.ι X self.im = DifferentialFormSpace.ι (J.J X) self.re

def dForm_20_proj {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) (f : Form01 J) (u v : VF) : Ω 0

The real part of the $(2,0)$-projection of $df$ for a $(0,1)$-form $f$, evaluated on a pair of vector fields $(u, v)$.

def dForm_20_proj_im {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (J : AlmostComplexStr) (f : Form01 J) (u v : VF) : Ω 0

The imaginary part of the $(2,0)$-projection of $df$ for a $(0,1)$-form $f$, evaluated on a pair of vector fields $(u, v)$.

def nijenhuis_dual_eval {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (nij : NijenhuisTensor J) (f : Form01 J) (u v : VF) : Ω 0

Evaluation of the Nijenhuis dual on the real part of $f$: $\iota_{N(u,v)} f_{\mathrm{re}}$.

def nijenhuis_dual_eval_im {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {J : AlmostComplexStr} (nij : NijenhuisTensor J) (f : Form01 J) (u v : VF) : Ω 0

Evaluation of the Nijenhuis dual on the imaginary part of $f$: $\iota_{N(u,v)} f_{\mathrm{im}}$.

theorem nijenhuis_dual_eq_dForm_20_proj_re {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h : IsNijenhuisOf J nij) (f : Form01 J) (u v : VF) : dForm_20_proj J f u v = nijenhuis_dual_eval nij f u v

For a $(0,1)$-form $f$, the real part of the $(2,0)$-projection of $df$ equals the Nijenhuis dual evaluation on $f_{\mathrm{re}}$.

theorem nijenhuis_dual_eq_dForm_20_im_raw {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h : IsNijenhuisOf J nij) (α β : Ω 1) (htype : ∀ (X : VF), DifferentialFormSpace.ι X β = DifferentialFormSpace.ι (J.J X) α) (u v : VF) : DifferentialFormSpace.ι v (DifferentialFormSpace.ι u (DifferentialFormSpace.d VF β)) - DifferentialFormSpace.ι (J.J v) (DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.d VF β)) - DifferentialFormSpace.ι v (DifferentialFormSpace.ι (J.J u) (DifferentialFormSpace.d VF α)) - DifferentialFormSpace.ι (J.J v) (DifferentialFormSpace.ι u (DifferentialFormSpace.d VF α)) = DifferentialFormSpace.ι (J.J (nij.N u v)) α

Raw form of the imaginary identity expressing the $(2,0)$-projection in terms of $\iota_{J\,N(u,v)}\alpha$.

theorem nijenhuis_dual_eq_dForm_20_proj_im {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h : IsNijenhuisOf J nij) (f : Form01 J) (u v : VF) : dForm_20_proj_im J f u v = nijenhuis_dual_eval_im nij f u v

The imaginary part of the $(2,0)$-projection of $df$ equals the Nijenhuis dual evaluation on $f_{\mathrm{im}}$.

theorem nijenhuis_dual_map_is_d_20_typed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [HasLieBracket Ω VF] (J : AlmostComplexStr) (nij : NijenhuisTensor J) (h : IsNijenhuisOf J nij) (f : Form01 J) (u v : VF) : dForm_20_proj J f u v = nijenhuis_dual_eval nij f u v

Typed version: the Nijenhuis dual map equals the $(2,0)$-projection of $d$ on a $(0,1)$-form.