TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13

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.

Kac integral formula for excursions

Statement

In an ergodic probability-preserving system, let $μ (E) > 0$ . For nonnegative measurable $f : X \to [0, \infty]$ , define $S_{E} f (x) = \sum_{j = 0}^{r_{E} (x) - 1} f (T^{j} x)$ on E, using the infinite nonnegative sum when $r_{E} (x) = \infty$ . Then $\int_{E} S_{E} f d μ = \int_{X} f d μ$ . For integrable real or complex f the excursion is absolutely summable a.e. on E; setting it to zero on its measurable null failure set gives the same identity.

Facts & Assumptions

[F1]

In an ergodic probability system, almost every point visits every fixed positive-measure set at some positive time. Positive sets sweep out ergodic probability systems.

[F2]

Pullback preserves nonnegative and integrable integrals. Integral invariance under measure-preserving maps.

[F3]

Return-time tails and finite iterates are measurable. First-return time and induced map are measurable.

[F4]

Nonnegative truncations and excursion partial sums pass through integrals. Monotone convergence for the integral.

[F5]

After absolute integrability is established, real/complex component integrals combine linearly. The Lebesgue integral is linear on $L^{1} (μ)$ .

[F6]

The measures of decreasing measurable sets of finite measure converge to the measure of their intersection. Continuity from above when one set has finite measure.

Proof

Given: In an ergodic probability-preserving system, let $μ (E) > 0$ . For nonnegative measurable $f : X \to [0, \infty]$ , define $S_{E} f (x) = \sum_{j = 0}^{r_{E} (x) - 1} f (T^{j} x)$ on E, using the infinite nonnegative sum when $r_{E} (x) = \infty$ . Then $\int_{E} S_{E} f d μ = \int_{X} f d μ$ . For integrable real or complex f the excursion is absolutely summable a.e. on E; setting it to zero on its measurable null failure set gives the same identity.

1.1

First let $0 \leq f \leq M < \infty$ . Put $A_{N} = ⋂_{j = 1}^{N} T^{- j} E^{c}$ . Splitting the integral at E and pulling the complement part back gives $\int f = \int_{E} f + \int f \circ T 1_{A_{1}}$ . More generally pulling back the part of $\int f \circ T^{N} 1_{A_{N}}$ outside E gives the next remainder, while its part on E is $\int_{E} f \circ T^{N} 1_{{r_{E} > N}}$ . Thus for N>=1 the exact finite identity is $\int f = \int_{E} \sum_{j = 0}^{N - 1} f \circ T^{j} 1_{{r_{E} > j}} + \int f \circ T^{N} 1_{A_{N}}$ . All products are defined piecewise as zero off their indicated sets.

F2F3

2.1

The sets $A_{N}$ decrease, and their intersection is the complement of $⋃_{j \geq 1} T^{- j} E$ . This intersection is null by [F1]. Since the ambient probability measure is finite, [F6] gives $μ (A_{N}) \to 0$ . The remainder is bounded between zero and $M μ (A_{N})$ and hence vanishes. The excursion partial sums on E increase pointwise to S_Ef; monotone convergence proves the identity for bounded nonnegative f.

step 1.1F1F4F6

3.1

For arbitrary nonnegative f use $f_{m} = \min (f, m)$ . These increase pointwise to f, and $S_{E} f_{m} ↑ S_{E} f$ : one inequality is termwise, and the other follows by first restricting to any finite number of excursion terms and then increasing m. Monotone convergence on X and E proves the equality, including infinite values.

step 2.1F4

4.1

For integrable real or complex f, apply step 3.1 to $∣ f ∣$ : $\int_{E} S_{E} ∣ f ∣ = \int ∣ f ∣ < \infty$ . Thus $S_{E} ∣ f ∣$ is finite a.e. (otherwise its integral is at least $K$ times the positive measure of its infinity set for every K). On this conull set the excursion is absolutely summable. Apply step 3.1 to the positive and negative parts of the real and imaginary components, each bounded by $∣ f ∣$ . Their excursion integrals are finite, so linearity yields the asserted identity without subtracting infinities. Null-set values have no effect.

step 3.1F5∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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 Theorem 1.7(3), pp.28–29 (standard reference, not scraped)