ExampleConstruction: Literature-sourcedVerification: 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.

A strictly plurisubharmonic exhaustion of the convex unit ball

Example

Assume the Axiom of Choice (AC). Fix $m \geq 1$ , let $B : = {z \in C^{m} : ∥ z ∥ < 1}$ be the unit ball, put $u (z) : = 1 - ∥ z ∥^{2}$ , and set $ψ (z) : = - \log u (z) = - \log (1 - ∥ z ∥^{2}) .$ Then $B$ is a nonempty convex domain in $C^{m}$ and $ψ$ is a $C^{\infty}$ strictly plurisubharmonic exhaustion of $B$ : at every $a \in B$ and every $ξ \in C^{m} ∖ {0}$ the Levi form is $L_{ψ} (a; ξ) = \frac{∥ ξ ∥^{2}}{u (a)} + \frac{∣ \sum_{j < m} \overline{a_{j}} ξ_{j} ∣^{2}}{u (a)^{2}} > 0,$ and every sublevel set ${ψ \leq c}$ , $c \in R$ , is a compact subset of $B$ .

Facts & Assumptions

Given: The Axiom of Choice; the unit ball $B = {z \in C^{m} : ∥ z ∥ < 1}$ with $m \geq 1$ ; the functions $u = 1 - ∥ z ∥^{2}$ and $ψ = - \log u$ .

[F1]

For open $Ω \subseteq C^{m}$ and $u \in C^{2} (Ω, R)$ the Levi form is $L_{u} (a; v) : = \sum_{j < m} \sum_{k < m} \frac{\partial^{2} u}{\partial z_{j} \partial {\overline{z}}_{k}} (a) v_{j} \overline{v_{k}},$ and $u$ is strictly plurisubharmonic when $L_{u} (a; v) > 0$ for every $a \in Ω$ and every $v \neq 0$ (The Levi form and strict plurisubharmonicity, with its coordinate labels relabeled from $1, \dots, m$ to the canonical $0, \dots, m - 1$ ).

[F2]

A $C^{2}$ function is plurisubharmonic on $Ω$ exactly when $L_{u} (a; v) \geq 0$ for every $a \in Ω$ and every $v \in C^{m}$ (The C^2 Levi criterion for plurisubharmonicity).

[F3]

A continuous plurisubharmonic exhaustion of a domain $Ω$ is a continuous plurisubharmonic $u$ on $Ω$ with ${u \leq c}$ compact in $Ω$ for every real $c$ (Plurisubharmonic exhaustions and Hartogs pseudoconvexity).

[F4]

The open ball and closed ball of centre $a$ and radius $ρ > 0$ are $B (a, ρ) = {z : ∥ z - a ∥ < ρ}$ and $\overline{B} (a, ρ) = {z : ∥ z - a ∥ \leq ρ}$ (Balls, polydiscs and the distinguished boundary in $C^{m}$ ).

[F5]

In a metric space $(X, d)$ the open ball $B (x, r)$ is open and the closed ball $\overset{ˉ}{B} (x, r)$ is closed, for every $x$ and every $r > 0$ (Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed).

[F6]

Through the dictionary $Φ : C^{m} \to R^{2 m}$ one has $∥ z ∥ = (\sum_{k < m} ∣ z_{k} ∣^{2})^{1 / 2}$ with $∣ z_{k} ∣^{2} = x_{k}^{2} + y_{k}^{2}$ , the balls, open sets and continuous maps of $C^{m}$ are verbatim those of $R^{2 m}$ , and a subset of $C^{m}$ is compact exactly when it is closed and bounded (Complex $m$ -space and its real coordinate dictionary).

[F7]

A subset $A$ of a metric space is bounded when $A = \emptyset$ or $A \subseteq B (x_{0}, r)$ for some point $x_{0}$ and some real $r > 0$ (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space).

[F8]

A norm $N$ satisfies $N (v) = 0$ if and only if $v = 0$ , absolute homogeneity $N (λ v) = ∣ λ ∣ N (v)$ , and the triangle inequality $N (u + v) \leq N (u) + N (v)$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[F9]

A subset $U \subseteq R^{m}$ is convex when for all $x, y \in U$ and all $t \in [0, 1]$ the point $(1 - t) x + t y$ lies in $U$ (A convex subset of $R^{m}$ contains every line segment between two of its points).

[F10]

A subset $A$ of a topological space is a compact subset when the subspace $(A, T_{A})$ is a compact topological space (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F11]

The Wirtinger operators are $\partial_{z_{k}} = \frac{1}{2} (\partial_{x_{k}} - i \partial_{y_{k}})$ and $\partial_{{\overset{ˉ}{z}}_{k}} = \frac{1}{2} (\partial_{x_{k}} + i \partial_{y_{k}})$ (Wirtinger operators in $C^{m}$ ).

[F12]

For $x > 0$ , $\log$ is differentiable with $\log^{'} (x) = 1 / x$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[F13]

For every real $α$ the function $x \mapsto x^{α}$ is differentiable on $(0, \infty)$ with $(x^{α})^{'} = α x^{α - 1}$ (Continuity and derivatives of positive-base real powers).

[F14]

The exponential function is continuous and strictly increasing on $R$ (The exponential function is strictly increasing).

[F15]

$\log$ is the inverse function of $\exp$ , so that $\exp (\log x) = x$ for every $x > 0$ (The natural logarithm as the inverse of the exponential function).

[F16]

A set $X$ is path-connected when every pair of its points is joined by a path in $X$ (Paths, path-connected spaces and path components); every path-connected space is connected (Every path-connected space is connected, and every path component lies inside a component).

[F17]

AC states that every family of nonempty sets has a choice function (The Axiom of Choice).

Choice use. AC is the ambient hypothesis recorded in the Example and [F17] is cited as that hypothesis. The proof selects nothing: the ball, the function $ψ$ , the straight-line paths and the radii $r = (1 - \exp (- c))^{1 / 2}$ are explicit formulas.

Verification

technique · direct

1.1F4F5F6F8F9F16F17givenalgebra

By [F6] one has $∥ z ∥^{2} = \sum_{j < m} ∣ z_{j} ∣^{2} = \sum_{j < m} (x_{j}^{2} + y_{j}^{2})$ , and $B$ is the open ball $B (0, 1)$ in the sense of [F4]; it is open by [F5] and nonempty because $∥ 0 ∥ = 0 < 1$ by [F8]. It is convex: for $z, w \in B$ and $t \in [0, 1]$ , [F8] gives $∥ (1 - t) z + t w ∥ \leq (1 - t) ∥ z ∥ + t ∥ w ∥ < (1 - t) + t = 1$ since $1 - t \geq 0$ and $t \geq 0$ , so $(1 - t) z + t w \in B$ , which is the straight-line condition of [F9] transported by the $R$ -linear dictionary [F6]. The segments $t \mapsto (1 - t) z + t w$ are continuous paths in $B$ from $z$ to $w$ , so $B$ is path-connected by [F16] and connected by [F16]; hence $B$ is a nonempty convex domain in $C^{m}$ .

2.1F6F11F12F13inductionalgebra

The function $u = 1 - \sum_{j < m} (x_{j}^{2} + y_{j}^{2})$ is a polynomial in the real coordinates, hence $C^{\infty}$ on $C^{m}$ , and $u > 0$ on $B$ by step 1.1, so $ψ = - \log u$ is real-valued on $B$ . Moreover $\log$ is $C^{\infty}$ on $(0, \infty)$ : $\log^{'} = 1 / t$ by [F12], and $t \mapsto t^{- 1}$ has $k$ -th derivative $(- 1)^{k} k! t^{- k - 1}$ , a continuous function on $(0, \infty)$ , by induction from [F13], so every higher derivative of $\log$ exists and is continuous there. Hence $ψ \in C^{\infty} (B)$ , and differentiating the composition along the real coordinate directions gives $\partial_{x_{j}} ψ = 2 x_{j} / u$ and $\partial_{y_{j}} ψ = 2 y_{j} / u$ on $B$ ; applying the Wirtinger operators of [F11] gives $\partial_{z_{j}} ψ = \frac{1}{2} (2 x_{j} - 2 i y_{j}) / u = (x_{j} - i y_{j}) / u = \overline{z_{j}} / u$ and $\partial_{{\overset{ˉ}{z}}_{j}} ψ = \frac{1}{2} (2 x_{j} + 2 i y_{j}) / u = (x_{j} + i y_{j}) / u = z_{j} / u$ at every point of $B$ .

3.1step 2.1algebra

Differentiating the first-order expressions of step 2.1 once more gives $\partial^{2} ψ / \partial z_{j} \partial {\overset{ˉ}{z}}_{k} = δ_{j k} / u + \overline{z_{j}} z_{k} / u^{2}$ : indeed $\partial_{{\overset{ˉ}{z}}_{k}} (\overline{z_{j}} / u) = (\partial_{{\overset{ˉ}{z}}_{k}} \overline{z_{j}}) / u - \overline{z_{j}} (\partial_{{\overset{ˉ}{z}}_{k}} u) / u^{2} = δ_{j k} / u + \overline{z_{j}} z_{k} / u^{2}$ , because $\partial_{{\overset{ˉ}{z}}_{k}} u = - z_{k}$ .

3.2F4F5F6F7F10F14F15step 2.1algebra

For $z \in B$ and real $c$ , since $\log$ is the inverse of the strictly increasing function $\exp$ by [F14] and [F15], one has $ψ (z) \leq c ⟺ u (z) \geq \exp (- c) ⟺ ∥ z ∥^{2} \leq 1 - \exp (- c)$ ; hence ${ψ \leq c} = {z : ∥ z ∥^{2} \leq 1 - \exp (- c)}$ . If $1 - \exp (- c) < 0$ this set is empty; if $1 - \exp (- c) = 0$ it is the compact singleton ${0}$ ; otherwise it is the closed ball $\overline{B} (0, r)$ of [F4] with $r : = (1 - \exp (- c))^{1 / 2} \in (0, 1)$ , which is closed by [F5] and bounded in the sense of [F7] because it is contained in $B (0, r + 1)$ , hence compact in $C^{m}$ by [F6]. As it is contained in $B$ , and compactness of a subset is intrinsic by [F10] with the subspace topology inherited from $B$ equal to that inherited from $C^{m}$ , it is a compact subset of $B$ .

4.1F1F2step 2.1step 3.1algebra

Substituting step 3.1 into [F1] gives, at every $a \in B$ and every $ξ \in C^{m}$ , the Levi form $L_{ψ} (a; ξ) = \sum_{j, k} (δ_{j k} / u (a) + \overline{a_{j}} a_{k} / u (a)^{2}) ξ_{j} \overline{ξ_{k}} = ∥ ξ ∥^{2} / u (a) + ∣ \sum_{j < m} \overline{a_{j}} ξ_{j} ∣^{2} / u (a)^{2}$ , because $u (a) > 0$ by step 2.1; this is $\geq ∥ ξ ∥^{2} / u (a) > 0$ for every $ξ \neq 0$ , so $ψ$ is strictly plurisubharmonic on $B$ by [F1], and in particular plurisubharmonic there by [F2].

5.1F3step 1.1step 2.1step 3.2step 4.1∎

Conclusion: by step 1.1 the ball $B$ is a nonempty convex domain in $C^{m}$ ; by step 2.1 the function $ψ$ is $C^{\infty}$ on $B$ ; by step 4.1 it is strictly plurisubharmonic, hence plurisubharmonic; and by step 3.2 every sublevel set ${ψ \leq c}$ is a compact subset of $B$ . Therefore $ψ$ is a continuous strictly plurisubharmonic exhaustion of the convex unit ball in the sense of [F3].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

95 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

Harold P. Boas, Lecture Notes on Several Complex Variables (standard reference, not scraped)
Jean-Pierre Demailly, Complex Analytic and Differential Geometry (standard reference, not scraped)