Alphabeta MathHow 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.
Nonnegative simple measurable functions
Definition
Let be a measure space. A measurable function (Extended-real-valued measurable functions) is a nonnegative simple measurable function when it has finite range.
Equivalently, there are pairwise disjoint measurable sets and coefficients such that Any such display is a simple representation of .
Depends on
Used by
- The integral of a nonnegative simple function Definition
- The nonnegative Lebesgue integral Definition
- Negative drift gives a finite mean small-set hit Example
- A topological invariant mean yields norm-approximately invariant densities Lemma
- Counting measure on a discrete group is Haar, Haar measures there are its multiples, and integrals against them are sums Lemma
- Følner nets give Reiter nets Lemma
- L1 of a second-countable locally compact group is separable Lemma
- Bounded Dirichlet problem for hitting probabilities Theorem
- Compact groups have property (T) by Haar averaging Theorem
- Every nonnegative measurable function is the increasing limit of simple measurable functions Theorem
- First-step equations for nonnegative exit costs Theorem
- Hitting probability as minimal harmonic extension Theorem
- Superharmonic majorants bound exit costs Theorem
Dependency tree · two levels
4 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, Definition 4.1 (standard reference, not scraped)
- Gerald B. Folland, Real Analysis, 2nd ed., §2.2 (standard reference, not scraped)