For $N\ge2$ and $β>0$, consider the canonical 2D Coulomb gas ensemble \begin{equation} \mathrm{d}\mathbb{P}_{N,β}(Z) =\mathsf{Z}_{N,β}^{-1}e^{-β|Z|^2/2} \prod_{i<j}|z_i-z_j|^{β/N}\mathrm{d} Z \qquadon \mathbb{C}^N. \end{equation} The factor $N^{-1}$ in the pair exponent places the ensemble at the diffusive, or high-temperature, scale. We prove that, for every fixed inverse temperature $β>0$, this Gibbs measure satisfies a logarithmic Sobolev inequality (LSI) on the closed Dirichlet-form domain generated by collision-free compactly supported smooth functions, with a positive constant independent of $N$. The LSI constant may be chosen uniformly when $β$ ranges over a compact subset of $(0,\infty)$. A second main result establishes Poincaré and logarithmic Sobolev inequalities for planar Gaussian measures weighted by finite products of positive powers of distances to points, with constants depending only on the total variance of the underlying Gaussian measure and the total exponent, not on the number or locations of the points. To prove the full labeled Poincaré inequality, we decompose variance into permutation-invariant and label-dependent parts, controlled respectively by a weighted $\bar\partial$ estimate and by relative-coordinate conditioning with random transpositions; separately, one-site logarithmic Sobolev inequalities, a conditional entropy inequality, and a repulsive partition estimate give a defective logarithmic Sobolev inequality. Rothaus tightening combines the resulting full labeled Poincaré inequality with the defective logarithmic Sobolev inequality. The two main theorems on their stated closed form domains and all results used in their formal proofs, including those from the literature, have been formalized in Lean 4.