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.
First-return times and induced transformations
Definition
Let preserve finite measure and let satisfy . For define the first-return time
A nonempty set of return times has a least element by The well-ordering principle. Define the infinitely returning core
This is the set-limsup convention of Limit superior and limit inferior of a sequence of sets. It is measurable by Sigma-algebras are closed under countable intersections, differences, symmetric differences, and set limits, and Poincare recurrence for finite measure-preserving systems gives . Define the induced transformation and normalized measure by
Here the trace is as in The trace of a sigma-algebra on a subset. Since is measurable, the trace equals : each intersection with is measurable and each such equals . Its closure under relative complement and countable union follows directly from these same operations in ; no sequence of ambient representatives needs to be chosen. This supplies the measurable-subset instance of The trace of a sigma-algebra is a sigma-algebra on the traced subset locally.
For , is finite, and the infinitely many visits after are exactly positive visits of , so . Restricting countable additivity of and dividing by the positive finite number makes a measure; its total mass is . The value is allowed for on , but is never used as an iterate in . No choice axiom enters this construction.
Depends on
- Poincare recurrence for finite measure-preserving systems
- The trace of a sigma-algebra on a subset
- The trace of a sigma-algebra is a sigma-algebra on the traced subset
- Limit superior and limit inferior of a sequence of sets
- Sigma-algebras are closed under countable intersections, differences, symmetric differences, and set limits
- The well-ordering principle
Used by
- Kac normalization needs ergodicity Counterexample
- First-return time and induced map are measurable Proposition
- Induced transformations preserve restricted finite measure Theorem
Dependency tree · two levels
18 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
- Sarig Definition 1.18 pp.28–29; domain correction (standard reference, not scraped)