Bounded semilinear Dirichlet existence theorem (source code)

= Bounded semilinear Dirichlet existence theorem
{title2=$-\Delta u=f(u),\quad u\in H_0^1(\Omega),\quad f\in C_b(\mathbb R)$}

For a smooth bounded domain and a bounded continuous scalar function $f$, this problem has a <weak solution>. Let $S$ be the zero-Dirichlet inverse of $-\Delta$, defined by the <Lax-Milgram theorem>. The <Poincaré inequality> gives $\|Sh\|_2\leq C_P^2\|h\|_2$. The <Rellich-Kondrachov compactness theorem> makes $S:L^2\to L^2$ compact. The <Nemytskii operator> $N_f$ is continuous and has bounded image, so $T=S\circ N_f$ is a <nonlinear compact operator> mapping a sufficiently large closed $L^2$ ball into itself. The <Schauder fixed-point theorem> gives a <fixed point>, necessarily in $H_0^1$, and its defining identity is the desired <weak formulation>. This proves existence; uniqueness requires additional assumptions.