ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

One-dimensional Dirichlet Green kernel on an interval

Statement

Assume the Axiom of Countable Choice. For $a < b$ and $x, y \in (a, b)$ , the one-dimensional Dirichlet kernel for $- d^{2} / d x^{2}$ is $G (x, y) = ((\min {x, y} - a) (b - \max {x, y})) / (b - a)$ . It is symmetric, nonnegative, vanishes at $a, b$ , and its $x$ -derivative has jump $\partial_{x} G (y +, y) - \partial_{x} G (y -, y) = - 1$ , so $- \partial_{x}^{2} G (\cdot, y) = δ_{y}$ in $D^{'} (a, b)$ . Its difference from $- ∣ x - y ∣ / 2$ is affine in $x$ . The stated Countable Choice assumption is used for the named Lebesgue-measure and regular-distribution interfaces below; no full Axiom of Choice is used.

Facts & Assumptions

Given: Assume ${A C}_{ω}$ , let $a < b$ , fix $y \in (a, b)$ , and put $L = b - a > 0$ . The differential operator is $- d^{2} / d x^{2}$ .

[A1]

Countable Choice is written ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). It enters through the Borel-to-Lebesgue, finite-interval measure, Riemann-to-Lebesgue, and published locally-integrable-to-distribution interfaces used in steps 2.2, 3.2 and 6.1. The piecewise slope and integration-by-parts calculations themselves make no choice.

[F1]

For two real numbers the minimum and maximum select the lesser and greater values (Maximum and minimum of a set).

[F2]

The one-dimensional normalized kernel is $Φ_{1} (x) = - ∣ x ∣ / 2$ ; the assigned Laplace definition separately verifies $- Φ_{1}^{''} = δ_{0}$ (Fundamental solution for the positive operator minus Laplacian). A fundamental solution of $L$ is a distribution $E$ with $L E = δ_{0}$ , and its translated distribution has source $δ_{y}$ (Fundamental solution of a constant-coefficient operator).

[F3]

A test function on $(a, b)$ has compact support in that open interval, so its zero extension is smooth on $R$ and it vanishes near both endpoints (Test function space d of an open set).

[F4]

The distributional second derivative satisfies $⟨ \partial_{x}^{2} T, φ ⟩ = ⟨ T, φ^{''} ⟩$ (Distributional derivative).

[F5]

The Dirac distribution satisfies $δ_{y} (φ) = φ (y)$ (Dirac delta and its derivatives).

[F6]

If $u, v$ are differentiable on a closed interval and their derivatives are integrable, integration by parts gives $\int u v^{'} = [u v] - \int u^{'} v$ (If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ). The statement is real-valued; apply it to the real and imaginary parts of a complex test separately.

[F7]

A continuous real function on a closed bounded interval is Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[F8]

The Riemann integral is additive over adjacent subintervals (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[F9]

Under ${A C}_{ω}$ , every bounded Riemann-integrable function on a closed bounded interval is Lebesgue integrable there with the same integral (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[F10]

A continuous map has Borel preimages of Borel sets, and under ${A C}_{ω}$ Borel functions on $R$ are Lebesgue measurable (A continuous map has Borel preimages of Borel sets, Borel measurable and Lebesgue measurable functions on $R^{n}$ ).

[F11]

Under ${A C}_{ω}$ , the interval $[a, b]$ is measurable and $λ_{1} ([a, b]) = b - a$ (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included). The nonnegative integral is monotone and positively homogeneous (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[F12]

A measurable complex function is integrable when its absolute value has finite integral (Integrable real and complex functions, and their integrals); local integrability is defined by finite absolute integrals on balls or, on an open set, on each compact subset (A locally integrable function on $R^{n}$ , Regular distribution from a locally integrable function).

[F13]

A locally integrable function defines the regular functional $⟨ u_{f}, φ ⟩ = \int f φ$ (Regular distribution from a locally integrable function).

[F14]

Under ${A C}_{ω}$ , this regular functional is a distribution (Locally integrable functions embed in distributions).

Proof

technique · direct

1.1givenF1algebra

Let $G_{y} (x) = G (x, y)$ on $(a, b)$ and extend it by zero off $(a, b)$ , including the endpoint values. By [F1], its branches on $[a, y]$ and $[y, b]$ are $(x - a) (b - y) / L$ and $(y - a) (b - x) / L$ . They agree at $x = y$ , both giving $(y - a) (b - y) / L$ , and vanish at $a, b$ , so the extension is continuous and compactly supported. Swapping $x, y$ leaves the min/max formula unchanged. Both factors are nonnegative on either branch, and their sum is at most $L$ , so their product is at most $L^{2} / 4$ ; hence $G_{y}$ is symmetric, nonnegative, bounded by $L / 4$ , and $G_{y} (y) > 0$ .

2.1step 1.1algebra

On $x < y$ and $x > y$ , respectively, the affine branches from step 1.1 have one-sided derivatives $s_{-} : = \partial_{x} G (y -, y) = (b - y) / L$ and $s_{+} : = \partial_{x} G (y +, y) = - (y - a) / L$ . Therefore $s_{+} - s_{-} = - ((y - a) + (b - y)) / L = - 1$ .

2.2A1F10F11F12step 1.1algebra

The continuous compactly supported extension $G_{y}$ is Borel by [F10] and hence Lebesgue measurable under [A1]. It is supported in $[a, b]$ and bounded by $L / 4$ by step 1.1. By [F11], $\int_{R} ∣ G_{y} ∣ d λ_{1} \leq (L / 4) λ_{1} ([a, b]) = L^{2} / 4 < \infty$ . Thus it is integrable and its restriction is locally integrable on $(a, b)$ by [F12] and monotonicity of the nonnegative integral. This is the exact measure-side use of ${A C}_{ω}$ .

3.1F2step 1.1step 2.1algebra

By [F2], the one-dimensional free-space fundamental profile translated to $y$ is $- ∣ x - y ∣ / 2$ . For $x < y$ , $G_{y} (x) + ∣ x - y ∣ / 2$ is affine with slope $s_{-} - 1 / 2$ ; for $x > y$ it is affine with slope $s_{+} + 1 / 2$ . Step 2.1 makes those slopes equal, and step 1.1 gives continuity at $y$ , so the two pieces form one affine function on $(a, b)$ .

3.2A1F13F14step 2.2

The locally integrable function $G_{y}$ defines the regular functional $T_{y} (φ) = \int_{(a, b)} G_{y} (x) φ (x) d x$ by [F13], and [F14] makes $T_{y}$ a distribution under ${A C}_{ω}$ . No full Axiom of Choice is used.

4.1F3F6F7step 3.2step 2.1

Fix a real-valued $φ \in D (a, b)$ . By [F3], $φ$ vanishes near $a$ . On $[a, y]$ , apply [F6] first with $u = G_{y}, v = φ^{'}$ and then with $u = s_{-}, v = φ$ ; the functions and derivatives involved are continuous and integrable by [F7]. This gives $\int_{a}^{y} G_{y} φ^{''} = [G_{y} φ^{'}]_{a}^{y} - s_{-} [φ]_{a}^{y} = G_{y} (y) φ^{'} (y) - s_{-} φ (y)$ .

5.1F3F6F7step 4.1step 2.1

Since $φ$ also vanishes near $b$ , the same two applications of [F6] on $[y, b]$ , with slope $s_{+}$ , give $\int_{y}^{b} G_{y} φ^{''} = [G_{y} φ^{'}]_{y}^{b} - s_{+} [φ]_{y}^{b} = - G_{y} (y) φ^{'} (y) + s_{+} φ (y)$ .

6.1A1F4F5F8F9F13step 2.1step 4.1step 5.1∎

By [F8], the two Riemann integrals from steps 4.1 and 5.1 sum to the Riemann integral on $[a, b]$ ; by [F9] and [A1], this equals the Lebesgue integral that gives $T_{y} (φ^{''})$ , since $φ$ vanishes near the endpoints. The terms at $y$ cancel, and step 2.1 gives $T_{y} (φ^{''}) = (s_{+} - s_{-}) φ (y) = - φ (y)$ . Apply this real calculation to the real and imaginary parts of a complex test. By [F4], [F5] and [F13], $⟨ - \partial_{x}^{2} T_{y}, φ ⟩ = - ⟨ T_{y}, φ^{''} ⟩ = φ (y) = ⟨ δ_{y}, φ ⟩$ . Thus $- \partial_{x}^{2} G (\cdot, y) = δ_{y}$ in $D^{'} (a, b)$ .

Source notes

Hunter, §2.6 equation (2.13), printed p. 33 (PDF p. 39), gives the free-space one-dimensional profile $Γ (x) = - ∣ x ∣ / 2$ ; the discussion on printed p. 40 (PDF p. 46) writes the corresponding whole-line potential for $- u^{''} = f$ . Teschl, §5.4 Problem 5.21, printed p. 129 (PDF p. 142), asks the reader to find the Green function for an interval but supplies neither its formula nor a solution. The piecewise Dirichlet formula, its endpoint and symmetry checks, and the distributional jump computation above are derived directly; the sources supply context and normalization, not this proof.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

99 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (2014) (standard reference, not scraped)