theorem CM8.dirichlet_existence (n : ℕ) [Fact (2 ≤ n)] (Ω : Set (Fin n → ℝ)) (hΩ_open : IsOpen Ω) (hΩ_bounded : Bornology.IsBounded Ω) (hΩ_lip : IsLipschitzDomain Ω) (f g : (Fin n → ℝ) → ℝ) (hg : ContinuousOn g (frontier Ω)) : ∃ (u : (Fin n → ℝ) → ℝ), ContDiffOn ℝ 2 u Ω ∧ ContinuousOn u (closure Ω) ∧ (∀ x ∈ Ω, laplacian u x = f x) ∧ (∀ x ∈ frontier Ω, u x = g x) ∧ ∀ (u' : (Fin n → ℝ) → ℝ), ContDiffOn ℝ 2 u' Ω → ContinuousOn u' (closure Ω) → (∀ x ∈ Ω, laplacian u' x = f x) → (∀ x ∈ frontier Ω, u' x = g x) → ∀ x ∈ closure Ω, u' x = u x

Theorem 2.1 (basic existence and uniqueness for the Dirichlet problem): on a bounded Lipschitz domain $\Omega \subset \mathbb{R}^n$ ($n \geq 2$) with continuous boundary data $g \in C(\partial \Omega)$, the Poisson problem $\Delta u = f$ in $\Omega$ with $u = g$ on $\partial \Omega$ has a unique solution $u \in C^2(\Omega) \cap C(\overline{\Omega})$.

theorem CM8.green_function_decomposition (n : ℕ) [hn : Fact (2 ≤ n)] (Ω : Set (Fin n → ℝ)) (hΩ_open : IsOpen Ω) (hΩ_bounded : Bornology.IsBounded Ω) (hΩ_lip : IsLipschitzDomain Ω) (hΦ_cont : ∀ x ∈ Ω, ContinuousOn (fun (σ : Fin n → ℝ) => FundSolN (x - σ)) (frontier Ω)) : ∃ (φ : (Fin n → ℝ) → (Fin n → ℝ) → ℝ), (∀ x ∈ Ω, ContDiffOn ℝ 2 (φ x) Ω) ∧ (∀ x ∈ Ω, ContinuousOn (φ x) (closure Ω)) ∧ (∀ x ∈ Ω, ∀ y ∈ Ω, laplacian (φ x) y = 0) ∧ (∀ x ∈ Ω, ∀ σ ∈ frontier Ω, φ x σ = FundSolN (x - σ)) ∧ ∀ x ∈ Ω, ∀ σ ∈ frontier Ω, FundSolN (x - σ) - φ x σ = 0

Proposition 2.0.2 (Green function decomposition): the Green function of $\Omega$ can be written as $G(x, y) = \Phi(x - y) - \varphi(x, y)$, where for each fixed $x \in \Omega$ the corrector $\varphi(x, \cdot)$ solves the Dirichlet problem $\Delta_y \varphi(x, y) = 0$ in $\Omega$ with $\varphi(x, \sigma) = \Phi(x - \sigma)$ on $\partial \Omega$.