ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generated

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.

Fredholm alternative for an integral equation

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $a < b$ be reals, let $K$ be $R$ or $C$ , let $k : [a, b] \times [a, b] \to K$ be continuous (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Continuity of a map of topological spaces at a point and globally) and let $g \in C ([a, b], K)$ . Write

$(K f) (x) : = \int_{a}^{b} k (x, y) f (y) d y,$

a compact operator on the Banach space $C ([a, b], K)$ with the supremum norm (Continuous kernel integral operator is compact on c of an interval, Banach space), and let $K^{*}$ be its transpose on the dual $C ([a, b], K)^{*}$ (The transpose of a bounded operator). Then:

the equation $f - K f = g$ has a solution $f \in C ([a, b], K)$ if and only if $φ (g) = 0$ for every $φ \in \ker (I - K^{*})$ ;
the equation has exactly one solution for every $g$ if and only if the homogeneous equation $f = K f$ has only the solution $f = 0$ .

Facts & Assumptions

[A1]

$[a, b]$ is a nonempty compact metric space (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line); $C ([a, b], R)$ with the supremum metric is complete ( $C (K, R)$ is complete in the supremum metric for every nonempty compact metric space $K$ ), and a uniform limit of continuous real functions is continuous (The uniform limit of continuous real-valued functions on a metric space is continuous).

[A2]

On $C ([a, b], K)$ the supremum norm $∥ f ∥_{\infty} = \sup_{x} ∣ f (x) ∣$ makes it a normed space, using the real definition when $K = R$ and the complex norm definition when $K = C$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms, Complex norm and complex normed space); for complex-valued functions $∣ f ∣ \leq ∣ Re f ∣ + ∣ Im f ∣$ and both parts are bounded by $∣ f ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, Real and imaginary parts, complex conjugation, and modulus); a metric space is complete when every Cauchy sequence converges (Complete metric space: every Cauchy sequence converges in the space, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[A3]

$K$ is a compact operator on $C ([a, b], K)$ (Continuous kernel integral operator is compact on c of an interval), and $K$ is a Banach space by finite-dimensional completeness (Every finite-dimensional normed space is Banach, Banach space); $A^{*} = I - K^{*}$ for $A = I - K$ (Transposition reverses composition, The transpose of a bounded operator).

[A4]

Assume AC. For a compact operator $C$ on a Banach space $X$ , the operator $I - C$ is injective if and only if it is surjective, and then boundedly invertible; and for $y \in X$ the equation $(I - C) x = y$ is solvable exactly when $φ (y) = 0$ for every $φ$ in the kernel of the transpose (Fredholm alternative for identity minus compact); the implications are the statement of the alternative, and $A C$ supplies ${A C}_{ω}$ and $D C$ (AC supplies the countable and dependent choices used in Banach integration, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain).

Verification

technique · direct

Given: $A C$ , reals $a < b$ , $K \in {R, C}$ , a continuous kernel $k$ on $[a, b]^{2}$ , the integral operator $K$ on $C ([a, b], K)$ with the supremum norm, its transpose $K^{*}$ , and $g \in C ([a, b], K)$ .

1.1A1A2

$C ([a, b], R)$ with the supremum norm is a Banach space, being complete by [A1] and normed by [A2].

1.2A2algebra

$C ([a, b], C)$ with the supremum norm is a Banach space: a sequence $(f_{j})$ is Cauchy for the supremum norm exactly when the real sequences $(Re f_{j})$ and $(Im f_{j})$ are Cauchy, by the two inequalities of [A2]; those have continuous limits $u, v$ by [A1], and then $∥ f_{j} - (u + i v) ∥_{\infty} \leq ∥ Re f_{j} - u ∥_{\infty} + ∥ Im f_{j} - v ∥_{\infty} \to 0$ ; the norm axioms hold by [A2].

1.3A3

The transpose of $I - K$ is $I - K^{*}$ , by [A3].

2.1step 1.1step 1.2A3

In either scalar field, $K$ is a compact operator on the Banach space $C ([a, b], K)$ , by [step 1.1], [step 1.2] and [A3].

3.1step 2.1step 1.3A4

Claim 1: by [A4] applied to the compact operator $K$ on the Banach space $C ([a, b], K)$ , the equation $f - K f = g$ is solvable exactly when $φ (g) = 0$ for every $φ$ in the kernel of $(I - K)^{*}$ , which is $\ker (I - K^{*})$ by [step 1.3].

3.2step 2.1A4

Claim 2: the equation $f - K f = g$ has exactly one solution for every $g$ exactly when $I - K$ is a bijection, which by [A4] is equivalent to injectivity of $I - K$ , that is, to the homogeneous equation $f = K f$ having only the zero solution.

4.1step 3.1step 3.2∎

The two displayed claims are [step 3.1] and [step 3.2].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

123 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, Topics in Real and Functional Analysis, version November 17, 2017 — §6.5 p.189, Theorem 6.30 and its integral-equation discussion (standard reference, not scraped)
Theo Bühler and Dietmar Salamon, Functional Analysis — §4.4 p.198, Remark 4.42 (standard reference, not scraped)