LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Stability, collective compactness, and consistency of half-order product integration

Statement

Assume AC and let $a : [0, 1]^{2} \to R$ be continuous. For $K$ and $K_{n}$ from Piecewise-linear product integration for a half-order diagonal singularity, put $A : = ∥ a ∥_{\infty}$ and $h : = 1 / n$ . Then both operators are bounded linear maps from $X = C ([0, 1], R)$ to itself, $K$ is compact, and $(K_{n})$ is collectively compact and converges pointwise in norm to $K$ . Their product weights satisfy $w_{n, j} (x) \geq 0, \sum_{j = 0}^{n} ∣ w_{n, j} (x) ∣ = 2 \sqrt{x} + 2 \sqrt{1 - x} \leq 2 \sqrt{2}$ for every $x \in [0, 1]$ . If each $g_{x} (y) : = a (x, y) u (y)$ extends to a $C^{2}$ function on a neighborhood of $[0, 1]$ and $M_{2} : = \sup_{x, y} ∣ \partial_{y}^{2} g_{x} (y) ∣ < \infty$ , then $∥ K_{n} u - K u ∥_{\infty} \leq \frac{\sqrt{2}}{4} M_{2} h^{2} .$

Facts & Assumptions

Given: AC, continuous $a$ , the scalar functionals $S_{x}$ , hat functions $ϕ_{n, j}$ , and operators $K, K_{n}$ defined in the preceding item.

[A1]

The Axiom of Choice and AC supplies the countable and dependent choices used in Banach integration: AC supplies the two choice hypotheses of real Arzelà–Ascoli.

[F1]

Piecewise-linear product integration for a half-order diagonal singularity: $K_{n} u (x) = S_{x} (I_{n} g_{x})$ for $g_{x} (y) = a (x, y) u (y)$ , and $w_{n, j} (x) = S_{x} (ϕ_{n, j})$ .

[F2]

The half-order diagonal singularity defines a bounded improper integral: $S_{x}$ is positive, linear, and $∣ S_{x} (g) ∣ \leq 2 \sqrt{2} ∥ g ∥_{\infty}$ ; it is integration against $∣ x - y ∣^{- 1 / 2}$ in the improper-Riemann sense.

[F3]

Translations of the half-order kernel are continuous in the improper L1 norm: the finite modulus $τ (d) : = \sup_{∣ x - x^{'} ∣ \leq d} \int_{0}^{1} ∣ s (x - y) - s (x^{'} - y) ∣ d y$ tends to zero as $d ↓ 0$ .

[F4]

Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous: continuous $a$ and $g_{u} (x, y) = a (x, y) u (y)$ on the compact square are uniformly continuous.

[F5]

Arzelà--Ascoli for real $C (K)$ under Countable Choice and Dependent Choice: compact closure iff equicontinuous and pointwise bounded: under Countable Choice and Dependent Choice, an equicontinuous pointwise bounded family on $[0, 1]$ has compact closure in $X$ .

[F6]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ and Pointwise linear interpolation error from a second-derivative bound: for $g \in C^{2}$ on a neighborhood of a panel of width $h$ , the linear interpolant error is at most $\frac{1}{2} ∥ g^{''} ∥_{\infty} (y - y_{j}) (y_{j + 1} - y) \leq h^{2} ∥ g^{''} ∥_{\infty} / 8$ .

[F7]

$C (K, R)$ is complete in the supremum metric for every nonempty compact metric space $K$ : every continuous $a$ on the compact square is bounded, so $A : = ∥ a ∥_{\infty} < \infty$ .

[F8]

The interval $[0, 1]$ and square $[0, 1]^{2}$ with their Euclidean metrics are nonempty compact metric spaces (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).

[F9]

On the nonempty compact interval $[0, 1]$ (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), let $X = C ([0, 1], R)$ with its supremum norm. Pointwise addition and real scalar multiplication preserve continuity. The supremum is finite by $C (K, R)$ is complete in the supremum metric for every nonempty compact metric space $K$ ; the pointwise absolute-value inequalities give $∥ u + v ∥_{\infty} \leq ∥ u ∥_{\infty} + ∥ v ∥_{\infty}$ and $∥ c u ∥_{\infty} = ∣ c ∣ ∥ u ∥_{\infty}$ , and $∥ u ∥_{\infty} = 0$ holds exactly when $u = 0$ . Thus this is a real norm (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms). Its induced metric is the complete supremum metric of $C (K, R)$ is complete in the supremum metric for every nonempty compact metric space $K$ , so $X$ is Banach (Banach space).

[F10]

A linear map between normed spaces is bounded when a constant bounds its output norm by that constant times the input norm (A bounded linear operator between normed spaces).

[F11]

Additivity and scalar homogeneity of finite sums make the finite-sum interpolation formula linear in its input (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[F12]

A bounded linear operator is compact if the image of its closed unit ball has compact closure (Compact linear operator).

Proof

Given: AC, the definitions in [F1], $A = ∥ a ∥_{\infty}$ , $h = 1 / n$ , and $s (t) : = ∣ t ∣^{- 1 / 2}$ for $0 < ∣ t ∣ \leq 1$ .

1.1givenF1F2F7F8F9algebra

By [F8], the square is compact, so [F7] makes $A = ∥ a ∥_{\infty}$ finite. In the Banach normed space [F9], the hat functions in [F1] are nonnegative and on each panel the two adjacent hats add to $1$ , while all other hats vanish. Hence $\sum_{j = 0}^{n} ϕ_{n, j} = 1$ pointwise. Positivity and linearity in [F2] give $w_{n, j} (x) \geq 0$ and $\sum_{j} ∣ w_{n, j} (x) ∣ = \sum_{j} w_{n, j} (x) = S_{x} (1) = 2 \sqrt{x} + 2 \sqrt{1 - x} \leq 2 \sqrt{2} .$ For every $u \in X$ , the same bound shows $∥ K_{n} u ∥_{\infty} \leq 2 \sqrt{2} A ∥ u ∥_{\infty}$ .

1.2F3

For $d : = ∣ x - x^{'} ∣$ , [F3] gives an upper bound $τ (d)$ for the improper kernel translation integral, with $τ (d) \to 0$ as $d ↓ 0$ .

2.1F1F2F4step 1.1

For fixed $u$ , [F4] makes $(x, y) \mapsto g_{x} (y)$ uniformly continuous. By step 1.1 the hats are nonnegative and sum to $1$ , so on a panel $[y_{j}, y_{j + 1}]$ , $I_{n} g_{x} (y)$ is a convex combination of the two endpoint values. Hence $∥ I_{n} g_{x} - g_{x} ∥_{\infty} \to 0$ uniformly in $x$ , and the operator bound in [F2] yields $∥ K_{n} u - K u ∥_{\infty} \leq 2 \sqrt{2} ∥ I_{n} g_{x} - g_{x} ∥_{\infty} \to 0$ .

2.2F1F2F3F4F5F8F9F10F11F12A1step 1.1step 1.2

Write $g_{x} (y) = a (x, y) u (y)$ . The identities in [F1], the translation bound in [F3], and the operator bound in [F2] show $∣ K u (x) - K u (x^{'}) ∣ \leq A ∥ u ∥_{\infty} τ (d) + 2 \sqrt{2} ∥ u ∥_{\infty} ω_{a} (d),$ where $τ (d)$ is the translation bound from step 1.2 and $ω_{a} (d) : = \sup_{∣ x - x^{'} ∣ \leq d, y} ∣ a (x, y) - a (x^{'}, y) ∣ \to 0$ by [F4] on the compact square from [F8]. Replacing $g_{x}$ by $I_{n} g_{x}$ gives the same bound for $K_{n} u$ : by step 1.1 the interpolant is a convex combination of nodal values, so $∥ I_{n} g_{x} ∥_{\infty} \leq ∥ g_{x} ∥_{\infty}$ and $∥ I_{n} (g_{x} - g_{x^{'}}) ∥_{\infty} \leq ∥ g_{x} - g_{x^{'}} ∥_{\infty}$ . Thus $K$ and all $K_{n}$ map into $X$ and have a common equicontinuity modulus. The formula [F1] and linearity of $S_{x}$ in [F2] make $K$ linear; its operator bound follows from [F2]. Each $K_{n}$ is linear by [F11], and step 1.1 bounds it. By [F9] and [F10], both are bounded linear maps. Their images of the unit ball are uniformly bounded and equicontinuous. By [F5] and [A1], $K$ is compact by [F12], and $(K_{n})$ is collectively compact.

3.1F1step 2.2

For each fixed $n, j$ , take $a \equiv 1$ and $u = ϕ_{n, j}$ in the preceding continuity argument; then $K_{n} u (x) = w_{n, j} (x)$ , so each weight function is continuous. Consequently the coefficient functions $x \mapsto w_{n, j} (x) a (x, y_{j})$ in the finite-node representation are continuous.

4.1F2F6∎

Under the $C^{2}$ extension hypothesis, [F6] bounds $∥ I_{n} g_{x} - g_{x} ∥_{\infty} \leq M_{2} h^{2} / 8$ uniformly in $x$ . Applying [F2] gives $∥ K_{n} u - K u ∥_{\infty} \leq 2 \sqrt{2} M_{2} h^{2} / 8 = \sqrt{2} M_{2} h^{2} / 4$ .

Depends on

Used by

Fredholm error bound for half-order product integration Theorem

Dependency tree · two levels

100 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

Andreas Neubauer and Ronny Ramlau, Lecture Notes: Integral Equations and Boundary Value Problems, §3.3 (standard reference, not scraped)
Jiri Lebl, Basic Analysis I, §5.5 Improper Integrals (standard reference, not scraped)