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

Fill-distance control of the population PINN loss

Statement

For $d \geq 2$ , let $U \subset R^{d}$ and $Γ \subset R^{d}$ be measurable, and let $μ_{r}$ and $μ_{b}$ be probability measures on them. For positive integers $m_{r}, m_{b}$ , let the residual samples $x_{1}^{r}, \dots, x_{m_{r}}^{r}$ and boundary samples $x_{1}^{b}, \dots, x_{m_{b}}^{b}$ form $ε_{r}$ - and $ε_{b}$ -nets of $U$ and $Γ$ in Euclidean distance. Assume that for every center $x \in U$ and $y \in Γ$ , $μ_{r} ({\overline{B}}_{ε_{r}} (x) \cap U) \leq C_{r} ε_{r}^{d}, μ_{b} ({\overline{B}}_{ε_{b}} (y) \cap Γ) \leq C_{b} ε_{b}^{d - 1} .$ Suppose $[L [h]]_{α; U}$ , $[B [h]]_{α; Γ}$ , $[f]_{α; U}$ , and $[g]_{α; Γ}$ are finite, where $[v]_{α; E} = \sup_{x \neq y \in E} ∣ v (x) - v (y) ∣ / ∣ x - y ∣^{α}$ , with value zero when $E$ has fewer than two points. Let $λ_{r}, λ_{b} > 0$ , and use the population and empirical weighted-square PINN losses ${Loss}^{P I N N} (h; λ) = λ_{r} \int_{U} ∣ L [h] - f ∣^{2} d μ_{r} + λ_{b} \int_{Γ} ∣ B [h] - g ∣^{2} d μ_{b},$ ${Loss}_{m}^{P I N N} (h; λ) = \frac{λ_{r}}{m_{r}} \sum_{i = 1}^{m_{r}} ∣ L [h] (x_{i}^{r}) - f (x_{i}^{r}) ∣^{2} + \frac{λ_{b}}{m_{b}} \sum_{j = 1}^{m_{b}} ∣ B [h] (x_{j}^{b}) - g (x_{j}^{b}) ∣^{2} .$ Define $C_{m} = 3 \max {C_{r} m_{r} ε_{r}^{d}, C_{b} m_{b} ε_{b}^{d - 1}}, λ_{r, m}^{R} = \frac{3 λ_{r} ε_{r}^{2 α}}{C_{m}}, λ_{b, m}^{R} = \frac{3 λ_{b} ε_{b}^{2 α}}{C_{m}} .$ Then ${Loss}^{P I N N} (h; λ) \leq C_{m} {Loss}_{m}^{P I N N} (h; λ) + C_{m} (λ_{r, m}^{R} [L [h]]_{α; U}^{2} + λ_{b, m}^{R} [B [h]]_{α; Γ}^{2}) + 3 λ_{r} ε_{r}^{2 α} [f]_{α; U}^{2} + 3 λ_{b} ε_{b}^{2 α} [g]_{α; Γ}^{2} .$

For $d = 1$ , assume $μ_{r}$ is a probability measure on measurable $U \subset R$ , and $Γ$ is a nonempty finite measurable set with probability measure $μ_{b}$ , with every singleton ${y} \subseteq Γ$ measurable. Every point of $Γ$ is available deterministically. For a positive integer $m_{r}$ , let $x_{1}^{r}, \dots, x_{m_{r}}^{r}$ form an $ε_{r}$ -net of $U$ , and assume $μ_{r} ({\overline{B}}_{ε_{r}} (x) \cap U) \leq C_{r} ε_{r}$ for every center $x \in U$ . Suppose the same four Hölder seminorms are finite. Use the exact weighted boundary loss ${Loss}^{P I N N, b} (h; λ_{b}) = λ_{b} \int_{Γ} ∣ B [h] - g ∣^{2} d μ_{b} = λ_{b} \sum_{y \in Γ} μ_{b} ({y}) ∣ B [h] (y) - g (y) ∣^{2}$ and the empirical loss ${Loss}_{m}^{P I N N} (h; λ) = \frac{λ_{r}}{m_{r}} \sum_{i = 1}^{m_{r}} ∣ L [h] (x_{i}^{r}) - f (x_{i}^{r}) ∣^{2} + {Loss}^{P I N N, b} (h; λ_{b})$ . Set $C_{m} = 3 C_{r} m_{r} ε_{r}, λ_{r, m}^{R} = \frac{3 λ_{r} ε_{r}^{2 α}}{C_{m}}, λ_{b, m}^{R} = 0.$ Then ${Loss}^{P I N N} (h; λ) \leq C_{m} {Loss}_{m}^{P I N N} (h; λ) + C_{m} λ_{r, m}^{R} [L [h]]_{α; U}^{2} + 3 λ_{r} ε_{r}^{2 α} [f]_{α; U}^{2} .$ There is no random boundary term or boundary-data error term in this branch because the full boundary contribution is evaluated exactly.

Statement references

Shin et al., Appendix B, Lemmas B.1–B.2: deterministic fill-distance inequality

Shin et al., Appendix B, proof of Lemma B.1

Facts & Assumptions

Given: The trial function, residual and boundary operators, sample sets, fill distances, measures, and positive loss weights in the Statement.

[F1]

The population and empirical PINN losses use the weighted-square conventions in the local definition (Physics-informed residual loss and Hölder regularization).

[F2]

For $d \geq 2$ , the residual cells have mass at most $C_{r} ε_{r}^{d}$ and the boundary cells have mass at most $C_{b} ε_{b}^{d - 1}$ by the upper ball-mass assumptions. For $d = 1$ , each residual cell has mass at most $C_{r} ε_{r}$ by the residual upper ball-mass assumption in the Statement.

[F3]

The Hölder seminorm convention is $∣ v (x) - v (y) ∣ \leq [v]_{α; E} ∣ x - y ∣^{α}$ (Physics-informed residual loss and Hölder regularization).

[F4]

In the one-dimensional branch, the exact full-boundary empirical contribution equals the population boundary integral, and a finite union of sample-centered $ε_{r}$ -balls covers $U$ (Physics-informed residual loss and Hölder regularization, Finite and countable subadditivity of measures).

Proof

Proof strategy: integrate local collocation bounds over a measurable partition subordinate to the sampling balls.

1.1givenconstruct

Put $A_{i} = {\overline{B}}_{ε_{r}} (x_{i}^{r}) \cap U$ and $V_{i} = A_{i} ∖ ⋃_{k < i} A_{k}$ . The ball-mass assumptions make the $A_{i}$ measurable, and the net property makes the $V_{i}$ a measurable partition of $U$ subordinate to the sampling balls. For $d \geq 2$ , use the same construction on $Γ$ with the boundary balls to obtain cells $W_{j}$ ; for $d = 1$ , use every point of the finite boundary deterministically and make no boundary partition.

1.2givenF2F3algebra

By [F2], $μ_{r} (V_{i}) \leq C_{r} ε_{r}^{d}$ in the $d \geq 2$ branch and $μ_{r} (V_{i}) \leq C_{r} ε_{r}$ in the $d = 1$ branch. If $x \in V_{i}$ , the three-term square inequality and [F3] give $∣ L [h] (x) - f (x) ∣^{2} \leq 3 ∣ L [h] (x_{i}^{r}) - f (x_{i}^{r}) ∣^{2} + 3 ε_{r}^{2 α} [L [h]]_{α; U}^{2} + 3 ε_{r}^{2 α} [f]_{α; U}^{2} .$ For $d \geq 2$ , each boundary cell satisfies $μ_{b} (W_{j}) \leq C_{b} ε_{b}^{d - 1}$ , and its analogous local square bound holds.

2.1step 1.1step 1.2F1algebra

Integrate the residual inequality over the cells. The collocation terms contribute at most $3 C_{r} m_{r} ε_{r}^{d} λ_{r} m_{r}^{- 1} \sum_{i} ∣ L [h] (x_{i}^{r}) - f (x_{i}^{r}) ∣^{2}$ for $d \geq 2$ , and $3 C_{r} m_{r} ε_{r} λ_{r} m_{r}^{- 1} \sum_{i} ∣ L [h] (x_{i}^{r}) - f (x_{i}^{r}) ∣^{2}$ for $d = 1$ . The seminorm and data terms contribute $3 λ_{r} ε_{r}^{2 α} ([L [h]]_{α; U}^{2} + [f]_{α; U}^{2})$ because $μ_{r} (U) = 1$ .

2.2step 1.1step 1.2F1F4algebra

For $d \geq 2$ , integrating the boundary inequality gives the estimate with $3 C_{b} m_{b} ε_{b}^{d - 1}$ multiplying the empirical boundary term and $3 λ_{b} ε_{b}^{2 α} ([B [h]]_{α; Γ}^{2} + [g]_{α; Γ}^{2})$ for the remaining terms. For $d = 1$ , the weighted boundary term in the population loss is exactly ${Loss}^{P I N N, b} (h; λ_{b})$ from [F4].

3.1step 2.1step 2.2F4algebra∎

For $d \geq 2$ , by the definition of $C_{m}$ , the empirical residual and boundary coefficients in steps 2.1–2.2 are at most $C_{m}$ . The seminorm coefficients equal $C_{m} λ_{r, m}^{R}$ and $C_{m} λ_{b, m}^{R}$ by definition, while the data terms already have their displayed coefficients. Adding the estimates yields the result. For $d = 1$ , the net and upper ball-mass bound imply $1 = μ_{r} (U) \leq \sum_{i = 1}^{m_{r}} μ_{r} ({\overline{B}}_{ε_{r}} (x_{i}^{r}) \cap U) \leq m_{r} C_{r} ε_{r}$ , so $C_{m} \geq 3$ . Thus $C_{m}$ dominates the exact boundary term, the residual empirical coefficient from step 2.1 equals $C_{m}$ , and $C_{m} λ_{r, m}^{R} = 3 λ_{r} ε_{r}^{2 α}$ . Combining these bounds with the residual data term proves the one-dimensional inequality.

Depends on

Used by

Regularized PINN minimizers have vanishing residuals under sample refinement Theorem

Dependency tree · two levels

9 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

Shin, Darbon, and Karniadakis, On the Convergence of Physics-Informed Neural Networks for Linear Second-Order Elliptic and Parabolic Type PDEs (standard reference, not scraped)