Documentation

Atlas.IntroductionToPartialDifferentialEquations.code.CM8.RepresentationFormulas

noncomputable def CM8.phiConvolution (f : (Fin 3)) (x : Fin 3) :

The Newtonian-potential convolution in $\mathbb{R}^3$: given $f : \mathbb{R}^3 \to \mathbb{R}$, phiConvolution f x is $\int_{\mathbb{R}^3} \Phi(x - y) f(y) \, d^3 y$, where $\Phi$ is the 3D fundamental solution of the Laplacian.

Instances For
    noncomputable def CM8.laplacian3 (f : (Fin 3)) (x : Fin 3) :

    The Laplacian $\Delta f = \sum_{i=1}^{3} \partial_i^2 f$ on $\mathbb{R}^3$, specialised from the general laplacian to dimension three.

    Instances For
      theorem CM8.leibniz_laplacian_phiConvolution (f : (Fin 3)) (hf : ContDiff f) (hsupp : HasCompactSupport f) (x : Fin 3) :
      laplacian3 (phiConvolution f) x = (y : Fin 3), Phi3 (x - y) * laplacian3 f y

      Leibniz/differentiation-under-the-integral for the Newtonian potential: if $f$ is smooth and compactly supported, then $\Delta(\Phi * f)(x) = \int \Phi(x-y) \Delta f(y) \, d^3y$.

      theorem CM8.newtonian_potential_inversion (f : (Fin 3)) (hf : ContDiff f) (hsupp : HasCompactSupport f) (x : Fin 3) :
      (y : Fin 3), Phi3 (x - y) * laplacian3 f y = f x

      Newtonian-potential inversion: convolution of $\Delta f$ with the fundamental solution $\Phi$ recovers $f$, i.e. $\int \Phi(x-y) \Delta f(y) \, d^3 y = f(x)$ for smooth compactly supported $f$.

      theorem CM8.poisson_solution (f : (Fin 3)) (hf_smooth : ContDiff f) (hf_supp : HasCompactSupport f) (x : Fin 3) :

      Solution of Poisson's equation on $\mathbb{R}^3$: for smooth compactly supported $f$, $u = \Phi * f$ satisfies $\Delta u = f$ pointwise.

      theorem CM8.phiConvolution_far_field_decay (f : (Fin 3)) (hf : ContDiff f) (hsupp : HasCompactSupport f) :
      ∃ (C₁ : ) (R₀ : ), 0 < C₁ 0 < R₀ ∀ (x : Fin 3), euclidNorm x > R₀|phiConvolution f x| C₁ / euclidNorm x

      Far-field decay of the Newtonian potential: there exist constants $C_1, R_0 > 0$ such that $|(\Phi * f)(x)| \le C_1 / |x|$ whenever $|x| > R_0$, reflecting the $1/r$ decay of $\Phi$ in $\mathbb{R}^3$.

      theorem CM8.phiConvolution_bounded (f : (Fin 3)) (hf : ContDiff f) (hsupp : HasCompactSupport f) :
      ∃ (M : ), 0 < M ∀ (x : Fin 3), euclidNorm x > 1|phiConvolution f x| M

      Boundedness of the Newtonian potential away from the origin: the convolution $\Phi * f$ is uniformly bounded on $\{|x| > 1\}$.

      theorem CM8.poisson_solution_decay (f : (Fin 3)) (hf_smooth : ContDiff f) (hf_supp : HasCompactSupport f) :
      C > 0, ∀ (x : Fin 3), euclidNorm x > 1|phiConvolution f x| C / euclidNorm x

      Combined decay estimate for the Poisson solution $u = \Phi * f$: there is a constant $C > 0$ such that $|u(x)| \le C / |x|$ for all $|x| > 1$, obtained by combining the far-field and global boundedness estimates.

      opaque CM8.outwardUnitNormal {n : } :
      Set (Fin n)(Fin n)Fin n

      The outward unit normal vector $\hat{N}(\sigma)$ to a domain $\Omega \subseteq \mathbb{R}^n$ at a boundary point $\sigma$. Declared opaque since the construction is not relevant here.

      theorem CM8.outwardUnitNormal_euclidBall_eq {n : } (R : ) (hR : 0 < R) (p σ : Fin n) ( : euclidNorm (σ - p) = R) :
      outwardUnitNormal {y : Fin n | euclidNorm (y - p) < R} σ = fun (i : Fin n) => (σ i - p i) / R

      On the boundary of the (Euclidean) ball $\{y : |y - p| < R\}$, the outward unit normal at $\sigma$ is the radial unit vector $(\sigma - p)/R$.

      noncomputable def CM8.normalDeriv {n : } (Ω : Set (Fin n)) (f : (Fin n)) (σ : Fin n) :

      The outward normal derivative of $f$ on $\partial\Omega$ at $\sigma$, given by $\nabla_{\hat{N}(\sigma)} f(\sigma) = Df(\sigma) \cdot \hat{N}(\sigma)$.

      Instances For
        opaque CM8.surfaceMeasure {n : } :
        Set (Fin n)MeasureTheory.Measure (Fin n)

        The surface (Hausdorff) measure on $\partial\Omega$, declared opaque since its precise construction is not used here.

        noncomputable def CM8.surfaceIntegral {n : } (Ω : Set (Fin n)) (f : (Fin n)) :

        The surface integral $\int_{\partial\Omega} f(\sigma) \, d\sigma$ of $f$ over the boundary of $\Omega$, with respect to the surface measure.

        Instances For
          noncomputable def CM8.unitSphereArea (n : ) :

          The surface area $\omega_n$ of the unit sphere $S^{n-1} \subset \mathbb{R}^n$, given by $\omega_n = 2 \pi^{n/2} / \Gamma(n/2)$ for $n \ge 1$.

          Instances For
            noncomputable def CM8.FundSolN {n : } [Fact (2 n)] (x : Fin n) :

            The fundamental solution $\Phi(x)$ of $-\Delta$ in $\mathbb{R}^n$ (equation 1.0.3): for $n = 2$ it is $\tfrac{1}{2\pi}\log|x|$, and for $n \ge 3$ it is $-1/(\omega_n |x|^{n-2})$.

            Instances For

              The surface area of the unit sphere $S^2 \subset \mathbb{R}^3$ equals $4\pi$.

              theorem CM8.FundSolN_eq_Phi3 [inst : Fact (2 3)] (x : Fin 3) :

              In dimension three, the general fundamental solution FundSolN agrees with the 3D-specific `Phi3 = -1/(4\pi |x|)$.

              theorem CM8.greens_second_identity {n : } [Fact (2 n)] (Ω : Set (Fin n)) (u v : (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (hv : ContDiffOn 2 v (closure Ω)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) :
              (y : Fin n) in Ω, v y * laplacian u y - u y * laplacian v y = surfaceIntegral Ω fun (σ : Fin n) => v σ * normalDeriv Ω u σ - u σ * normalDeriv Ω v σ

              Green's second identity on a Lipschitz domain $\Omega \subset \mathbb{R}^n$: for $u, v \in C^2(\bar\Omega)$, $$\int_\Omega \bigl(v \Delta u - u \Delta v\bigr)\, dy = \int_{\partial\Omega} \bigl(v \, \nabla_{\hat N} u - u \, \nabla_{\hat N} v\bigr)\, d\sigma.$$

              noncomputable def CM8.sphereIntegral {n : } (center : Fin n) (r : ) (f : (Fin n)) :

              The surface integral $\int_{|\sigma - c| = r} f(\sigma)\, d\sigma$ of $f$ over the sphere of radius $r$ centred at $c$, with respect to the surface measure of the ball.

              Instances For
                theorem CM8.laplacian_FundSolN_eq_zero_away {n : } [Fact (2 n)] (x y : Fin n) (hxy : x y) :
                laplacian (fun (z : Fin n) => FundSolN (x - z)) y = 0

                The fundamental solution is harmonic away from its pole: $\Delta_y \Phi(x - y) = 0$ whenever $y \ne x$.

                theorem CM8.IsLipschitzDomain_diff_closedBall {n : } (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hx : x Ω) ( : 0 < ε) :

                Removing a small closed ball from a Lipschitz domain $\Omega$ centred at an interior point keeps the resulting set $\Omega \setminus \overline{B(x,\varepsilon)}$ a Lipschitz domain.

                theorem CM8.contDiffOn_FundSolN_diff_ball {n : } [Fact (2 n)] (x : Fin n) (Ω : Set (Fin n)) (ε : ) ( : 0 < ε) :
                ContDiffOn 2 (fun (y : Fin n) => FundSolN (x - y)) (closure (Ω \ Metric.closedBall x ε))

                The map $y \mapsto \Phi(x - y)$ is $C^2$ on $\overline{\Omega \setminus \overline{B(x,\varepsilon)}}$, since the singularity at $y = x$ has been removed.

                theorem CM8.contDiffOn_restrict_punctured {n : } (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) ( : 0 < ε) :

                A $C^2$ function on $\overline\Omega$ remains $C^2$ when restricted to the closure of the punctured domain $\Omega \setminus \overline{B(x,\varepsilon)}$.

                theorem CM8.setIntegral_ball_eq_closedBall {n : } (f : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) :
                (y : Fin n) in Ω \ Metric.ball x ε, f y = (y : Fin n) in Ω \ Metric.closedBall x ε, f y

                Removing an open ball versus its closure differs only by the sphere, which has Lebesgue measure zero, so the corresponding set integrals agree.

                theorem CM8.integral_laplacian_v_vanishes {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                (y : Fin n) in Ω \ Metric.closedBall x ε, (fun (y : Fin n) => FundSolN (x - y)) y * laplacian u y - u y * laplacian (fun (z : Fin n) => FundSolN (x - z)) y = (y : Fin n) in Ω \ Metric.closedBall x ε, (fun (y : Fin n) => FundSolN (x - y)) y * laplacian u y

                On the punctured domain $\Omega \setminus \overline{B(x,\varepsilon)}$, since $\Delta_y \Phi(x - y) = 0$, the volume term $u(y)\, \Delta_y \Phi(x-y)$ vanishes and the integrand reduces to $\Phi(x - y) \Delta u(y)$.

                theorem CM8.surfaceIntegral_punctured_normalDeriv_decomp {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : IsOpen Ω) (hx : x Ω) ( : 0 < ε) (f g h k : (Fin n)) :
                (surfaceIntegral (Ω \ Metric.closedBall x ε) fun (σ : Fin n) => f σ * normalDeriv (Ω \ Metric.closedBall x ε) g σ - h σ * normalDeriv (Ω \ Metric.closedBall x ε) k σ) = (((surfaceIntegral Ω fun (σ : Fin n) => f σ * normalDeriv Ω g σ) - surfaceIntegral Ω fun (σ : Fin n) => h σ * normalDeriv Ω k σ) - sphereIntegral x ε fun (σ : Fin n) => f σ * normalDeriv Ω g σ) + sphereIntegral x ε fun (σ : Fin n) => h σ * normalDeriv Ω k σ

                Decomposition of a surface integral over $\partial(\Omega \setminus \overline{B(x,\varepsilon)})$ into the contribution from $\partial\Omega$ minus the contribution from the inner sphere $\partial B(x,\varepsilon)$ (with the normal pointing inward toward $x$ contributing the sign flip).

                theorem CM8.surfaceIntegral_punctured_domain_decomp {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hx : x Ω) ( : 0 < ε) :
                (surfaceIntegral (Ω \ Metric.closedBall x ε) fun (σ : Fin n) => (fun (y : Fin n) => FundSolN (x - y)) σ * normalDeriv (Ω \ Metric.closedBall x ε) u σ - u σ * normalDeriv (Ω \ Metric.closedBall x ε) (fun (y : Fin n) => FundSolN (x - y)) σ) = (((surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) - sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                Specialisation of surfaceIntegral_punctured_normalDeriv_decomp to the integrand $\Phi(x - \sigma) \nabla_{\hat N} u - u(\sigma) \nabla_{\hat N} \Phi$ appearing in the representation formula.

                theorem CM8.greens_identity_on_omega_eps {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (x : Fin n) (hx : x Ω) (ε : ) ( : 0 < ε) :
                (y : Fin n) in Ω \ Metric.ball x ε, FundSolN (x - y) * laplacian u y = (((surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) - sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                Green's second identity applied on the punctured domain $\Omega \setminus B(x,\varepsilon)$ with $v(y) = \Phi(x - y)$: the volume integral equals the $\partial\Omega$ surface terms minus the sphere terms at $|y - x| = \varepsilon$.

                theorem CM8.FundSolN_mul_integrable {n : } [Fact (2 n)] (Ω : Set (Fin n)) (f : (Fin n)) (x : Fin n) :

                Integrability of $y \mapsto \Phi(x - y) f(y)$ on $\Omega$: the local singularity of the fundamental solution at $y = x$ is integrable, so the product is integrable on the domain.

                theorem CM8.volume_integral_limit {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => (y : Fin n) in Ω \ Metric.ball x ε, FundSolN (x - y) * laplacian u y) (nhdsWithin 0 (Set.Ioi 0)) (nhds ( (y : Fin n) in Ω, FundSolN (x - y) * laplacian u y))

                As $\varepsilon \downarrow 0$, the punctured-domain integral $\int_{\Omega \setminus B(x,\varepsilon)} \Phi(x-y) \Delta u(y) \, dy$ converges to the full volume integral over $\Omega$.

                theorem CM8.surfaceMeasure_sphere_lt_top {n : } [Fact (2 n)] (center : Fin n) (ε : ) ( : 0 < ε) :
                (surfaceMeasure (Metric.ball center ε)) (Metric.sphere center ε) <

                The surface measure of a sphere $\partial B(c, \varepsilon)$ is finite.

                theorem CM8.FundSolN_norm_on_sphere {n : } [Fact (2 n)] (hn3 : 3 n) :
                ∃ (C_F : ), 0 C_F ∀ (x : Fin n) (ε : ), 0 < εσMetric.sphere x ε, FundSolN (x - σ) C_F / ε ^ (n - 2)

                For $n \ge 3$, on the sphere $|σ - x| = \varepsilon$ the fundamental solution satisfies $\|\Phi(x - \sigma)\| \le C_F / \varepsilon^{n-2}$ for some constant $C_F \ge 0$.

                theorem CM8.normalDeriv_bounded_of_C2 {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) :
                ∃ (M : ), 0 M ∀ (σ : Fin n), normalDeriv Ω u σ M

                If $u \in C^2(\overline\Omega)$ then the normal derivative $\nabla_{\hat N} u$ is uniformly bounded on $\partial\Omega$ (and in fact globally, by some constant $M$).

                theorem CM8.surfaceMeasure_sphere_real_le {n : } [Fact (2 n)] :
                ∃ (C_S : ), 0 C_S ∀ (x : Fin n) (ε : ), 0 < ε(surfaceMeasure (Metric.ball x ε)).real (Metric.sphere x ε) C_S * ε ^ (n - 1)

                Linear upper bound on the surface area of a sphere of radius $\varepsilon$ in $\mathbb{R}^n$: there exists $C_S \ge 0$ with $\mathrm{area}(\partial B(x, \varepsilon)) \le C_S \varepsilon^{n-1}$.

                theorem CM8.sphereIntegral_Phi_gradU_pointwise_area_bound {n : } [Fact (2 n)] (hn3 : 3 n) (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                ∃ (K : ), ∀ (ε : ), 0 < ε∃ (B : ), (∀ σMetric.sphere x ε, FundSolN (x - σ) * normalDeriv Ω u σ B) B * (surfaceMeasure (Metric.ball x ε)).real (Metric.sphere x ε) K * ε

                Pointwise-times-area bound for $n \ge 3$: there exists $K$ such that for every $\varepsilon > 0$ one can choose a pointwise bound $B$ for $\Phi(x-\sigma) \nabla_{\hat N}u(\sigma)$ on the sphere with $B \cdot \mathrm{area}(\partial B(x,\varepsilon)) \le K \varepsilon$.

                theorem CM8.sphere_integral_Phi_gradU_bound {n : } [Fact (2 n)] (hn3 : 3 n) (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                ∃ (K : ), ∀ (ε : ), 0 < εsphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ K * ε

                Linear-in-$\varepsilon$ estimate on the sphere integral $\int_{|σ-x|=ε} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma)\, d\sigma$ for $n \ge 3$: it is bounded by $K\varepsilon$ for some constant $K$.

                theorem CM8.sphere_integral_R3_bound {n : } [Fact (2 n)] (hn3 : 3 n) (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                ∃ (C : ), ∀ (ε : ), 0 < εsphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ C * ε

                Alias for sphere_integral_Phi_gradU_bound: for $n \ge 3$ the third sphere term $R_3(\varepsilon)$ in the punctured-domain decomposition is $O(\varepsilon)$.

                theorem CM8.sphere_integral_R3_bound_n2 {n : } [Fact (2 n)] (hn2 : n = 2) (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                ∃ (K : ) (C : ), 0 C ∀ (ε : ), 0 < εsphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ K * (ε * (|Real.log ε| + C))

                Refined sphere-integral bound in dimension $n = 2$, where $\Phi(x) \sim \log|x|$: the third sphere term is dominated by $K \varepsilon (|\log \varepsilon| + C)$ for some constants $K$ and $C \ge 0$.

                theorem CM8.sphere_integral_R3_vanishes_n2 {n : } [Fact (2 n)] (hn2 : n = 2) (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                In dimension $n = 2$, the sphere integral $R_3(\varepsilon) = \int_{|σ-x|=ε} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma) \, d\sigma \to 0$ as $\varepsilon \downarrow 0$, using the $\varepsilon |\log \varepsilon|$ bound.

                theorem CM8.sphere_integral_R3_vanishes {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                Combined result: in any dimension $n \ge 2$, the sphere integral $\int_{|σ-x|=ε} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma) \, d\sigma$ vanishes as $\varepsilon \downarrow 0$.

                theorem CM8.outwardUnitNormal_sphere_spec {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) (σ : Fin n) ( : σ Metric.sphere x ε) :
                outwardUnitNormal Ω σ = fun (i : Fin n) => (σ i - x i) / ε

                Specification of the outward unit normal on a sphere of radius $\varepsilon$ centred at $x$: at $\sigma$ with $|\sigma - x| = \varepsilon$, the normal vector is the radial direction $(\sigma - x)/\varepsilon$.

                theorem CM8.surfaceMeasure_ball_sphere_eq {n : } [Fact (2 n)] (x : Fin n) (ε : ) ( : 0 < ε) :

                Exact formula for the surface area of the sphere $\partial B(x, \varepsilon)$ in $\mathbb{R}^n$: $\omega_n \, \varepsilon^{n-1}$.

                theorem CM8.euclidNorm_eq_on_sphere {n : } [Fact (2 n)] (x σ : Fin n) (ε : ) ( : 0 < ε) ( : σ Metric.sphere x ε) :
                euclidNorm (x - σ) = ε

                On the sphere of radius $\varepsilon$ centred at $x$, the Euclidean distance $|x - \sigma|$ equals $\varepsilon$.

                theorem CM8.hasFDerivAt_FundSolN_sub {n : } [Fact (2 n)] (x σ : Fin n) (hr : euclidNorm (x - σ) > 0) :
                HasFDerivAt (fun (z : Fin n) => FundSolN (x - z)) ((1 / (unitSphereArea n * euclidNorm (x - σ) ^ (n - 1))) i : Fin n, ((σ i - x i) / euclidNorm (x - σ)) ContinuousLinearMap.proj i) σ

                Explicit Fréchet derivative of $z \mapsto \Phi(x - z)$ away from the pole, given as a sum involving the radial direction $(\sigma - x)/|x - \sigma|$ and the coordinate projections.

                theorem CM8.fderiv_FundSolN_radial_eq {n : } [Fact (2 n)] (x σ : Fin n) (ε : ) ( : 0 < ε) ( : σ Metric.sphere x ε) :
                ((fderiv (fun (z : Fin n) => FundSolN (x - z)) σ) fun (i : Fin n) => (σ i - x i) / ε) = 1 / (unitSphereArea n * ε ^ (n - 1))

                On the sphere $|σ - x| = \varepsilon$, applying the Fréchet derivative of $z \mapsto \Phi(x - z)$ to the radial unit vector $(\sigma - x)/\varepsilon$ yields the constant $1/(\omega_n \varepsilon^{n-1})$.

                theorem CM8.normalDeriv_FundSolN_constant_on_sphere {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) (σ : Fin n) ( : σ Metric.sphere x ε) :
                normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ = 1 / (surfaceMeasure (Metric.ball x ε)).real (Metric.sphere x ε)

                On the sphere $\partial B(x, \varepsilon)$, the normal derivative of $z \mapsto \Phi(x-z)$ is the constant $1/\mathrm{area}(\partial B(x,\varepsilon))$, regardless of the surrounding domain $\Omega$.

                theorem CM8.surfaceMeasure_sphere_real_pos {n : } [Fact (2 n)] (x : Fin n) (ε : ) ( : 0 < ε) :

                The surface area of any sphere of positive radius is strictly positive.

                theorem CM8.sphereIntegral_normalDeriv_Phi_eq_one {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                (sphereIntegral x ε fun (σ : Fin n) => normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) = 1

                Total flux of the fundamental solution through a sphere equals $1$: integrating the normal derivative $\nabla_{\hat N}\Phi(x - \sigma)$ over $\partial B(x,\varepsilon)$ gives exactly $1$, the source strength.

                theorem CM8.integrable_normalDeriv_Phi_sphere {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                MeasureTheory.Integrable (fun (σ : Fin n) => normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) ((surfaceMeasure (Metric.ball x ε)).restrict (Metric.sphere x ε))

                The normal derivative $\nabla_{\hat N}\Phi(x - \cdot)$ is integrable on the sphere $\partial B(x, \varepsilon)$ with respect to the surface measure.

                theorem CM8.integrable_mul_normalDeriv_Phi_sphere {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                MeasureTheory.Integrable (fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) ((surfaceMeasure (Metric.ball x ε)).restrict (Metric.sphere x ε))

                The product $u(\sigma) \nabla_{\hat N} \Phi(x - \sigma)$ is integrable on the sphere $\partial B(x, \varepsilon)$ with respect to the surface measure.

                theorem CM8.sphere_normalDeriv_Phi_normalization {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                (sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) = u x + sphereIntegral x ε fun (σ : Fin n) => (u σ - u x) * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                Splitting the sphere integral $\int_{|σ-x|=ε} u(\sigma) \nabla_{\hat N} \Phi(x-\sigma)$ as $u(x)$ plus an error term $\int (u(\sigma) - u(x)) \nabla_{\hat N} \Phi$, using the normalisation $\int \nabla_{\hat N} \Phi = 1$.

                theorem CM8.bddAbove_abs_deviation_sphere {n : } [Fact (2 n)] (u : (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                BddAbove (Set.range fun (σ : Fin n) => ⨆ (_ : σ Metric.sphere x ε), |u σ - u x|)

                The family of conditional suprema $\sup_{σ \in \text{sphere}} |u(\sigma) - u(x)|$ is bounded above (as a function of $\sigma$), used to manipulate expressions safely.

                theorem CM8.le_biSup_abs_deviation {n : } [Fact (2 n)] (u : (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) (σ : Fin n) ( : σ Metric.sphere x ε) :
                |u σ - u x| σ'Metric.sphere x ε, |u σ' - u x|

                For any $\sigma$ on the sphere $\partial B(x,\varepsilon)$, $|u(\sigma) - u(x)|$ is bounded above by the corresponding indexed supremum over the sphere.

                theorem CM8.sphereIntegral_deviation_abs_le {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : 0 < ε) :
                |sphereIntegral x ε fun (σ : Fin n) => (u σ - u x) * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ| σMetric.sphere x ε, |u σ - u x|

                The absolute value of the deviation sphere integral $\int (u(\sigma) - u(x)) \nabla_{\hat N}\Phi$ is bounded by the maximal oscillation $\sup_\sigma |u(\sigma) - u(x)|$ over the sphere.

                theorem CM8.sup_sphere_oscillation_tendsto_zero {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => σMetric.sphere x ε, |u σ - u x|) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                Continuity at $x$ implies that the supremum of the oscillation $|u(\sigma) - u(x)|$ over the shrinking sphere $\partial B(x,\varepsilon)$ tends to zero as $\varepsilon \downarrow 0$.

                theorem CM8.sphere_integral_deviation_bound {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => sphereIntegral x ε fun (σ : Fin n) => (u σ - u x) * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                The deviation sphere integral $\int (u(\sigma) - u(x)) \nabla_{\hat N}\Phi(x-\sigma)$ tends to $0$ as $\varepsilon \downarrow 0$, obtained by combining the deviation bound with the oscillation $\to 0$ result.

                theorem CM8.sphereIntegral_u_normalDeriv_Phi_tends_to_ux {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

                Mean-value-type limit: as $\varepsilon \downarrow 0$, the sphere integral $\int_{|σ-x|=ε} u(\sigma) \nabla_{\hat N}\Phi(x - \sigma)\, d\sigma$ converges to $u(x)$.

                theorem CM8.sphere_integral_u_normalDeriv_Phi_decomp {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                ∃ (error : ), (∀ ε > 0, (sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) = u x + error ε) Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                Reformulation: the sphere integral $\int u(\sigma) \nabla_{\hat N}\Phi(x-\sigma)$ admits the decomposition $u(x) + \text{error}(\varepsilon)$ where the error vanishes as $\varepsilon \downarrow 0$.

                theorem CM8.sphere_integral_R4_decomposition {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                ∃ (error : ), (∀ ε > 0, (sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) = u x + error ε) Filter.Tendsto error (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

                Alias for sphere_integral_u_normalDeriv_Phi_decomp: the fourth sphere term $R_4(\varepsilon)$ decomposes as $u(x)$ plus a vanishing error.

                theorem CM8.sphere_integral_R4_limit {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (x : Fin n) (hx : x Ω) :
                Filter.Tendsto (fun (ε : ) => sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) (nhdsWithin 0 (Set.Ioi 0)) (nhds (u x))

                The limit of the fourth sphere term is $u(x)$, the value of $u$ at the centre — the mean-value property of the fundamental solution.

                theorem CM8.epsilon_ball_limit_representation {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (x : Fin n) (hx : x Ω) :
                u x = (( (y : Fin n) in Ω, FundSolN (x - y) * laplacian u y) - surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                Representation formula obtained by taking $\varepsilon \downarrow 0$ in Green's identity on the punctured domain: for $u \in C^2(\bar\Omega)$ and $x \in \Omega$, $$u(x) = \int_\Omega \Phi(x-y) \Delta u(y), dy

                • \int_{\partial\Omega} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma), d\sigma
                • \int_{\partial\Omega} u(\sigma) \nabla_{\hat N} \Phi(x-\sigma), d\sigma.$$
                theorem CM8.representation_formula_n {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (x : Fin n) (hx : x Ω) :
                u x = (( (y : Fin n) in Ω, FundSolN (x - y) * laplacian u y) - surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                Proposition 2.0.3 in general dimension $n \ge 2$: the representation formula for $u \in C^2(\bar\Omega)$ at an interior point $x \in \Omega$ in terms of the fundamental solution $\Phi$, the volume integral of $\Delta u$, and the boundary terms involving $u$ and $\nabla_{\hat N} u$.

                theorem CM8.representation_formula (u : (Fin 3)) (Ω : Set (Fin 3)) (hu : ContDiff 2 u) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (x : Fin 3) (hx : x Ω) :
                u x = (( (y : Fin 3) in Ω, Phi3 (x - y) * laplacian3 u y) - surfaceIntegral Ω fun (σ : Fin 3) => Phi3 (x - σ) * normalDeriv Ω u σ) + surfaceIntegral Ω fun (σ : Fin 3) => u σ * normalDeriv Ω (fun (z : Fin 3) => Phi3 (x - z)) σ

                Proposition 2.0.3 specialised to $\mathbb{R}^3$ with the 3D fundamental solution $\Phi_3(x) = -1/(4\pi|x|)$: for $u \in C^2(\mathbb{R}^3)$, $\Omega$ a Lipschitz domain and $x \in \Omega$, $$u(x) = \int_\Omega \Phi_3(x-y) \Delta u(y), dy

                • \int_{\partial\Omega} \Phi_3(x-\sigma) \nabla_{\hat N} u(\sigma), d\sigma
                • \int_{\partial\Omega} u(\sigma) \nabla_{\hat N} \Phi_3(x-\sigma), d\sigma.$$
                structure CM8.GreenFunctionN (n : ) [Fact (2 n)] (Ω : Set (Fin n)) :

                Green function for the domain $\Omega \subset \mathbb{R}^n$ (Definition 2.0.2 together with the decomposition in Proposition 2.0.2): a function $G(x, y)$ on $\Omega \times \Omega$ with $\Delta_y G(x, y) = \delta(x)$ and $G(x, \sigma) = 0$ for $\sigma \in \partial \Omega$. It is packaged as the decomposition $G(x, y) = \Phi(x - y) - \phi(x, y)$, where the corrector $\phi(x, \cdot)$ is harmonic in $\Omega$ with boundary data $\Phi(x - \cdot)|_{\partial\Omega}$.

                Instances For

                  Instance: $2 \le 3$, supplied so that FundSolN and related results specialise to the three-dimensional setting.

                  theorem CM8.surfaceIntegral_eq {n : } (Ω : Set (Fin n)) (f : (Fin n)) :
                  surfaceIntegral Ω f = (σ : Fin n) in frontier Ω, f σ surfaceMeasure Ω

                  Unfolding lemma for surfaceIntegral: definitionally equal to the integral $\int_{\partial\Omega} f(\sigma) \, d\sigma$.

                  theorem CM8.surfaceIntegral_congr_frontier {n : } (Ω : Set (Fin n)) (f g : (Fin n)) (h : σfrontier Ω, f σ = g σ) :

                  Congruence of surface integrals: if $f = g$ on $\partial\Omega$, then their surface integrals agree.

                  theorem CM8.regularity_extension_axiom {n : } (Ω : Set (Fin n)) (u : (Fin n)) ( : IsOpen Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) :

                  Regularity-extension axiom: a function that is $C^2$ on the interior $\Omega$ and continuous on the closure $\bar\Omega$ is in fact $C^2$ on $\bar\Omega$.

                  theorem CM8.surfaceIntegral_punctured_inward_decomp {n : } [Fact (2 n)] (Ω : Set (Fin n)) (x : Fin n) (ε : ) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hx : x Ω) ( : 0 < ε) (u : (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) :
                  (surfaceIntegral (Ω \ Metric.closedBall x ε) fun (σ : Fin n) => (fun (y : Fin n) => FundSolN (x - y)) σ * normalDeriv (Ω \ Metric.closedBall x ε) u σ - u σ * normalDeriv (Ω \ Metric.closedBall x ε) (fun (y : Fin n) => FundSolN (x - y)) σ) = (((surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) + sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                  Textbook-sign variant of the punctured-domain surface decomposition: the surface integral over $\partial(\Omega \setminus \overline{B(x,\varepsilon)})$ equals the $\partial\Omega$ boundary contribution plus (rather than minus) the inner-sphere contribution, reflecting the choice of inward-pointing normal on $\partial B(x,\varepsilon)$.

                  theorem CM8.greens_identity_on_omega_eps_textbook_sign {n : } [Fact (2 n)] (u : (Fin n)) (Ω : Set (Fin n)) (hu : ContDiffOn 2 u (closure Ω)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (x : Fin n) (hx : x Ω) (ε : ) ( : 0 < ε) :
                  (y : Fin n) in Ω \ Metric.ball x ε, FundSolN (x - y) * laplacian u y = (((surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) + sphereIntegral x ε fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - sphereIntegral x ε fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                  Green's identity on the punctured domain with the textbook sign convention (inward normal on the inner sphere), giving the version of the identity matching equation (2.0.30) in the text.

                  theorem CM8.equation_2_0_30_core {n : } [Fact (2 n)] (Ω : Set (Fin n)) (u : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) (x : Fin n) (hx : x Ω) :
                  u x = ((- (y : Fin n) in Ω, FundSolN (x - y) * laplacian u y) + surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                  Core equation (2.0.30) of the textbook: representation of $u(x)$ in terms of $\Delta u$, the trace of $u$ on $\partial\Omega$, and the normal derivative of $u$, all paired with the fundamental solution $\Phi$, expressed using the textbook sign convention.

                  theorem CM8.equation_2_0_30 {n : } [Fact (2 n)] (Ω : Set (Fin n)) (u f g : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) (hu_pde : xΩ, laplacian u x = f x) (hu_bdy : σfrontier Ω, u σ = g σ) (x : Fin n) (hx : x Ω) :
                  u x = ((- (y : Fin n) in Ω, FundSolN (x - y) * f y) + surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) - surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ

                  Equation (2.0.30) for solutions of the Poisson boundary value problem $\Delta u = f$ in $\Omega$, $u = g$ on $\partial\Omega$: $u(x)$ is represented as $-\int_\Omega \Phi(x-y) f(y), dy

                  • \int_{\partial\Omega} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma), d\sigma
                  • \int_{\partial\Omega} g(\sigma) \nabla_{\hat N} \Phi(x-\sigma), d\sigma$.
                  theorem CM8.contDiffOn_closure_of_interior {n : } (Ω : Set (Fin n)) (u : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) :

                  Duplicate of the regularity-extension axiom under a Lipschitz domain assumption: $C^2$ on $\Omega$ together with continuity on $\bar\Omega$ promotes to $C^2$ on $\bar\Omega$.

                  theorem CM8.integrableOn_surfaceMeasure {n : } (Ω : Set (Fin n)) (f : (Fin n)) :

                  Integrability axiom for surface integrals: every function under consideration is integrable on $\partial\Omega$ with respect to the surface measure.

                  theorem CM8.surfaceIntegral_sub {n : } (Ω : Set (Fin n)) (f g : (Fin n)) :
                  (surfaceIntegral Ω fun (σ : Fin n) => f σ - g σ) = surfaceIntegral Ω f - surfaceIntegral Ω g

                  Linearity (subtraction) of the surface integral: $\int_{\partial\Omega} (f - g) = \int_{\partial\Omega} f - \int_{\partial\Omega} g$.

                  theorem CM8.equation_2_0_33_core {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (u : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) (x : Fin n) (hx : x Ω) :
                  0 = (( (y : Fin n) in Ω, gf.corrector x y * laplacian u y) - surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + surfaceIntegral Ω fun (σ : Fin n) => u σ * normalDeriv Ω (gf.corrector x) σ

                  Identity (2.0.33) at the core level: applying Green's second identity to $u$ and the harmonic corrector $\phi(x, \cdot)$ in $\Omega$ produces the relation $0 = \int_\Omega \phi(x, y) \Delta u(y), dy

                  • \int_{\partial\Omega} \Phi(x-\sigma) \nabla_{\hat N} u(\sigma), d\sigma
                  • \int_{\partial\Omega} u(\sigma) \nabla_{\hat N} \phi(x, \sigma), d\sigma$.
                  theorem CM8.equation_2_0_33 {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (u f g : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) (hu_pde : xΩ, laplacian u x = f x) (hu_bdy : σfrontier Ω, u σ = g σ) (x : Fin n) (hx : x Ω) :
                  0 = (( (y : Fin n) in Ω, gf.corrector x y * f y) - surfaceIntegral Ω fun (σ : Fin n) => FundSolN (x - σ) * normalDeriv Ω u σ) + surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (gf.corrector x) σ

                  Equation (2.0.33) for the Poisson boundary value problem: substituting $\Delta u = f$ in $\Omega$ and $u = g$ on $\partial\Omega$ into the corrector identity yields a relation among the source $f$, boundary data $g$, the corrector $\phi$, and the normal derivative of $u$.

                  theorem CM8.volume_integral_G_decomp {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (f : (Fin n)) (x : Fin n) (hPhi_int : MeasureTheory.IntegrableOn (fun (y : Fin n) => FundSolN (x - y) * f y) Ω MeasureTheory.volume) (hcorr_int : MeasureTheory.IntegrableOn (fun (y : Fin n) => gf.corrector x y * f y) Ω MeasureTheory.volume) :
                  (y : Fin n) in Ω, f y * gf.G x y = ( (y : Fin n) in Ω, FundSolN (x - y) * f y) - (y : Fin n) in Ω, gf.corrector x y * f y

                  Volume-integral form of the decomposition $G = \Phi - \phi$: under integrability, $\int_\Omega f(y) G(x, y)\, dy = \int_\Omega \Phi(x-y) f(y)\, dy - \int_\Omega \phi(x, y) f(y)\, dy$.

                  theorem CM8.FundSolN_comp_sub_differentiableAt {n : } [Fact (2 n)] (x σ : Fin n) :
                  DifferentiableAt (fun (z : Fin n) => FundSolN (x - z)) σ

                  Differentiability of $z \mapsto \Phi(x - z)$ at any point $\sigma$.

                  theorem CM8.corrector_differentiableAt {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (x σ : Fin n) :

                  Differentiability of the corrector $\phi(x, \cdot)$ at any point $\sigma$.

                  theorem CM8.normalDeriv_G_decomp {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (x σ : Fin n) :
                  normalDeriv Ω (fun (z : Fin n) => gf.G x z) σ = normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ - normalDeriv Ω (gf.corrector x) σ

                  Normal-derivative decomposition $\nabla_{\hat N} G = \nabla_{\hat N} \Phi - \nabla_{\hat N} \phi$ inherited from $G(x, y) = \Phi(x - y) - \phi(x, y)$.

                  theorem CM8.surface_integral_G_decomp {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (g : (Fin n)) (x : Fin n) :
                  (surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (fun (z : Fin n) => gf.G x z) σ) = (surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (fun (z : Fin n) => FundSolN (x - z)) σ) - surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (gf.corrector x) σ

                  Surface-integral form of the Green-function decomposition: $\int_{\partial\Omega} g(\sigma) \nabla_{\hat N} G(x, \sigma)\, d\sigma$ splits as the $\Phi$-part minus the corrector $\phi$-part.

                  theorem CM8.green_representation {n : } [Fact (2 n)] (Ω : Set (Fin n)) (gf : GreenFunctionN n Ω) (u f g : (Fin n)) ( : IsOpen Ω) (hΩ_lip : IsLipschitzDomain Ω) (hu_reg : ContDiffOn 2 u Ω) (hu_cont : ContinuousOn u (closure Ω)) (hu_pde : xΩ, laplacian u x = f x) (hu_bdy : σfrontier Ω, u σ = g σ) (x : Fin n) (hx : x Ω) (hPhi_int : MeasureTheory.IntegrableOn (fun (y : Fin n) => FundSolN (x - y) * f y) Ω MeasureTheory.volume) (hcorr_int : MeasureTheory.IntegrableOn (fun (y : Fin n) => gf.corrector x y * f y) Ω MeasureTheory.volume) :
                  u x = (- (y : Fin n) in Ω, f y * gf.G x y) - surfaceIntegral Ω fun (σ : Fin n) => g σ * normalDeriv Ω (fun (z : Fin n) => gf.G x z) σ

                  Theorem 2.2 (Green-function representation for solutions of the boundary value Poisson equation): given a Green function $G$ for $\Omega$ and a solution $u$ of $\Delta u = f$ in $\Omega$ with $u = g$ on $\partial \Omega$, $$u(x) = -\int_\Omega f(y) G(x, y), dy

                  • \int_{\partial\Omega} g(\sigma) \nabla_{\hat N} G(x, \sigma), d\sigma.$$