LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Kernel Riemann sums converge uniformly on compact continuous-input sets

Statement

Let $d, d^{'} \in N$ with $d, d^{'} \geq 1$ , let $D \subset R^{d}$ be nonempty, bounded, and Jordan measurable, let $D^{'} \subset R^{d^{'}}$ be nonempty and bounded, let $κ \in C ({\overset{ˉ}{D}}^{'} \times \overset{ˉ}{D})$ be scalar-valued, and let $K \subset C (\overset{ˉ}{D})$ be nonempty and compact in the supremum norm. Give products of metric spaces the max metric. Let $Q_{n} : C (\overset{ˉ}{D}) \to R$ be bounded linear quadrature functionals with $\sup_{n} ∥ Q_{n} ∥ < \infty$ and $Q_{n} f \to \int_{D} f (y) d y$ for every $f \in C (\overset{ˉ}{D})$ . Then $\sup_{a \in K} \sup_{x \in {\overset{ˉ}{D}}^{'}} ∣ Q_{n} (κ (x, \cdot) a (\cdot)) - \int_{D} κ (x, y) a (y) d y ∣ ⟶ 0.$ This conclusion is in the supremum norm on the output variable. It does not by itself establish convergence in an arbitrary Banach output norm $U$ .

Statement references

Kovachki et al., Appendix E: compact-uniform approximation of the integral layers

Kovachki et al., Appendix E: Riemann sums on compact families of integrands

Facts & Assumptions

Given: The compact set $K$ , the continuous kernel $κ$ , and the quadrature functionals in the Statement.

[F1]

A compact metric space is totally bounded, so for every $δ > 0$ it has a finite $δ$ -net (A compact metric space is complete and totally bounded, and neither implication uses any choice principle, Finite $ε$ -net and totally bounded metric space).

[F2]

The hypotheses give pointwise convergence $Q_{n} f \to \int_{D} f$ on $C (\overset{ˉ}{D})$ and a uniform bound on the operator norms of $Q_{n}$ .

[F3]

Heine–Borel makes $\overset{ˉ}{D}$ and ${\overset{ˉ}{D}}^{'}$ compact. Finite products are compact in the product topology, which agrees with the topology of the max product metric because its balls are products of factor balls and such rectangles form a basis. The kernel is bounded and uniformly continuous on the compact metric product ${\overset{ˉ}{D}}^{'} \times \overset{ˉ}{D}$ , and each $a \in C (\overset{ˉ}{D})$ is bounded on $\overset{ˉ}{D}$ (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, A product of finitely many compact spaces is compact in the product topology, The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, Every continuous map from a nonempty compact Hausdorff space to a uniform space is uniformly continuous, A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value, The space $C (K, R)$ of continuous real-valued functions on a nonempty compact metric space).

[F4]

The continuous image of a compact metric space is compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset).

Proof

Proof strategy: direct finite-net argument.

1.1givenF3F4algebra

Define $Φ (x, a) = κ (x, \cdot) a (\cdot)$ on ${\overset{ˉ}{D}}^{'} \times K$ . For $(x, a), (x^{'}, a^{'})$ in this product, $∥ Φ (x^{'}, a^{'}) - Φ (x, a) ∥_{\infty} \leq ∥ κ ∥_{\infty} ∥ a^{'} - a ∥_{\infty} + ∥ a ∥_{\infty} \sup_{y \in \overset{ˉ}{D}} ∣ κ (x^{'}, y) - κ (x, y) ∣ .$ The constants are finite by [F3]. Given $η > 0$ , uniform continuity of $κ$ on ${\overset{ˉ}{D}}^{'} \times \overset{ˉ}{D}$ gives a positive $δ_{1}$ making the second term less than $η / 2$ when $∣ x^{'} - x ∣ < δ_{1}$ ; choosing $δ_{2} > 0$ with $∥ κ ∥_{\infty} δ_{2} < η / 2$ bounds the first term whenever $∥ a^{'} - a ∥_{\infty} < δ_{2}$ (if $∥ κ ∥_{\infty} = 0$ , that term is zero). Thus $Φ$ is continuous for the max product metric. The domain is compact by [F3], so [F4] makes its image $S$ compact.

1.2givenF2algebra

Put $M = 1 + \sup_{n} ∥ Q_{n} ∥ + ∣ D ∣ > 0$ . For any $f, g \in C (\overset{ˉ}{D})$ , $∣ Q_{n} (f) - \int_{D} f - Q_{n} (g) + \int_{D} g ∣ \leq M ∥ f - g ∥_{\infty},$ since $∣ \int_{D} (f - g) ∣ \leq ∣ D ∣ ∥ f - g ∥_{\infty}$ .

2.1step 1.1F1F2choose

Fix $ε > 0$ . Put $M = 1 + \sup_{n} ∥ Q_{n} ∥ + ∣ D ∣ > 0$ . By [F1] and step 1.1, choose a finite $ε / (3 M)$ -net $f_{1}, \dots, f_{J}$ for $S$ . For each $j$ , [F2] gives an index $n_{j}$ such that $∣ Q_{n} (f_{j}) - \int_{D} f_{j} ∣ < ε / 3$ whenever $n \geq n_{j}$ .

3.1step 1.2step 2.1algebra∎

Let $n \geq \max_{j} n_{j}$ and $f \in S$ . Choose $j$ with $∥ f - f_{j} ∥_{\infty} < ε / (3 M)$ . By [step 1.2] and the bound from [step 2.1], $∣ Q_{n} (f) - \int_{D} f ∣ \leq M ∥ f - f_{j} ∥_{\infty} + ∣ Q_{n} (f_{j}) - \int_{D} f_{j} ∣ + M ∥ f_{j} - f ∥_{\infty} < ε .$ Every $f \in S$ has this bound, so taking the supremum over $a \in K$ and $x \in {\overset{ˉ}{D}}^{'}$ proves the assertion.

Depends on

Used by

Neural-operator quadratures in the uniform norm and compatible Banach norms Theorem

Dependency tree · two levels

90 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

Kovachki et al., Neural Operator: Learning Maps Between Function Spaces With Applications to PDEs (standard reference, not scraped)