LemmaStatement: AI-adaptedProof: 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.

The half-order diagonal singularity defines a bounded improper integral

Statement

For $x \in [0, 1]$ , $g \in C ([0, 1], R)$ , and $0 < ε < 1$ , let $S_{x, ε} (g) : = \int_{[0, 1] ∖ (x - ε, x + ε)} ∣ x - y ∣^{- 1 / 2} g (y) d y,$ where the integral is the sum of the ordinary Riemann integrals on the at most two remaining closed intervals, and an empty interval contributes zero. The limit $S_{x} (g) : = \lim_{ε ↓ 0} S_{x, ε} (g)$ exists. The map $S_{x} : C ([0, 1], R) \to R$ is linear and positive, and its operator norm (The operator norm as the least bound and as the unit-sphere or unit-ball supremum) is $∥ S_{x} ∥ = S_{x} (1) = 2 \sqrt{x} + 2 \sqrt{1 - x} \leq 2 \sqrt{2} .$

Facts & Assumptions

Given: $x \in [0, 1]$ , $g \in C ([0, 1], R)$ , and the truncated Riemann integrals $S_{x, ε} (g)$ from the Statement.

[F1]

Riemann–Stieltjes sums, upper and lower sums, and the Riemann–Stieltjes integral: $\int_{a}^{b}$ denotes the ordinary Riemann integral, realized as the Riemann–Stieltjes integral with the identity integrator.

[F2]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous real-valued function on each remaining closed interval has an ordinary Riemann integral.

[F3]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : pointwise inequalities between integrable functions on an interval pass to their integrals.

[F4]

The two FTC forms for a Riemann–Stieltjes integral with a $C^{1}$ integrator: for the identity integrator, an antiderivative evaluates the integral; since $(2 \sqrt{r})' = r^{- 1 / 2}$ on $r > 0$ , $\int_{δ}^{ε} r^{- 1 / 2} d r = 2 (\sqrt{ε} - \sqrt{δ})$ for $0 < δ < ε$ .

[F5]

The reals are complete: every Cauchy sequence of real numbers converges.

[F6]

Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ : finite Riemann integrals are linear in their integrands.

[F7]

$C (K, R)$ is complete in the supremum metric for every nonempty compact metric space $K$ : every continuous real-valued function on $[0, 1]$ is bounded, so $M : = ∥ g ∥_{\infty}$ is finite.

[F8]

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$ : integrals over disjoint intervals add when an interval is split at its endpoints.

[F9]

The interval $[0, 1]$ with its usual metric 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).

[F10]

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).

[F11]

The operator norm of a bounded linear map is the supremum of its values on the closed unit ball (The operator norm as the least bound and as the unit-sphere or unit-ball supremum).

Proof

Given: The data in the Statement, $M : = ∥ g ∥_{\infty}$ , and $0 < δ < ε < 1$ .

1.1givenF1F2F7F9

By [F9], [F7] applies and $M = ∥ g ∥_{\infty}$ is finite. The integrand $y \mapsto ∣ x - y ∣^{- 1 / 2} g (y)$ is continuous on each closed interval in $[0, 1] ∖ (x - ε, x + ε)$ , because that set stays away from $x$ . Thus the truncated integrals are finite and defined by [F1].

1.2givenF2F3F4F5F8algebra

For $m \geq 2$ , put $a_{m} : = S_{x, 1 / m} (g)$ . By [F8], the difference $a_{m} - a_{ℓ}$ integrates only over the two annuli between the cutoffs $1 / m$ and $1 / ℓ$ . On each annulus, $∣ g (y) ∣ \leq M$ ; by [F2] and [F3], its absolute integral is bounded by $M \int_{\min (1 / m, 1 / ℓ)}^{\max (1 / m, 1 / ℓ)} r^{- 1 / 2} d r$ . Adding at most two sides gives $∣ a_{m} - a_{ℓ} ∣ \leq 4 M ∣ m^{- 1 / 2} - ℓ^{- 1 / 2} ∣$ , so $(a_{m})$ is Cauchy and has a limit $L$ by [F5]. For any $ε > 0$ , choose $m$ with $1 / m < ε$ ; comparing the two cutoffs gives $∣ S_{x, ε} (g) - a_{m} ∣ \leq 4 M \sqrt{ε}$ . Letting $m \to \infty$ along such choices yields $∣ S_{x, ε} (g) - L ∣ \leq 4 M \sqrt{ε}$ , so $S_{x, ε} (g) \to L$ as $ε ↓ 0$ .

2.1givenF3F4F8step 1.2algebra

For every $ε$ , comparison on the left and right of $x$ with the positive function $r^{- 1 / 2}$ gives $∣ S_{x, ε} (g) ∣ \leq M (2 \sqrt{x} + 2 \sqrt{1 - x}) .$ Taking the limit from step 1.2 proves the same bound for $S_{x} (g)$ . For $g = 1$ , the truncated integrals increase to the sum of the two endpoint integrals by [F8], so $S_{x} (1) = 2 \sqrt{x} + 2 \sqrt{1 - x}$ . Since $(2 x - 1)^{2} \geq 0$ , we have $2 \sqrt{x (1 - x)} \leq 1$ , and therefore $S_{x} (1)^{2} = 4 (1 + 2 \sqrt{x (1 - x)}) \leq 8$ . Thus $S_{x} (1) \leq 2 \sqrt{2}$ .

3.1F3F6F9F10F11step 2.1algebra∎

Each truncated functional is linear and nonnegative on nonnegative $g$ ; limits preserve those equalities and inequalities, so $S_{x}$ is linear and positive. By [F10] it is a linear functional on a normed space. Step 2.1 gives $∣ S_{x} (g) ∣ \leq S_{x} (1) ∥ g ∥_{\infty}$ , and the input $g = 1$ attains equality; [F11] therefore gives $∥ S_{x} ∥ = S_{x} (1)$ .

Depends on

Used by

Dependency tree · two levels

104 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

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