Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Hartogs pseudoconvexity implies Levi pseudoconvexity for C2 domains

Statement

Let Ω⊆Cm be a domain with C2 boundary. If Ω is Hartogs pseudoconvex, then Ω is Levi pseudoconvex.

Facts & Assumptions

Given: A domain Ω⊆Cm with C2 boundary.

[L1]
[L2]

The restriction of a plurisubharmonic function to an affine complex line is subharmonic or identically −∞ (Plurisubharmonic functions).

[L3]

Levi pseudoconvexity is the tangential Levi-form condition and is independent of the chosen defining function (Levi pseudoconvex domains, Levi pseudoconvexity does not depend on the defining function).

[L4]

A plane subharmonic function cannot exceed its finite boundary maximum on a disc unless it is constant (A plane subharmonic function with an interior maximum is constant on its component).

Proof

technique · direct
1.1L3givenassume-contraconstructalgebra

Suppose toward a contradiction that Ω is not Levi pseudoconvex at a boundary point p. Choose a defining function ρ and a complex tangent vector v with Lρ(p;v)<0. Translate p to 0, make a complex-linear change of coordinates sending v to the first coordinate direction and the real normal into the last coordinate, and normalize the last coordinate by subtracting the holomorphic pure-quadratic part of the Taylor expansion. After multiplying ρ by a positive constant, its restriction to the resulting (z1,zm)-plane has the form ρ(z1,0,…,0,zm)=Re⁡zm−c∣z1∣2+o(∣z1∣2+∣zm∣2) for some c>0; subtracting that pure-quadratic part does not change the tangential Levi coefficient. Choose λ>0 and then s0>0 small enough that the remainder is dominated by the two displayed negative terms. The affine analytic discs Φs(ζ)=(λζ,0,…,0,−s)(∣ζ∣≤1) then lie in Ω for 0<s≤s0, their centres Φs(0) converge to p as s↓0, and K:=⋃0≤s≤s0Φs(∂D) is compactly contained in Ω: on the boundary circles the term −cλ2 stays uniformly negative even at s=0.

2.1L1L2L3L4step 1.1discharge-contradiction∎

By [L1], choose a continuous plurisubharmonic exhaustion u of Ω, and let M:=max⁡Ku. For 0<s≤s0, the function u∘Φs is subharmonic on D by [L2] and continuous on its closure. Its boundary values are at most M, so [L4] gives u(Φs(0))≤M. Thus all the centres lie in the compact sublevel set {u≤M}⋐Ω. But those centres converge to the boundary point p, contradicting compact containment. Therefore no negative tangential Levi direction exists, and [L3] makes Ω Levi pseudoconvex.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources