ExampleConstruction: Literature-sourcedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27

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 function $x^{- 1 / 2}$ on $(0, 1]$ is unbounded and integrable

Example

The function $f (x) = x^{- 1 / 2}$ on $(0, 1]$ is unbounded near $0$ but belongs to $L^{1} ((0, 1], λ)$ .

Facts & Assumptions

Given: The function $f (x) = x^{- 1 / 2}$ on $(0, 1]$ .

[L1]

Monotone convergence holds for the nonnegative integral (Monotone convergence for the integral).

[L2]

Intervals have the expected Lebesgue measure (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[L3]

The geometric series with ratio $2^{- 1 / 2}$ converges (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L4]

The nonnegative integral is additive on measurable sets (Additivity of the nonnegative Lebesgue integral).

Verification

technique · direct

1.1

On the dyadic interval $I_{k} : = (2^{- k - 1}, 2^{- k}]$ , one has $f (x) \leq 2^{(k + 1) / 2}$ and $λ (I_{k}) = 2^{- k - 1}$ .

L2constructalgebra

Hence

$\int_{I_{k}} f d λ \leq 2^{(k + 1) / 2} 2^{- k - 1} = 2^{- (k + 1) / 2} .$

2.1

The partial sums of the integrals over $⋃_{k < n} I_{k} = (2^{- n}, 1]$ are bounded by $\sum_{k < n} 2^{- (k + 1) / 2}$ .

step 1.1L1L3L4

That series converges by [L3]. Since $f χ_{(2^{- n}, 1]} ↑ f$ , [L1] and [L4] give $\int_{0}^{1} x^{- 1 / 2} d λ < + \infty$ . The pointwise values $f (2^{- m}) = 2^{m / 2}$ show that $f$ is unbounded. [step 1.1, L1, L3, L4] ∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

37 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

John K. Hunter, Measure Theory Notes, Chapter 4 (standard reference, not scraped)

The function x−1/2x−1/2 on (0,1](0,1] is unbounded and integrable