LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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.

A power above exponent minus one is Lebesgue integrable at zero

Statement

Assume the Axiom of Countable Choice. For $γ > - 1$ , define $g_{γ} (0) = 0$ and $g_{γ} (x) = x^{γ}$ for $0 < x \leq 1$ . Then $g_{γ}$ is Lebesgue measurable and integrable on $[0, 1]$ , with $\int_{[0, 1]} g_{γ} d λ = \frac{1}{γ + 1} .$

Facts & Assumptions

Given: Countable Choice and a real exponent $γ > - 1$ .

[A1]

The Axiom of Countable Choice ( ${A C}_{ω}$ ): every sequence of nonempty sets has a choice function; this is the assumption used by the construction of Lebesgue measure.

[F1]

Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume: under [A1], Lebesgue measure is a measure and gives each interval its length.

[F2]

Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable: under [A1], Borel sets are Lebesgue measurable. A nonnegative measurable function multiplied by the indicator of a measurable set remains measurable, and increasing limits of measurable functions are measurable (Closure properties of measurable functions used by the integral).

[F3]

The improper integral of a power at zero: for every $γ > - 1$ , $\lim_{ε ↓ 0} \int_{ε}^{1} x^{γ} d x = 1 / (γ + 1)$ .

[F4]

Continuity and derivatives of positive-base real powers: $x^{γ}$ is continuous on $(0, \infty)$ and has derivative $γ x^{γ - 1}$ there.

[F5]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : on a compact interval bounded away from zero, the integral of the derivative of a primitive equals its endpoint increment.

[F6]

Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ : a bounded function is Riemann integrable if Darboux upper and lower sums can be made arbitrarily close.

[F7]

A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral: a bounded Riemann-integrable function is Lebesgue measurable and its Lebesgue integral equals its Riemann integral.

[F8]

Monotone convergence for the integral: nonnegative measurable functions increasing pointwise to $g$ have integrals increasing to $\int g d λ$ .

[F9]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: $[1 / n, 1]$ is closed and bounded, hence compact, and the continuous power attains a finite maximum there.

Proof

1.1givenA1F2F4F6F9construct

For each integer $n \geq 2$ , define $g_{n} (x) = x^{γ}$ on $[1 / n, 1]$ and $g_{n} (x) = 0$ on $[0, 1 / n)$ . For every real $c$ , its strict superlevel is all of $[0, 1]$ if $c < 0$ , and $[1 / n, 1] \cap {x > 0 : x^{γ} > c}$ if $c \geq 0$ . The latter is Borel because the power is continuous on $(0, \infty)$ by [F4]; hence [F2] makes $g_{n}$ measurable, and $g_{n} \geq 0$ . By [F9], $x^{γ}$ is bounded on $[1 / n, 1]$ , so $g_{n}$ is bounded and continuous on each side of its only possible jump at $1 / n$ ; isolating that point in an interval of arbitrarily small length and using uniform continuity on the two remaining compact pieces makes its Darboux gap arbitrarily small, so [F6] gives Riemann integrability.

2.1F1F4F5F7step 1.1algebra

The equality of Riemann and Lebesgue integrals in [F7], followed by [F4] and [F5] on $[1 / n, 1]$ , gives $\int g_{n} d λ = \int_{1 / n}^{1} x^{γ} d x = (1 - n^{- (γ + 1)}) / (γ + 1)$ . The sequence $g_{n}$ is nondecreasing and converges pointwise to $g_{γ}$ .

3.1A1F1F2F3F8step 2.1∎

The increasing-limit clause of [F2] makes $g_{γ}$ measurable. Apply monotone convergence [F8] to the sequence $(g_{k + 1})_{k \geq 1}$ from step 2.1. Its integral limit is $1 / (γ + 1)$ by [F3], so $g_{γ}$ is integrable and the displayed value follows. The only choice assumption used is [A1], which supplies the underlying Lebesgue measure in [F1].

Depends on

Used by

The Jacobi weight defines a finite positive measure with full support Lemma

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

J. Lebl, Basic Analysis I, §5.4.1–5.4.2, The logarithm and the exponential (standard reference, not scraped)