CorollaryStatement: AI-adaptedProof: AI-generatedPipeline-generatedprecheck pending

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.

Invariant conditional-entropy description of the SMB limit

Statement

Under AC, identifies the componentwise SMB limit with E[g_infinity|I], conditional expectation of infinite-past information given the invariant sigma-algebra.

Facts & Assumptions

Given: AC, a stationary finite-alphabet source, its invariant sigma-algebra $I = {E : T^{- 1} E = E}$ , and $g_{\infty}$ from Finite-past information densities.

[A1]

The Axiom of Choice: AC is assumed only for the published finite-measure Birkhoff-limit identification used below.

[F1]

Componentwise Shannon–McMillan–Breiman theorem: the block information limit is the Birkhoff limit of $g_{\infty}$ .

[F2]

Finite-measure identification of the Birkhoff limit: under AC, the Birkhoff limit integrates like the function over every strict invariant event.

[F3]

Conditional expectation given a sigma algebra: conditional expectation is characterized by measurability and equality of integrals on all events in the conditioning sigma-algebra.

[F4]

Strict and mod-null invariant sigma-algebras: the strict invariant sigma-algebra consists of events $E$ satisfying $T^{- 1} E = E$ .

Proof

Given: AC, the source, $g_{\infty}$ and the strict invariant sigma-algebra.

1.1A1F1F2F4given

The function $g_{\infty}$ is integrable by [F1]. Apply [F2] to its Birkhoff limit $G^{*}$ on the probability-preserving shift: $G^{*}$ has an $I$ -measurable representative and $\int_{E} G^{*} d P = \int_{E} g_{\infty} d P$ for every $E \in I$ .

2.1F1F2F3step 1.1algebra∎

These are exactly the defining tests in [F3] for $E [g_{\infty} ∣ I]$ . Hence $G^{*} = E [g_{\infty} ∣ I]$ almost surely, and the componentwise SMB limit has this description by [F1]. AC is used only through [F2]; the componentwise SMB theorem itself does not use this identification.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 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

Robert M. Gray, Entropy and Information Theory, corrected edition (standard reference, not scraped)