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.
Integrable real and complex functions, and their integrals
Definition
Let be measurable. Its positive and negative parts are they are measurable by Closure properties of measurable functions used by the integral and satisfy and .
The Lebesgue integral of a real measurable function is defined whenever at most one of and is , in which case The function is integrable when both integrals are finite, equivalently when .
For a complex measurable function with (Real and imaginary parts, complex conjugation, and modulus), define to be integrable when is integrable, and then define
Depends on
Used by
- A C¹ diffeomorphism satisfies the change-of-variables formula for L¹ functions Corollary
- A finite complex measure absolutely continuous with respect to a sigma-finite positive measure has an integrable complex density Corollary
- Polar integration may discard the cut locus Corollary
- A nonintegrable observable with divergent ergodic averages Counterexample
- A pointwise limit of integrable functions need not be integrable Counterexample
- A step has no locally integrable weak derivative Counterexample
- Infinite variance can defeat square-root-n CLT scaling Counterexample
- The fundamental Hessian is not absolutely locally integrable Counterexample
- The sine integral is improperly Riemann integrable and not Lebesgue integrable Counterexample
- A locally integrable function on ℝⁿ Definition
- A tight family of integrable functions Definition
- A uniformly integrable family Definition
- Characteristic function of a real random variable Definition
- Complex Haar Lᵖ spaces and compactly supported functions Definition
- Complex Lp classes and Euclidean test-function conventions Definition
- Counting, chordal proximity and characteristic Definition
- Direct integral of a measurable Hilbert field Definition
- Expectation of a nonnegative or integrable random variable Definition
- Indefinite Lebesgue integral on a compact interval Definition
- Rademacher functions on the unit interval Definition
- Riesz potential of order alpha Definition
- Spatial and frequency centres and variances of an L² function with finite second moments Definition
- The class L¹(μ) of integrable functions Definition
- The Fourier transform on an LCA group Definition
- The one-dimensional torus and its normalized Haar integral Definition
- The standard intertwining operator A(nu) Definition
- Weak convergence of borel probability measures Definition
- A circle representation with an averaged orthogonal weight form Example
- CLT for sums of uniform random variables Example
- Compact groups have a constant Reiter net Example
- Conjugate phases norm a three-atom function Example
- Integrating against a Dirac measure is evaluation at the point Example
- Matching C¹ pieces across a hyperplane have no jump derivative Example
- Negative drift gives a finite mean small-set hit Example
- Newton shell theorem from harmonic mean values Example
- Newtonian potential of radial compact data Example
- One-dimensional Dirichlet Green kernel on an interval Example
- Point evaluation is represented by a Dirac measure Example
- The positive-type Gaussian on the real line and its cyclic model Example
- The standard inner products make K n, ell two and quotient L two Hilbert spaces Example
…and 78 more results.
Dependency tree · two levels
12 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, Definition 6.2 (standard reference, not scraped)
- John K. Hunter, Measure Theory Notes, Definition 4.8 (standard reference, not scraped)