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.
Strongly measurable Banach-valued function
Definition
Let be a measure space and a real or complex Banach space. A function is strongly measurable (or Bochner measurable) if there are measurable -valued simple functions and a measurable null set such that
for every .
This is a norm-convergence condition. It is not, by definition, merely Borel measurability of or measurability of every scalar function . Changing on a null set preserves strong measurability: enlarge by that null set and retain the same approximants.
Remarks
- The zero function is strongly measurable, witnessed by the constant zero simple sequence.
- A single measurable simple function is strongly measurable, witnessed by the constant sequence and .
Depends on
Used by
- Bochner L2 space for a finite product-law input Definition
- Bochner-integrable function Definition
- Compact-group isotypic projection Definition
- L2-m-approximable causal Bernoulli shifts Definition
- The Duhamel heat potential Definition
- Isotypic Haar projections specialize to finite character sums Example
- A Borel map into a separable Banach space is strongly measurable Lemma
- A positive rank-one Haar average is a nonzero compact intertwiner Lemma
- Affine diffusion forms are well-defined on Bochner L2 Lemma
- Bochner L2 on a finite interval is a separable Hilbert space Lemma
- Characters of the L1 algebra of an abelian group Lemma
- Independent centered Hilbert-valued elements have zero expected inner product Lemma
- Integrated pressure recovery and MINI pressure-primitive convergence Lemma
- Laplace resolvents of a unitary group Lemma
- Long-run covariance of an L2-m-approximable shift is trace class Lemma
- Positive trace-class covariance defines a Hilbert Gaussian Lemma
- Recovering a unitary group representation from a nondegenerate L one representation Lemma
- Smooth mollifiers approximate Bochner L² functions Lemma
- The L1 action of a strongly continuous unitary representation Lemma
- The variation-of-constants integral is continuous for integrable forcing Lemma
- Time translations and mollification in Bochner Lp Lemma
- Weak compactness of bounded space-time Sobolev gradients Lemma
- Bochner dominated convergence theorem Theorem
- Bochner Lp is complete for a Banach value space Theorem
- Compact groups have property (T) by Haar averaging Theorem
- Finite-variance Hilbert mean bound for geometric medians of means Theorem
- First-order smooth pressure-primitive error for backward Euler MINI Theorem
- Isotypic projections are mutually orthogonal equivariant projections Theorem
- L1 in time estimate for Lp Duhamel forcing Theorem
- Pettis measurability criterion for strong measurability Theorem
- RNP and almost-everywhere differentiability of Lipschitz curves Theorem
- Stochastic Galerkin coercivity and Cea quasi-optimality Theorem
- Tensor products are dense in Bochner L2 under scalar and spatial density 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
- Gerald Teschl, Topics in Real and Functional Analysis (standard reference, not scraped)