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.
Complex Haar L^p spaces and compactly supported functions
Definition
Let be an LCH space with a fixed Radon measure , and write for the space of continuous complex-valued functions of compact support (Compact support, , and ). A complex-valued function on is measurable when its real and imaginary parts are measurable, and it is integrable when its modulus is integrable (Integrable real and complex functions, and their integrals). For the space consists of the almost-everywhere equivalence classes of measurable complex functions with the quotient and class notation being those of The space as the quotient by null functions. The modulus of a complex measurable function is measurable and depends only on the class of up to a null set, so is well defined on classes; on classes it is the norm of a complex normed space, and and are the complex Lebesgue spaces used on this page.
Let now be an LCH group with a fixed left Haar measure (Left Haar integral and left Haar measure). Then and suppressing the measure from the notation; the Haar measure is kept fixed throughout the page, so no ambiguity arises. The subscript is written and for the two norms.
Remarks
- Every function lies in both spaces. If then is bounded on the compact set and this set has finite -measure, so and ; the class of in is therefore defined for .
- Why the complex spaces are defined locally. The quotient construction of The space as the quotient by null functions is stated for real-valued functions and its norm theory is developed there for that case; the present definition fixes the complex version and its notation before convolution and the regular representations use it. No additional choice is needed here once is fixed.
- Finiteness of the Haar measure on compact sets. The integrability just claimed uses that a left Haar measure is finite on compact sets, which is part of the definition of a Radon measure recorded in Left Haar integral and left Haar measure.