LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Smooth strict plurisubharmonic regularization of a psh exhaustion

Statement

Assume the Axiom of Choice (AC) and the Axiom of Countable Choice. Let $Ω \subseteq C^{n}$ , $n \geq 1$ , be a domain and let $u : Ω \to R$ be a continuous plurisubharmonic exhaustion, that is, $u$ is continuous and plurisubharmonic and every sublevel set ${z \in Ω : u (z) \leq c}$ , $c \in R$ , is a compact subset of $Ω$ .

Then there exist a function $S \in C^{\infty} (Ω)$ and a strictly increasing sequence $c_{1} < c_{2} < \dots$ with $c_{k} \to + \infty$ such that, writing $Ω_{k} : = {z \in Ω : S (z) < c_{k}}$ :

$S$ is strictly plurisubharmonic on $Ω$ , $S > u$ on $Ω$ , and $S$ is again an exhaustion of $Ω$ , that is, ${z \in Ω : S (z) \leq c}$ is a compact subset of $Ω$ for every real $c$ ;
every $c_{k}$ is a regular value of $S$ , and $\partial Ω_{k} = {z \in Ω : S (z) = c_{k}}$ is a nonempty $C^{\infty}$ hypersurface of $Ω$ ;
$\overline{Ω_{k}} \subseteq Ω_{k + 1}$ and $⋃_{k \geq 1} Ω_{k} = Ω$ , so every $\overline{Ω_{k}}$ is a compact subset of $Ω$ ;
(strong pseudoconvexity) for every $k$ , every $p \in \partial Ω_{k}$ and every $v \in C^{n} ∖ {0}$ with $\sum_{j < n} \frac{\partial S}{\partial z_{j}} (p) v_{j} = 0$ one has $L_{S} (p; v) > 0$ .

Facts & Assumptions

Given: The Axiom of Choice and the Axiom of Countable Choice; a domain $Ω \subseteq C^{n}$ with $n \geq 1$ ; and a continuous plurisubharmonic exhaustion $u : Ω \to R$ .

[F1]

A function $u : Ω \to R$ is a continuous plurisubharmonic exhaustion when it is continuous, plurisubharmonic, and every sublevel ${u \leq c}$ is compact in $Ω$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F2]

(Richberg's approximation theorem.) If $v \in Psh (X)$ is continuous and strictly plurisubharmonic on an open set $V \subseteq X$ , with $H_{v} > γ$ for a continuous positive Hermitian form $γ$ , then for every continuous $0 < λ < 1$ there is $\tilde{v} \in C^{0} (X) \cap C^{\infty} (V)$ such that $v \leq \tilde{v} \leq v + λ$ on $V$ and $H_{\tilde{v}} > (1 - λ) γ$ ; if $v$ is strictly plurisubharmonic on all of $X$ , $\tilde{v}$ can be chosen strictly plurisubharmonic on all of $X$ (Demailly, Complex Analytic and Differential Geometry, Ch. I §5.E, Theorem 5.21, printed pp. 43-44).

[F3]

For a smooth map from a finite-dimensional manifold to $R$ , the regular values are dense; in particular every nonempty open interval contains a regular value when the Axiom of Countable Choice holds (Regular values have null complement and are dense).

[F4]

A value $c$ is regular for $S$ if every point of $S^{- 1} (c)$ is a regular point; an empty fibre is regular by convention (Regular and critical points and values).

[F5]

A regular level of a smooth real-valued function on an open subset of $R^{N}$ is locally a smooth graph of dimension $N - 1$ (A regular level set is locally a $C^{k}$ graph of dimension $m - n$ ).

[F6]

In ZF, AC implies AC $_{ω}$ (AC implies DC implies countable choice; The Axiom of Countable Choice ( ${A C}_{ω}$ )), and AC states that every family of nonempty sets has a choice function (The Axiom of Choice).

Choice use. AC and AC $_{ω}$ are the ambient hypotheses. The proof uses AC $_{ω}$ only to choose a sequence of regular values from nonempty open intervals; each such interval contains regular values by [F3].

Proof

technique · Richberg approximation, followed by Sard's theorem

1.1F1algebra

Put $u_{0} : = u + ∣ z ∣^{2} + 1$ and $γ : = \frac{1}{2} H_{∣ z ∣^{2}}$ . Then $u_{0}$ is continuous and plurisubharmonic, and $H_{u_{0}} \geq H_{∣ z ∣^{2}} > γ$ because $u$ is plurisubharmonic. It is an exhaustion: if $u_{0} (z) \leq c$ , then $u (z) \leq c - 1$ , and ${u_{0} \leq c}$ is closed in $Ω$ ; thus it is a closed subset of the compact set ${u \leq c - 1}$ . Moreover $u_{0} > u$ everywhere.

2.1F2step 1.1algebra

Apply [F2] to $u_{0}$ on $X = V = Ω$ with the constant error $λ = 1 / 2$ . This gives $S \in C^{\infty} (Ω)$ satisfying $u_{0} \leq S \leq u_{0} + 1 / 2$ and $H_{S} > \frac{1}{2} γ$ . Hence $S$ is strictly plurisubharmonic, $S > u$ , and $S$ is an exhaustion because each sublevel ${S \leq c}$ is closed in $Ω$ and contained in the compact sublevel ${u_{0} \leq c}$ .

3.1F3F6step 2.1given

Fix $z_{0} \in Ω$ . The exhaustion $S$ is unbounded above: otherwise $Ω = {S \leq c}$ for some $c$ , making the noncompact open set $Ω$ compact. Choose an integer $M > S (z_{0})$ . For each $k \geq 1$ , [F3] supplies a regular value in the fixed nonempty interval $(M + 2 k, M + 2 k + 1)$ ; AC $_{ω}$ selects one such $c_{k}$ for each $k$ . Then $c_{1} < c_{2} < \dots$ , $c_{k} \to + \infty$ , and every level ${S = c_{k}}$ is nonempty: the continuous image $S (Ω)$ is an interval because $Ω$ is connected, it contains $S (z_{0})$ , and it is unbounded above.

4.1F1F4F5step 2.1step 3.1

Set $Ω_{k} : = {S < c_{k}}$ . Each $\overline{Ω_{k}}$ is contained in the compact set ${S \leq c_{k}}$ , and $\overline{Ω_{k}} \subseteq {S \leq c_{k}} \subseteq {S < c_{k + 1}} = Ω_{k + 1} .$ The sublevels cover $Ω$ because $c_{k} \to + \infty$ . Continuity gives $\partial Ω_{k} \subseteq {S = c_{k}}$ ; conversely, every point of the regular level $S = c_{k}$ is a boundary point by the implicit function theorem. Thus $\partial Ω_{k} = {S = c_{k}}$ is a nonempty smooth hypersurface, by [F4] and [F5].

5.1

At every $p \in \partial Ω_{k}$ the function $S - c_{k}$ defines $Ω_{k}$ near $p$ . Since $S$ is strictly plurisubharmonic, every nonzero complex tangent vector $v$ satisfies $L_{S} (p; v) > 0$ . Steps 2.1–4.1 establish the remaining assertions in the Statement. [F1, F2, step 2.1, step 4.1] $□$

Depends on

Used by

Dependency tree · two levels

31 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

Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)