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.
Closure properties of measurable functions used by the integral
Statement
Let be a measure space.
- If are measurable and is defined pointwise, then is measurable.
- If and is measurable, then is measurable.
- If is measurable, then , , and are measurable.
- If and is measurable, then is measurable, where this function equals on and off (in particular, here).
- If is a sequence of measurable functions , then is measurable; if moreover pointwise, then is measurable.
Facts & Assumptions
Given: A measure space and functions or sets as in the relevant clause.
A function is measurable exactly when for every real (Extended-real-valued measurable functions).
A sigma-algebra contains and and is closed under complements and countable unions; countable intersections follow by taking complements (Sigma-algebras).
The rationals are countable and dense in the reals ( is countably infinite, Both and are dense in , and every nonempty open subset of is uncountable).
Proof
For any extended-real-valued , the identities and follow from rational density, including when is infinite. Thus [L2] and [L3] show that measurability of all strict sublevels is equivalent to measurability of all strict superlevels.
Put as defined in clause 4. For , , since . For , . Both sets are measurable, including at , so clause 4 follows.
For a pointwise-defined sum, . Indeed, if both summands are finite and their sum exceeds , choose a rational strictly between and . If one summand is , the other is not , and a rational meeting the two inequalities still exists; if a summand is , the defined sum cannot exceed . The reverse inclusion follows by adding the inequalities. The union is countable and measurable, proving clause 1.
For , ; for , . If , each superlevel is either or . Step 1.1 and [L1] therefore prove clause 2.
Put and . The defining order properties of infimum and supremum give and , including infinite values. By step 1.1 and [L2] these sets are measurable, so and are measurable by [L1]. If , then pointwise. This proves clause 5.
The function is measurable by step 2.1. For any real-valued measurable , the superlevel of is when and when . Apply this to and to obtain measurable and . They are finite-valued, so step 1.3 makes measurable, proving clause 3.
Clauses 1–5 follow respectively from steps 1.3, 2.1, 3.1, 1.2, and 2.2.
Depends on
Used by
- Additivity of the nonnegative Lebesgue integral Corollary
- Beppo Levi's theorem for nonnegative series Corollary
- Polar integration may discard the cut locus Corollary
- Reverse Fatou's lemma under an integrable majorant Corollary
- Complex L^∞ space of a locally compact group Definition
- Integrable real and complex functions, and their integrals Definition
- Integral over a measurable subset Definition
- Wiener measure on continuous path space Definition
- A bounded Riemann integrable function admits Borel Darboux envelopes with the same Lebesgue integral Lemma
- A Caratheodory integrand composed with measurable functions is measurable Lemma
- Borel sigma-algebra of continuous path space is generated by coordinates Lemma
- Conditional expectation is unique almost surely Lemma
- Conditioning a known state and independent noise Lemma
- Generic evaluation of bounded measurable functions by rational cuts Lemma
- K-type eigenvalues of A(nu): recurrence, closed form and nonvanishing Lemma
- L1 of a second-countable locally compact group is separable Lemma
- Solovay densities and localized small null joins Lemma
- The essential supremum is attained as the least essential bound Proposition
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral Theorem
- A complex L¹ density defines a complex measure whose total variation is |h| dmu Theorem
- A real L¹ density defines a finite signed measure with its canonical Hahn and Jordan data Theorem
- Basic algebra and order properties of conditional expectation Theorem
- Change of variables for expectation Theorem
- Conditional monotone convergence Theorem
- Every nonnegative measurable function is the increasing limit of simple measurable functions Theorem
- Fatou's lemma Theorem
- Fekete–Szegő equality of logarithmic capacity, transfinite diameter, and Chebyshev constant Theorem
- First-step equations for nonnegative exit costs Theorem
- Integrating against a density agrees with integrating the product Theorem
- Lᵖ and L^∞ are vector spaces for p ≥ 1 Theorem
- Measurability of integration against a kernel Theorem
- Riesz-Fischer completeness of Lᵖ for 1 ≤ p ≤ ∞ Theorem
- The Lebesgue integral is linear on L¹(μ) Theorem
- The Lᵖ distance for 0 < p < 1 is a complete translation-invariant metric Theorem
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
- Richard F. Bass, Real Analysis for Graduate Students, Proposition 6.3 (standard reference, not scraped)
- John K. Hunter, Measure Theory Notes, Chapter 3, Propositions 3.5–3.7 and Theorem 3.8 (standard reference, not scraped)