LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 Caratheodory integrand composed with measurable functions is measurable

Statement

Assume Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Ω \subseteq R^{n}$ be Lebesgue measurable and let $f : Ω \times R \times R^{n} \to R$ be a Caratheodory integrand: for every $(s, ξ) \in R \times R^{n}$ the map $x \mapsto f (x, s, ξ)$ is measurable (Borel measurable and Lebesgue measurable functions on $R^{n}$ ), and for almost every $x \in Ω$ the map $(s, ξ) \mapsto f (x, s, ξ)$ is continuous. If $u : Ω \to R$ and $w : Ω \to R^{n}$ are measurable, then $x \mapsto f (x, u (x), w (x))$ is measurable.

Facts & Assumptions

Given: Countable Choice; a Lebesgue measurable set $Ω \subseteq R^{n}$ ; a Caratheodory integrand $f : Ω \times R \times R^{n} \to R$ , so that $x \mapsto f (x, s, ξ)$ is measurable for every $(s, ξ) \in R \times R^{n}$ and $(s, ξ) \mapsto f (x, s, ξ)$ is continuous for almost every $x \in Ω$ ; measurable maps $u : Ω \to R$ and $w : Ω \to R^{n}$ . Throughout, $Ω$ carries the trace of the Lebesgue sigma-algebra and the restricted Lebesgue measure, and $N : = {x \in Ω : (s, ξ) \mapsto f (x, s, ξ) is not continuous}$ satisfies $∣ N ∣ = 0$ .

[F1]

Every real-valued measurable function is the pointwise limit everywhere of a sequence of real-valued simple functions (Every measurable function admits simple approximations dominated by its absolute value).

[F2]

Measurable real-valued functions are closed under finite sums, real scalar multiplication, positive and negative parts, and multiplication by measurable indicators. Countable infima and increasing suprema of measurable extended-real functions are measurable; thus ${lim inf}_{k} g_{k} = \sup_{m} \inf_{k \geq m} g_{k}$ is extended-real measurable and need not be finite (Closure properties of measurable functions used by the integral).

[F3]

For a map into $R^{m}$ , measurability means that preimages of Borel sets are measurable in the domain, and when $m = 1$ this is the usual notion of a real-valued measurable function (Borel measurable and Lebesgue measurable functions on $R^{n}$ ); under the ambient Axiom of Countable Choice this is the Lebesgue sigma-algebra framework used throughout.

[F4]

The Lebesgue measure space is complete: every subset of a Lebesgue null set is Lebesgue measurable (Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume).

Proof

technique · direct, by approximation with measurable simple functions and passage to the pointwise limit

1.1F3

Measurability of $u$ and of the coordinates of $w$ . For every $a \in R$ and every coordinate index $i$ the set ${ξ \in R^{n} : ξ_{i} > a}$ is Borel, so $(w^{i})^{- 1} ((a, \infty)) = w^{- 1} ({ξ_{i} > a})$ is measurable in $Ω$ by [F3]; hence each coordinate function $w^{i}$ of $w$ is real-valued measurable, and so is $u$ .

2.1F1step 1.1

Simple approximants. By [F1] applied to $u$ there are simple functions $u_{k} : Ω \to R$ with $u_{k} \to u$ pointwise on $Ω$ , and by [F1] applied to each coordinate $w^{i}$ there are simple functions $s_{k}^{i}$ with $s_{k}^{i} \to w^{i}$ pointwise. Setting $w_{k} : = (s_{k}^{1}, \dots, s_{k}^{n})$ gives, for each $k$ , a map with finitely many values that converges to $w$ pointwise.

3.1F2step 2.1

Measurability of the composed approximations. Fix $k$ and write $u_{k} = \sum_{i = 1}^{I} a_{i} 1_{E_{i}}$ and $w_{k} = \sum_{j = 1}^{J} b_{j} 1_{F_{j}}$ with pairwise disjoint measurable sets $E_{i}, F_{j}$ covering $Ω$ . For each pair $(i, j)$ the map $x \mapsto f (x, a_{i}, b_{j})$ is measurable by the first Caratheodory clause, so $x \mapsto f (x, a_{i}, b_{j}) 1_{E_{i} \cap F_{j}} (x)$ is measurable by the indicator clause of [F2] applied to its positive and negative parts; the finite sum $g_{k} : = \sum_{i, j} f (x, a_{i}, b_{j}) 1_{E_{i} \cap F_{j}}$ is therefore measurable [F2]. Since the $E_{i}$ and the $F_{j}$ partition $Ω$ , one has $g_{k} (x) = f (x, u_{k} (x), w_{k} (x))$ for every $x$ .

4.1F2step 2.1step 3.1

The limit inferior. On $Ω ∖ N$ the map $(s, ξ) \mapsto f (x, s, ξ)$ is continuous, so $g_{k} (x) = f (x, u_{k} (x), w_{k} (x)) \to f (x, u (x), w (x))$ there by step 2.1. Hence the extended-real measurable function $g : = {lim inf}_{k} g_{k}$ , which exists by [F2], satisfies $g (x) = f (x, u (x), w (x))$ for every $x \in Ω ∖ N$ .

5.1F4step 4.1∎

Conclusion. The function $x \mapsto f (x, u (x), w (x))$ differs from the measurable function $g$ only on the null set $N$ . For a Borel set $B \subseteq R$ (also Borel in $\overline{R}$ ) its preimage is the union of ${g \in B} ∖ N$ , which is measurable, and a subset of $N$ , which is measurable by the completeness of Lebesgue measure [F4]. So $x \mapsto f (x, u (x), w (x))$ is measurable.

Depends on

Used by

Dependency tree · two levels

32 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

Francesco Paolo Maiale (course by Giovanni Alberti), Lecture Notes Calculus of Variations A, University of Pisa (last update 21 August 2019; complete 149-page notes) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2026 author manuscript; complete 392-page archived text) (standard reference, not scraped)