[proofplan] We prove the standard equivalence of the four formulations of the Levi problem. The equivalence of domain of holomorphy and holomorphic convexity is the Cartan-Thullen theorem. The distance formulation is Levi's local pseudoconvexity criterion. The hard implication is pseudoconvexity implies domain of holomorphy, obtained by solving $\bar\partial$ with plurisubharmonic weights and constructing holomorphic functions with controlled boundary growth. [/proofplan] [step:Domains of holomorphy are holomorphically convex] Assume $\Omega$ is a domain of holomorphy and let $K\Subset \Omega$. If the holomorphic hull $\widehat K_\Omega$ failed to be relatively compact, one could choose a sequence $z_j\in \widehat K_\Omega$ converging to a boundary point. The defining inequality for the hull says that every $f\in\mathcal{O}(\Omega)$ is bounded at $z_j$ by its supremum on $K$. The Cartan-Thullen continuation theorem then implies that all holomorphic functions on $\Omega$ extend across that boundary point, contradicting the definition of a domain of holomorphy. Hence $\widehat K_\Omega\Subset\Omega$. [/step] [step:Holomorphic convexity gives a domain of holomorphy] Assume $\Omega$ is holomorphically convex. For each boundary point $p\in\partial\Omega$, choose compact sets exhausting $\Omega$ and points approaching $p$. Holomorphic convexity lets one separate a point near $p$ from a fixed compact set by a holomorphic function. A standard diagonal product construction then gives a holomorphic function on $\Omega$ that becomes unbounded along a sequence tending to $p$. Such a function cannot extend holomorphically across $p$, because a holomorphic extension would be bounded in a small neighbourhood of $p$. Thus $\Omega$ is a domain of holomorphy. [/step] [step:Relate pseudoconvexity to the boundary distance] For a proper domain in $\mathbb{C}^n$, Levi pseudoconvexity is equivalent to plurisubharmonicity of the boundary distance potential $-\log d(z,\partial\Omega)$, up to the standard regularisation needed near non-smooth boundary points. If $-\log d$ is plurisubharmonic, its sublevel sets stay a positive Euclidean distance from the boundary, so on bounded domains it is a plurisubharmonic exhaustion, and on unbounded domains it is combined with a harmless psh growth term to control escape to infinity. Conversely, any plurisubharmonic exhaustion forces the Levi form of smooth boundary pieces to be nonnegative; the boundary distance criterion globalises this local condition. [/step] [step:Use $\bar\partial$ solvability to pass from pseudoconvexity to holomorphic convexity] Assume $\Omega$ has a plurisubharmonic exhaustion. Hörmander's weighted $L^2$ estimates solve $\bar\partial u=f$ with weights growing rapidly near chosen boundary points. Applying this to cut-off local holomorphic functions produces global holomorphic functions that are small on a prescribed compact set and large near a point outside its holomorphic hull. Therefore holomorphic hulls of compact sets remain in compact sublevel sets of the exhaustion. This proves holomorphic convexity, and the previous steps give all four equivalences. [/step]