Dependencies

Let \(\pi :(\alpha ,T,\mu )\to (\beta ,S,\nu )\) be a factor map of measure-preserving systems on probability spaces (\(\alpha \) standard Borel), and let \(P, R\) be finite partitions of the total and factor systems, supplied with the generator reductions \(h(T)=h(T,P)\), \(h(S)=h(S,R)\), the relative-generator reduction \(h(T\mid \pi ^{-1}\mathcal B_\beta )=h(T,P\mid \pi ^{-1}\mathcal B_\beta )\), and the partition-level identity of Theorem 9.20 for \(P\) over \(\pi ^{-1}R\). Then the entropy of the total system splits as

the factor entropy plus the fibrewise entropy relative to the pulled-back factor \(\sigma \)-algebra \(\pi ^{-1}\mathcal B_\beta =\operatorname {comap}\pi \, m_\beta \).

Let \(T\) preserve \(\mu \) on a standard Borel probability space, let \(\mathcal A\le m_\alpha \) be forward invariant, and let \(P, Q\) be finite partitions such that (i) each cell of the \(n\)-fold \(P\)-join lies \(\mu \)-a.e. inside a single cell of the \(n\)-fold \(Q\)-join (a refinement witness \(g\)), and (ii) the join filtration of \(Q\) saturates \(\mathcal A\): \(\bigvee _n \sigma \bigl(\bigvee _{k{\lt}n}T^{-k}Q\bigr)=\mathcal A\). Then

The saturation hypothesis is essential: the identity is false without it.

If \(g\) is an ultrametric growth function and \(g(v)\neq g(w)\) (with \(v,w,v+w\) nonzero), then \(g(v+w)=\max (g(v),g(w))\).

For a permutation \(\sigma \in \mathfrak {S}_d\), the permutation dynamics \(\mathrm{adPerm}\, \sigma \) is conjugation \(x\mapsto P_\sigma \, x\, P_\sigma ^{\dagger }\) by the permutation matrix, a unital \(*\)-endomorphism; on diagonal matrices it acts by \((\mathrm{adPerm}\, \sigma )(\operatorname {diag}v)=\operatorname {diag}(v\circ \sigma )\). Paired with a \(\sigma \)-invariant diagonal state \(\rho _\mu \) (\(\mu \circ \sigma =\mu \), Definition 14.27) and a projection partition (Definition 14.28), this is the abelian corner: it mirrors the classical system \((\operatorname {Fin}d,\mu ,\sigma )\) with the measurable partition \(c^{-1}(\cdot )\).

For a finite measure, a measure-preserving \(T\) and integrable \(g\), the Birkhoff averages \(n \mapsto \texttt{birkhoffAverage}\, \mathbb {R}\, T\, g\, (n+1)\, x\) are a.e. bounded above (and, applied to \(-g\), a.e. bounded below).

For all \(a, b \in \mathbb {R}\) with \(a + b {\lt} 0\),

For a.e. \(x\), for every forward level \(i\) and backward level \(s\) with \(\mathrm{expEnum}\, \mathrm{lam0}\, d\, i + \mathrm{expEnum}\, \mathrm{mu0}\, d\, s {\lt} 0\),

For a finite measure, measure-preserving \(T\) and an a.e. measurable \(F\) with \(F\, x \le F\, (Tx)\) for a.e. \(x\), one has \(F \circ T =^{\text{a.e.}} F\).

Under the same hypotheses, for a.e. \(x\) the EReal limsup of the normalized cocycle is dominated by its liminf.

For a.e. \(x\) and all \(t \in \mathbb {R}\),

Let \( V \) be the Oseledets filtration of the time-one data, and fix \( t_0 \in \mathbb {R}\). Then for almost every \( x \) and every level \( i \),

For \(\mu \)-a.e. \(x\) and every threshold index \(k\in [1,d)\), the block term \((e^{\lambda ^0_{k-1}}-e^{\lambda ^0_k})\cdot P^{c_k}_n(x)\) converges, where \(P^{c}_n\) is the band projector \(\mathbf1_{(c,\infty )}(q_n(x))\).

For \(\mu \)-a.e. \(x\) and every \(t\), \(\mathrm{lambdaSublevel}(x,t) \le \mathrm{vslow}(x,e^t)\).

For a measure-preserving \(T\) and a finite partition indexed by a nonempty \(\iota \),

Neither ergodicity nor any ergodic theorem enters: this is the Algoet–Cover engine fed the uniform competing measure, whose partition-function bound \(\int \exp \bigl(i_n - n\log \# \iota \bigr)\, d\mu \le 1\) is the lemma .

For a.e. \(x\),

Under the same hypotheses, \(\bar d_\mu (x) = \operatorname {finrank}_{\mathbb {R}} E\) for \(\mu \)-almost every \(x\): the measure is exact-dimensional with dimension equal to the ambient dimension.

If \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) holds, then \(\mu \)-a.e. each interior flag level is exactly a growth-sublevel set: for every \(i\) and vector \(v\),

For \(\mu \)-a.e. \(x\), every \(c{\gt}0\) that is not one of the limiting eigenvalues \(e^{\lambda _{\mathrm{sing}}(x,i)}\) of \(\Lambda (x)\) satisfies

For a finite measure, measure-preserving measurable \(T\), an integrable subadditive cocycle with normalized integrals bounded below, there is an integrable \(G\) with \(\texttt{cdiv}\, g\, n\, x \to G\, x\) for \(\mu \)-a.e. \(x\).

Let \(T\) be ergodic and let \((i_n)\) be any sequence of functions satisfying, for \(\mu \)-a.e. \(x\) and all \(n\), the Breiman telescoping identity

where \(g_k\) is the conditional information function of \(P\) given \(\mathcal C_k\). Then

Let \(T\) be an ergodic measure-preserving transformation of a standard Borel probability space and \(P\) a finite measurable partition (nonempty index). Then the concrete information functions of Definition 10.1 satisfy

the measure of the atom of \(x\) in the \(n\)-fold join decays like \(e^{-n\, h(P,T)}\) (entropy equipartition, the AEP of ergodic theory).

For integrable \( g, g' \) and a measure-preserving flow \( \varphi \), for almost every \( x \) the combined fluctuation along the integer orbit vanishes:

Let \(E\) be a finite-dimensional real inner-product space (Borel-measurable) and let \(\mu \) be a probability measure on \(E\) absolutely continuous with respect to an additive Haar measure \(\nu \) (e.g. Lebesgue). Then for \(\mu \)-almost every \(x\) the local-dimension quotient \(\log \mu (\bar B(x,r)) / \log r\) converges, as \(r \to 0^+\), to the ambient dimension \(\dim _{\mathbb {R}} E = \operatorname {finrank}_{\mathbb {R}} E\).

Fix a real time \( t_0 \). For almost every \( x \), both \( n^{-1}\log \left\lVert A(t_0, \varphi (n)x) \right\rVert \) and \( n^{-1}\log \left\lVert (A(t_0, \varphi (n)x))^{-1} \right\rVert \) tend to \( 0 \) as \( n \to \infty \).

For a measure-preserving \(T\) and integrable \(g\), the orbital tail \(n^{-1}\, g(T^{[n]}x)\) tends to \(0\) for \(\mu \)-a.e. \(x\).

If \(\det A(x) \neq 0\) for all \(x\), \(A\) is measurable, \(T\) is measure-preserving, and \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1(\mu )\), then the backward system \((T^{-1}, B)\) satisfies the same four hypotheses: \(\det B \neq 0\) everywhere, \(B\) measurable, and \(\log ^+\left\lVert B \right\rVert , \log ^+\left\lVert B^{-1} \right\rVert \in L^1(\mu )\).

For \(A : X \to \mathrm{Matrix}\, (\mathrm{Fin}\, d)\, (\mathrm{Fin}\, d)\, \mathbb {R}\) and \(T : X \simeq _m X\), the backward generator is

Its cocycle is taken over \(T^{-1}\).

The Bernoulli suspension flow is the time-translation flow on the suspension (mapping-torus) of the two-sided Bernoulli shift \(T\) over \(\operatorname {bernZ}\nu \) with constant roof \(\tau \equiv 1\): points are orbits \([x, s]\) of the identification \((x, s) \sim (Tx, s - 1)\), the flow is \(\zeta _t[x,s] = [x, s+t]\), and it preserves the normalized suspension measure \(\hat\mu \) (the product of \(\operatorname {bernZ}\nu \) with Lebesgue on the fibres; the constant roof makes the normalizing constant \(1\)). It is a MeasurePreservingFlow of \(\hat\mu \) (Definition 8.1).

The witness partition of the suspension measure \(\hat\mu \) is the base time-\(0\) coordinate partition of \(\operatorname {bernZ}\nu \) pulled back along the base projection (factor map) \(\pi : [x,s] \mapsto T^{\lfloor s \rfloor } x\), which is measure-preserving onto \(\operatorname {bernZ}\nu \). Its cells are indexed by \(\operatorname {Fin}(\operatorname {card} \alpha _0)\); the crux mass identity is that pulling back does not change cell masses, so the \(j\)-th cell carries the single-symbol mass \(\nu \{ a_j\} \) of the corresponding symbol.

The bottom exponent \(\lambda _d = \Gamma _d - \Gamma _{d-1}\) is lower semicontinuous in the generator: \(\lambda _d(A) \le \liminf _i \lambda _d(B_i)\).

Let \(\operatorname {catLift}:\mathbb {R}^2\to \mathbb {R}^2\) () be the linear lift of the cat map to the universal cover — the continuous linear map with matrix \(M\), which genuinely lifts \(\operatorname {catTorus}\): the covering projection \(\mathbb {R}^2\to \mathbb {T}^2\) satisfies \(\pi \circ \operatorname {catLift} = \operatorname {catTorus}\circ \pi \) (). Its derivative cocycle in the sense of Definition 12.1 is the constant matrix \(M\) at every point (), and the top Lyapunov exponent of this genuine derivative cocycle, over the genuine ergodic base \(\operatorname {catTorus}\), is

the formalized hyperbolicity of the Arnold cat map. (Reading the derivative on the torus manifold itself via \(\texttt{mfderiv}\) is a documented gap: Mathlib has no manifold-derivative API for \(\texttt{AddCircle}\) endomorphisms; the lift and the map share the same derivative everywhere because the covering projection is a local diffeomorphism with identity derivative.)

Realized as a constant cocycle with generator the cat-map matrix \(M\) over an ergodic base (here the doubling map — the spectrum depends only on \(M\)), the two Lyapunov exponents are

Honesty caveat (as in the Lean docstring): the cocycle here is the constant matrix, not the derivative cocycle of the genuine toral automorphism; the genuine dynamics is treated below.

\(\lambda _1 + \lambda _2 = 0\): the cocycle is conservative (\(\det M = 1\)).

The map \(\operatorname {catTorus}:\mathbb {T}^2\to \mathbb {T}^2\), \((\operatorname {catTorus} y)_i = \sum _j M_{ij}\cdot y_j\), with the integer cat-map matrix \(M\) acting by integer scalar multiplication on each circle coordinate. Since \(\det M = 1\), the integer matrix \(M^{-1}\) (with rows \((1,-1)\) and \((-1,2)\)) induces a two-sided inverse, so \(\operatorname {catTorus}\) is a continuous additive automorphism of the compact group \(\mathbb {T}^2\). Throughout this section \(\mathbb {T}^2\) carries the product Haar probability measure (the normalization for which Mathlib’s multivariate Fourier basis is stated).

Realized as a constant cocycle with generator \(M\) over the genuine ergodic Arnold cat map \(\operatorname {catTorus}\), the two Lyapunov exponents are \(\log \bigl((3+\sqrt5)/2\bigr)\) and \(\log \bigl((3-\sqrt5)/2\bigr)\) — the same spectrum as Theorem 12.19, now over the hyperbolic toral automorphism itself rather than a surrogate base.

For any finite measurable partition \(P\) of \(\mathbb {T}^2\) whose \(n\)-fold refinement under \(\operatorname {catTorus}\) eventually has at most \(C\cdot e^{\, n\log \lambda _+}\) non-empty atoms (\(C\ge 1\), \(\lambda _+ = (3+\sqrt5)/2\)),

As in the doubling-map case this is the per-partition bound, not the system inequality; the rate \(\log \lambda _+\) is the genuine top Lyapunov exponent of the cat map (Theorem 12.25), and the atom-count growth is the honest named geometric input. The sharp system-level equality \(h_\mu = \log \lambda _+\) is a documented wall (it needs an Adler–Weiss Markov generating partition for the upper bound and Pesin/Ledrappier–Young machinery for the lower bound).

The normalized cocycle is \(\texttt{cdiv}\, g\, n\, x = g\, (n+1)\, x / (n+1)\), the sequence whose a.e. limit is the content of Kingman’s theorem; its EReal coercion is \(\texttt{ecdiv}\, g\, n\, x\), used where \(-\infty \) cannot be excluded a priori.

If \(M\) is self-adjoint and \(M v = c\, v\) for \(v \neq 0\), then \((\mathrm{cfc}\, f\, M)\, v = f(c)\cdot v\).

For positive-definite \(A,B\), \(\ \log (A\otimes B) = \log A\otimes 1 + 1\otimes \log B\).

For a differentiable \(T\), the \(n\)-th cocycle iterate of the derivative generator represents the derivative of the \(n\)-th iterate of the map:

For any Kraus channel with all four states faithful, saturation \(S(\rho \| \sigma )=S(\Lambda \rho \| \Lambda \sigma )\) implies IntertwinesIt.

For a Kraus channel \(\Lambda \) with all four states \(\rho ,\sigma ,\Lambda \rho ,\Lambda \sigma \) faithful, if data processing is saturated (\(S(\rho \| \sigma )=S(\Lambda \rho \| \Lambda \sigma )\)), then the two \(-\log \) modular quadratic forms agree at the output cyclic vector \(\xi =\operatorname {vec}((\Lambda \rho )^{1/2})\):

with \(W=\texttt{petzWChanVec}\), \(\Delta =\sigma \otimes (\rho ^{-1})^{\top }\), \(\Delta _{\mathrm{out}}=(\Lambda \sigma )\otimes ((\Lambda \rho )^{-1})^{\top }\).

Under entropy saturation, the channel contraction intertwines the modular unitary power on the output cyclic vector, \(W\bigl(\Delta _{\mathrm{out}}^{it}\, \xi \bigr)=\Delta ^{it}\, (W\xi )\), with \(W\xi =\operatorname {vec}(\rho ^{1/2})\).

For a countable family of cells \(s : \iota \to \mathrm{Set}\, \alpha \), the countable Shannon entropy is \(\; c H_\mu (s) = \sum _i \operatorname {negMulLog}\, \mu (s_i) = -\sum _i \mu (s_i)\log \mu (s_i)\), an unconditionally convergent tsum. Downarowicz’s Fact 1.1.4 supplies the finiteness criterion (): if the index-weighted masses satisfy \(\sum _i i\cdot \mu (s_i) {\lt} \infty \), the entropy terms are summable, so \(cH_\mu (s)\) is a genuine finite sum. This is the form in which the Keane–Serafin construction certifies finite entropy of its limit partition.

For Kraus operators \(K\) with \(\sum _i K_i^{\dagger }K_i=1\) and \(X\) self-adjoint with spectrum in \((0,\infty )\),

Let \(g_k\) be the conditional information function of \(P\) given the \(k\)-th Breiman conditioning \(\sigma \)-algebra \(\mathcal C_k = \sigma (T^{-1}\bigvee _{j=0}^{k-1}T^{-j}P)\), and let \(g^{*} = \sup _k g_k\) be the Chung maximal information function (, valued in \([0,\infty ]\)). Then for every cell \(P_{i_0}\) and every \(\lambda {\gt} 0\),

Consequently \(g^{*} \in L^1(\mu )\), with \(\int g^{*}\, d\mu \le H(P) + 1\) () — Chung’s \(L^1\) domination, the one genuinely analytic leaf of the SMB proof.

The entropy of a partition is the infimum von Neumann entropy rate

and the CNT dynamical entropy of \(\Phi \) in the state \(\rho \) is the supremum over all finite operational partitions, \(h_\Phi (\rho )=\sup _{k,X}h_\Phi (\rho ,X)\) (valued in \(\overline{\mathbb {R}}\)). The \(\inf _n\) form is the honest analogue of the subadditive limit \(\lim _n S(\cdot )/n\) and sidesteps an operator-Fekete argument.

The abelian-corner CNT dynamical entropy of \(\mathrm{adPerm}\, \sigma \) in the state \(\rho _\mu \) is the supremum of the partition rate over all projection operational partitions, \(h^{\mathrm{ab}}_{\mathrm{adPerm}\, \sigma }(\rho _\mu ) =\sup _{k,c}h_{\mathrm{adPerm}\, \sigma }(\rho _\mu ,\mathrm{projPartition}\, c)\).

Suppose every state carries positive mass (\(\mu _i{\gt}0\) for all \(i\)). Then the abelian-corner CNT dynamical entropy equals the classical Kolmogorov–Sinai entropy of the permutation system:

For each projection partition \(\mathrm{projPartition}\, c\), the CNT partition entropy in the abelian corner equals the classical Kolmogorov–Sinai partition entropy of the corresponding measurable partition \(c^{-1}(\cdot )\):

Given \(A : X \to \operatorname {Matrix}(\operatorname {Fin}d)(\operatorname {Fin}d)\, \mathbb {R}\) and \(T : X \to X\), define \(A^{(n)} = \texttt{cocycle}\, A\, T\, n\) by recursion on \(n\):

Unfolding, \(A^{(n)}(x) = A(T^{n-1}x)\cdots A(Tx)\, A(x)\), with the newest factor on the left. The matrix norm throughout is the scoped L2 operator norm, which is submultiplicative; vectors live in \(\mathrm{EuclideanSpace}\; \mathbb {R}\, (\operatorname {Fin}d)\) and the action is via \(\texttt{toEuclideanCLM}\).

For all \(m, n \in \mathbb {N}\) and \(x \in X\),

For \(c\ge 0\) and \(n\ge 1\),

Writing \(B = \mathrm{backwardGen}\, A\, T\), the cocycle of \(B\) over \(T^{-1}\) satisfies

If \(T\) is differentiable and uniformly expanding with constant \(K {\gt} 1\), then the derivative of the \(n\)-th iterate stretches every vector by at least \(K^n\):

For any generator \(A\) and map \(T\), \(A^{(n+1)}(x) = A(T^{[n]}x)\cdot A^{(n)}(x)\).

Let \(\mu \) be an invariant probability measure with \(\mu \ll \operatorname {volume}\), let \(T\) be differentiable with everywhere nonvanishing Jacobian, let \(\xi \) be an injectivity partition, and assume \(\log \rho \in L^1(\mu )\) for the density \(\rho = d\mu /d\operatorname {vol}\) and \(\log \left\lvert \det D T \right\rvert \in L^1(\mu )\). Then the conditional Shannon entropy of \(\xi \) given the pulled-back \(\sigma \)-algebra \(T^{-1}\mathcal{A}\) is

independently of the partition (no generating hypothesis).

For any finite measurable partition \(P\) of a standard Borel probability space and any sub-\(\sigma \)-algebra \(\mathcal A\le m_\alpha \),

On a standard Borel probability space, the conditional Shannon entropy of a finite family of cells \(s\) given a sub-\(\sigma \)-algebra \(\mathcal A\) is

the \(\mu \)-average of the pointwise entropy computed against the regular conditional probability kernel \(\kappa =\operatorname {condExpKernel}\mu \, \mathcal A\). It measures the information about the partition remaining after conditioning on \(\mathcal A\); conditioning on the trivial \(\sigma \)-algebra recovers the ordinary entropy.

For a finite measure, a measure-preserving measurable \(T\) and integrable \(g\), the conditional expectation onto the \(\sigma \)-algebra \(\texttt{invariants}\, T\) of \(T\)-invariant sets is a.e. \(T\)-invariant:

For a sub-\(\sigma \)-algebra \(\mathcal A\) of a standard Borel space, the conditional information function of \(P\) given \(\mathcal A\) is

the conditional probability realized by the regular conditional probability kernel; exactly one indicator survives at each point. Its integral is the conditional entropy: for \(\mathcal A \le m_\alpha \), \(\int g_{\mathcal A}\, d\mu = H(P \mid \mathcal A)\) (); in particular \(g_{\mathcal A}\) is integrable.

The relative entropy of the system given \(\mathcal A\) is the \(\overline\mathbb {R}\)-valued supremum \(h(T\mid \mathcal A) = \sup _\alpha h(T,\alpha \mid \mathcal A)\) over all finite measurable partitions, mirroring Definition 9.13.

For a sub-\(\sigma \)-algebra \(\mathcal A\le m_\alpha \) with \(T^{-1}\mathcal A\le \mathcal A\) (forward invariance), the relative entropy of \(T\) on a partition \(\alpha \) given \(\mathcal A\) is the Fekete limit of the conditional iterated-join entropies,

the conditional sequence being subadditive by the conditional analogues of Theorem 9.4 and Lemma 9.5.

Under the hypotheses of Theorem 14.12, for every continuous \(g\),

For a contraction \(W\) with defect \((1-W^{\dagger }W)\xi =0\), positive-definite shifts \(X,\mathrm{Out}\), writing \(\eta =\mathrm{Out}^{-1}\xi \), \(b=X^{-1}(W\xi )-W\eta \), \(Y=W^{\dagger }XW\),

In the setting of Lemma 14.10, with the compression bound \(W^{\dagger }XW\le \mathrm{Out}\), if the total resolvent gap \(\operatorname {Re}\langle \xi ,(W^{\dagger }X^{-1}W-\mathrm{Out}^{-1})\xi \rangle \) vanishes, then \(X^{-1}(W\xi )=W(\mathrm{Out}^{-1}\xi )\).

Let \(W\) be a contraction (\(W^{\dagger }W\le 1\)), \(\Delta ,\Delta _{\mathrm{out}}\) positive definite with compression bound \(W^{\dagger }\Delta W\le \Delta _{\mathrm{out}}\), cyclic-norm condition \(\left\lVert W\xi \right\rVert =\left\lVert \xi \right\rVert \), and the scalar \(-\log \) saturation \(\operatorname {Re}\langle \xi ,W^{\dagger }(-\log \Delta )W\xi \rangle =\operatorname {Re}\langle \xi ,(-\log \Delta _{\mathrm{out}})\xi \rangle \). Then for every \(t{\gt}0\),

For a dynamics \(\Phi \), a state \(\rho \) (a density matrix on \(\mathbb {C}^d\)) and an operational partition \(X\), the depth-\(n\) correlation density matrix \(\mathrm{corrMatrix}\, \Phi \, \rho \, X\, n\) is the matrix on the classical index set \((\operatorname {Fin}k)^{\operatorname {Fin}n}\) with entries

It is a genuine density matrix: its trace is \(1\) by the telescoping identity (Lemma 14.24) together with \(\operatorname{tr}\rho =1\), and it is positive semidefinite because the quadratic form \(x^{\dagger }Mx\) equals \(\operatorname{tr}(T\rho T^{\dagger })\ge 0\) for \(T=\sum _f x_f\, \mathrm{refine}(n,f)\).

For a finite index type \(n\), a density matrix is a structure bundling a matrix \(\rho \in \operatorname {Matrix}_n(\mathbb {C})\) together with proofs that \(\rho \) is positive semidefinite and has unit trace, \(\operatorname{Tr}\rho = 1\). It is the finite-dimensional state of a quantum system on \(\mathbb {C}^n\).

The real eigenvalues \(\lambda _i\) of a density matrix \(\rho \) are nonnegative, each at most \(1\), and sum to \(1\): \(\sum _i \lambda _i = \operatorname{Tr}\rho = 1\).

For a probability vector \(\mu :\operatorname {Fin}d\to \mathbb {R}_{\ge 0}\) (\(\sum _i\mu _i=1\)), the associated diagonal state is \(\rho _\mu =\operatorname {diag}\mu \), a density matrix on \(\mathbb {C}^d\).

For a self-map \(T\) of \(E = \operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\), the derivative cocycle generator is the matrix-valued map

the matrix representing the Fréchet derivative \(D_xT = \operatorname {fderiv}\, \mathbb {R}\, T\, x\), transported along the star-algebra equivalence between \(d\times d\) real matrices and continuous linear endomorphisms of \(E\). Since that equivalence is an \(L^2\)-operator-norm isometry, the generator has the same norm as \(D_xT\). Feeding it to the iterated cocycle construction of Definition 2.2 yields the tangent cocycle of the smooth system.

If \(\det A(x) \neq 0\) for every \(x\), then \(\det A^{(n)}(x) \neq 0\) for all \(n, x\).

Let \(\operatorname {bern}\nu \) be the Bernoulli (i.i.d. product) measure on the full shift with single-symbol law \(\nu \), and suppose \(\nu \) charges two distinct symbols \(i \ne j\) with positive mass. Then there is a \(\operatorname {bern}\nu \)-conull set \(s\) with

the single-symbol Shannon entropy (Hnu in the sources). No ergodicity or positive-entropy hypothesis remains: both standing conditionals of Theorem 11.18 are discharged for the Bernoulli case.

Let \(\mu \) be a probability measure on a finite-dimensional real inner-product space \(E\), absolutely continuous with respect to a Haar measure. Then every set \(s\) of full \(\mu \)-measure has Hausdorff dimension equal to the ambient dimension: \(\dim _H s = \operatorname {finrank}_{\mathbb {R}} E\).

Let \(\mu \) be a shift-invariant probability measure on the full shift \(\Sigma \) such that the left shift \(\sigma \) is ergodic for \(\mu \), and suppose the Kolmogorov–Sinai entropy of the coordinate partition is positive. Then there is a full-measure carrier set \(s \subseteq \Sigma \) (\(\mu (s^{\mathsf c}) = 0\)) with

where \(h_\mu (\sigma )\) is the partition-independent system entropy (ksEntropy, Definition 9.13).

Let \(\mu \) be a probability measure on a Borel second-countable metric space \(E\), let \(\alpha {\gt} 0\), and let \(s\) be a set of full \(\mu \)-measure (\(\mu (s^{\mathsf c}) = 0\)) such that for every \(x \in s\) the local-dimension quotient \(\log \mu (\bar B(x,r))/\log r\) tends to \(\alpha \) as \(r \to 0^+\). Then \(\dim _H s = \alpha \).

For any finite measurable partition \(P\) of the circle whose \(n\)-fold refinement \(\bigvee _{k=0}^{n-1}T^{-k}P\) under the doubling map eventually has at most \(C\cdot e^{n\log 2}\) non-empty atoms (\(C\ge 1\)),

This is the per-partition bound \(h(\alpha ,T)\le \sum \lambda ^{+}\), not the system Margulis–Ruelle inequality; the right-hand side is the computed Lyapunov datum (Corollary 12.14), not an abstract constant. The atom-count hypothesis is automatic for the binary partition, where the bound is attained (Theorem 12.17).

The sum of the strictly positive Lyapunov exponents of the doubling-map cocycle is \(\log 2\), with every spectrum hypothesis (invertibility, measurability, both log-integrability conditions) discharged unconditionally from the constant-cocycle API.

The constant cocycle with generator \(M = (2)\) over the ergodic doubling map has top Lyapunov exponent \(\log 2\).

The Shannon entropy of a finite family of cells \(s:\iota \to \mathcal P(\alpha )\) with respect to a measure \(\mu \) is

the average information gained by learning which cell a \(\mu \)-random point lies in. The definition is on loose data — an arbitrary Fintype-indexed family of sets — so it applies both to genuine partitions and to intermediate non-partition families.

For two finite measurable partitions \(\alpha =(A_i)\) and \(\beta =(B_j)\) of a probability space, the entropy of the join (common refinement) \(\alpha \vee \beta \), whose cell family at \((i,j)\) is the intersection \(A_i\cap B_j\), satisfies

A finite measurable partition of a probability space into \(k\) cells (with \(k\ge 1\)) has Shannon entropy at most \(\log k\).

For a measure-preserving \(T\) and a finite measurable partition \(\beta \), the pullback partition \(T^{-1}\beta \) with cells \(T^{-1}B_j\) has the same Shannon entropy as \(\beta \): \(H(T^{-1}\beta )=H(\beta )\).

Let \(S\) be orthogonal (\(S S^{\top }=1\)) with the graded forward decay \(\left\lvert S_{ab} \right\rvert \le c\cdot e^{-\max (g_b-g_a,0)}\). Then every entry obeys the reverse bound at the full pairwise rate:

Assume the base shift \(T\) is ergodic for \(\operatorname {bernZ}\nu \). Then every measurable set \(A\) invariant under all time-\(t\) maps of the suspension flow (\(\zeta _t^{-1}(A) = A\) for every \(t \in \mathbb {R}\)) is null or conull: \(\hat\mu (A) = 0\) or \(\hat\mu (A) = 1\). The base hypothesis is discharged unconditionally by the two-sided Bernoulli ergodicity theorem (ergodic_biShiftEquiv_bernZ); the companion ergodic_bernSuspensionFlow_uncond records the unconditional statement. By contrast, the time-\(1\) map alone is never ergodic (not_ergodic_bernSuspensionFlow_one): the saturated section set \(\{ [x,s] : \operatorname {fract} s {\lt} 1/2\} \) is invariant of mass \(1/2\) — the constant-roof special-flow dichotomy of Cornfeld–Fomin–Sinai.

\(\operatorname {catTorus}\) is ergodic for the Haar probability measure on \(\mathbb {T}^2\).

Define \(E_i = V_i \sqcap W_{\mathrm{sidx}\, i}\). Then \(\mathrm{finrank}\, E_i \ge 1\), the telescoping identities \(V_i = E_i \sqcup V_{i+1}\) and \(E_i \sqcap V_{i+1} = \bot \) hold, and consequently \((E_i)\) is independent with \(\bigsqcup _i E_i = V_0 = \top \).

For \(T\) measure-preserving on a probability space and a conull measurable set \(S\), there is a conull measurable \(S' \subseteq S\) invariant under both \(T\) and \(T^{-1}\).

Let \((\alpha ,\mu )\) be standard Borel with automorphism \(e\), and let \(Q : \mathbb {N}\to \mathrm{Set}\, \alpha \) be a countable family of measurable cells such that (i) the two-sided \(Q\)-itinerary recovers each set of a fixed standard-Borel generating sequence up to a \(\mu \)-null set, and (ii) the entropy terms \(i \mapsto \operatorname {negMulLog}\, \mu (Q_i)\) are summable. Then there is a countable family that two-sidedly generates \((\alpha ,e,\mu )\) mod \(0\) and has finite static Shannon entropy — sub-problem A of Krieger’s theorem (Downarowicz, Thm. 4.2.3, first half). The structural reduction from the inductive Keane–Serafin data — an increasing sequence of finite partitions with per-level recovery and a summable geometric mass envelope — is ; the construction of that data from the raw dynamical hypotheses (the SMB-driven Rokhlin-tower marker painting of Keane–Serafin §2) is the disclosed residual, isolated as an explicit hypothesis bundle rather than formalized.

Let \(T\) be measure preserving and assume the in-measure SMB upper bound of Theorem 10.10. Write \(h = h(P,T)\). For every \(\varepsilon {\gt} 0\) and all sufficiently large \(N\), there is a finite set \(S\) of rank-\(N\) names \(g : \operatorname {Fin}N \to \iota \) with

The set \(S\) is the set of good names () — names whose join cell has measure at least \(e^{-N(h+\varepsilon )}\); the cardinality bound is the unconditional pigeonhole .

For merely measure-preserving \(T\) (no ergodicity) and invertible measurable \(A\) with the standing integrability, there is a family of \(T\)-invariant integrable functions \(\lambda _i : X \to \mathbb {R}\) such that for each \(i {\lt} d\) and \(\mu \)-a.e. \(x\), \(\tfrac 1n\log \sigma _i(A^{(n)}(x)) \to \lambda _i(x)\). The exponents become invariant functions rather than constants.

For a measure-preserving \(T\), an integrable subadditive cocycle \(g\) whose normalized integrals are bounded below, the sequence \((\int g\, (n+1)\, d\mu )/(n+1)\) converges to the Fekete constant \(\gamma \).

For ergodic \(T\) and invertible \(A\), every Oseledets filtration has a deterministic dimension profile: there is a strictly decreasing \(m : \mathrm{Fin}(k+1) \to \mathbb {N}\) with \(m_0 = d\), \(m_k = 0\) and, \(\mu \)-a.e., \(\mathrm{finrank}\, V_i(x) = m_i\).

Let \( \mu \) be a probability measure, \( \varphi \) a measure-preserving flow with \( \varphi (1) \) ergodic, and \( A \) a flow cocycle with the two uniform integrable dominators \( g, g' \). Then there exist \( k \), exponents \( \lambda : \mathrm{Fin}\, k \to \mathbb {R}\), and a subspace family \( V \) forming an Oseledets filtration for the generator \( A(1,\cdot ) \) over the dynamics \( \varphi (1) \).

There is an antitone sequence \(\lambda ^0 : \mathbb {N}\to \mathbb {R}\) (antitone on \([0,d)\)) such that, for every \(i{\lt}d\) and \(\mu \)-a.e. \(x\),

where \(\sigma _i\) is the \(i\)-th sorted singular value.

For ergodic \(T\) and invertible \(A\), each exponent \(\lambda _i\) carries a positive deterministic multiplicity \(m_i = \dim V_i - \dim V_{i+1}\) with \(\sum _i m_i = d\).

Over an alphabet \(\operatorname {Fin}l\) with a reserved sentinel letter \(s\), any finite name set with \(\# \mathrm{Name} \le (l-1)^m\) admits an injection \(\mathrm{enc} : \mathrm{Name} \hookrightarrow \mathrm{List}(\operatorname {Fin}l)\) into blocks of length \(m+1\), each containing the sentinel exactly once (at its end). The blocks form a prefix-free family, so arbitrary concatenations are uniquely decodable (); when \(e^{N(h+\varepsilon )} {\lt} k^{N}\), the good names of Theorem 10.12 embed into \(\operatorname {Fin}k\)-blocks of length \(O(N)\) — the symbolic code from which the coding partition is read off along a Rokhlin tower.

Summing the positive parts \(\max (\lambda _i(x),0)\) over \(i {\lt} d\) yields a single \(T\)-invariant integrable function \(G_+ : X \to \mathbb {R}\), the non-ergodic analogue of the positive-exponent sum.

\(\mu \)-a.e., \(\exp (\mathrm{exponents}_i)\) is the \(i\)-th sorted eigenvalue of the Oseledets limit matrix \(\Lambda (x)\).

Under the same hypotheses, every singular value of the cocycle iterate \(A^{(n)}(x) = \operatorname {cocycle}(\operatorname {derivativeCocycle} T)\, T\, n\, x\) is at least \(K^n\): \(\ K^n\le \sigma _i\bigl(A^{(n)}(x)\bigr)\) for every \(i {\lt} d\).

The full Lyapunov spectrum with multiplicity is the total function \(\mathrm{exponents} : \mathrm{Fin}\, d \to \mathbb {R}\), whose \(i\)-th entry is the deterministic limit of \(\tfrac 1n\log \sigma _i(A^{(n)})\), sorted non-increasingly. The top entry is \(\mathrm{topExponent}\).

Every Lyapunov exponent of a uniformly expanding map is strictly positive: \(0 {\lt} \log K \le \lambda _i\).

For each sorted index \(i\) and \(\mu \)-a.e. \(x\), \(\tfrac 1n\log \sigma _i(A^{(n)}(x)) \to \mathrm{exponents}_i\); moreover \(\mathrm{exponents}\) is antitone.

The \(k\)-th exterior generator \(\mathrm{extGen}\, k\, A\) sends \(x\) to the \(k\)-th compound matrix \(C_k(A x)\) of \(k\times k\) minors. Its iterated cocycle is the compound of the iterate: \(\mathrm{cocycle}(\mathrm{extGen}\, k\, A)\, T\, n\, x = C_k(A^{(n)}(x))\).

If \(E\) is finite-dimensional and \(g\) is an ultrametric growth function, then \(\{ g(v) : v\neq 0\} \) is finite, with at most \(\dim _{\mathbb {R}} E\) elements.

A descending flag \(V_0 \supseteq \cdots \supseteq V_k = \bot \) in a modular lattice, with complements \(E_i\) satisfying \(V_i = E_i \sqcup V_{i+1}\) and \(E_i \sqcap V_{i+1} = \bot \), telescopes into an independent family \((E_i)\) with \(\bigsqcup _i E_i = V_0\).

A continuous-time linear cocycle over a measure-preserving flow \( \varphi \), valued in invertible \( d \times d \) real matrices, is a family \( A : \mathbb {R}\to X \to \mathrm{Mat}_d(\mathbb {R}) \) with \( A(0,x) = 1 \), the cocycle identity (newest factor on the left) \( A(t+s,x) = A(t, \varphi (s)x)\, A(s,x) \), a proof that \( \det A(t,x) \ne 0 \) for all \( t, x \), and measurability of each time-\( t \) map \( A(t,\cdot ) \).

Let \(T\) be ergodic for a probability measure \(\mu \), let \(A\) be measurable and everywhere invertible with \(\log ^{+}\left\lVert A \right\rVert , \log ^{+}\left\lVert A^{-1} \right\rVert \in L^{1}(\mu )\). Then there is a constant \(\lambda _1 \in \mathbb {R}\) (the top Lyapunov exponent) with

Under the same hypotheses there is a constant \(\lambda \in \mathbb {R}\) with

so the bottom Lyapunov exponent \(\lambda _k = -\lambda \) exists and is finite.

The partial-sum growth rate is the infimum over \(n\) of the normalized integrals:

For \(k \le d\), the ergodic growth rate \(\Gamma _k\) of the product of the top-\(k\) singular values equals the sum of the top-\(k\) exponents: \(\Gamma _k = \sum _{i{\lt}k} \mathrm{exponents}_i\).

Along a filter of generators \(B_i \to A\) for which each fixed-\(n\) integral is continuous, the partial-sum rate is upper semicontinuous: \(\limsup _i \Gamma _k(B_i) \le \Gamma _k(A)\); specializing \(k=1\) gives the same for the top exponent. This is USC, not continuity — equality can fail when a spectral gap closes.

Fix a real time \( t_0 \). For almost every \( x \) and every test vector \( u \), the discrete-time growth \( \limsup \) of the cocycle applied to \( u \) at \( x \) equals that at \( \varphi (t_0)x \) applied to the pushed-forward vector \( A(t_0,x)\, u \).

For \(x\in X\) and \(v\in \mathbb {R}^d\) the growth sequence is

where \(A^{(n)}(x)=\mathtt{cocycle}\, A\, T\, n\, x\) is the \(n\)-step cocycle iterate acting on \(v\) via \(\mathtt{toEuclideanCLM}\).

Let \(f\) be operator convex on an interval \(I\), let \(A,B\) be a contraction pair (\(A^{*}A + B^{*}B = 1\)), and let \(X,Y\) be self-adjoint with spectra in \(I\). Then

If \(x \mapsto V(x)\) and \(x \mapsto W(x)\) are measurable subspace families, then so is \(x \mapsto V(x) \sqcap W(x)\).

Fix \(x\). If the forward envelope for \(V_x\) holds at rate \(a\), \(U_x\) decays backward at rate \(\le b\), and \(a + b {\lt} 0\), then \(V_x \sqcap U_x = \bot \).

Every point \(x\) has an \(n\)-step itinerary \(f : \operatorname {Fin}n \to \iota \), recording for each \(k {\lt} n\) which cell of \(P\) contains \(T^k x\); among the admissible codes the least one in a fixed enumeration is chosen, which makes the selector genuinely measurable (the cells may overlap on a null set, so a bare choice function would not be). The atom of \(x\) is the cell \(\bigcap _{k{\lt}n} T^{-k}(P_{f(k)})\) of the iterated join containing \(x\), and the information function is

the surprise of learning the \(n\)-name of \(x\). It is nonnegative and measurable (): in its simple-function form it is a finite sum of indicators of the itinerary fibers, each the difference of a join cell and the finitely many strictly smaller cells.

For self-adjoint \(Q\), a band indicator \(\chi =\mathbf1_{(c,\infty )}\), and a continuous \(f\ge 0\) on \(\mathrm{spec}(Q)\) with \(a\le f(t)\) whenever \(c{\lt}t\),

A matrix is a function \(m \to n \to \alpha \), and we equip \(\operatorname {Matrix}\, m\, n\, \alpha \) with the Pi (product) \(\sigma \)-algebra induced from the entry type \(\alpha \). For finitely many entries over a Borel \(\alpha \) this agrees with the Borel \(\sigma \)-algebra. Mathlib does not register this automatically because \(\operatorname {Matrix}\) is a def rather than reducibly the underlying Pi type, so the ambient Pi instance does not transfer; we install it explicitly.

The entrywise (Pi) measurable structure on \(\operatorname {Matrix}(\operatorname {Fin}d)(\operatorname {Fin}d)\, \mathbb {R}\) is an OpensMeasurableSpace for the L2 operator-norm topology, since that topology is installed (via replaceTopology) to be definitionally the Pi product topology, of which the Pi \(\sigma \)-algebra is exactly the Borel structure.

Under the same hypotheses, the limsup envelope \(f_+\) is integrable.

Let \(T\) be measure-preserving for a finite measure \(\mu \), \(A\) measurable and everywhere invertible, \(d \neq 0\), with both \(\log ^{+}\left\lVert A \right\rVert \) and \(\log ^{+}\left\lVert A^{-1} \right\rVert \) integrable. Then each \(x \mapsto \log \left\lVert A^{(n)}(x) \right\rVert \) is integrable. The companion \(\texttt{integrable\_ logNorm\_ inv\_ cocycle}\) gives the same for the inverse iterates.

If \(T\) is measure-preserving and \(g\) is integrable, then each Birkhoff partial sum and the maximal function \(\texttt{maxBirkhoff}\, T\, g\, N\) are integrable; if moreover \(g\) and \(T\) are measurable, then \(\texttt{maxBirkhoff}\, T\, g\, N\) is measurable.

The hypothesis \(\texttt{IntegrableLogNorm}\, A\, \mu \) asserts that the positive part of the log-norm of the generator is integrable: \(\log ^{+}\left\lVert A(\cdot ) \right\rVert \in L^{1}(\mu )\), where \(\log ^{+} t = \max (\log t, 0)\). This is the standard integrability assumption of the Furstenberg–Kesten and Oseledets theorems; combined with the same hypothesis for the inverse generator \(A^{-1}\) it pins both extremal Lyapunov exponents in \(\mathbb {R}\).

If \( g \in L^1(\mu ) \) dominates \( \log ^{+}\left\lVert A(s,x) \right\rVert \) for all \( s \in [0,1] \) and all \( x \), then the time-one map \( A(1,\cdot ) \) has integrable positive log-norm.

If \( g' \in L^1(\mu ) \) dominates \( \log ^{+}\left\lVert (A(s,x))^{-1} \right\rVert \) for all \( s \in [0,1] \) and all \( x \), then the inverse \( (A(1,\cdot ))^{-1} \) has integrable positive log-norm.

For measure-preserving \(T\) and integrable \(f\), \(\int \sum _{k{\lt}n} f(T^{k}x)\, d\mu = n\int f\, d\mu \).

For every \(n\),

the Shannon entropy of the \(n\)-fold iterated join (the \(n\)-th term of the Kolmogorov–Sinai entropy sequence).

The channel adjoint intertwines the modular \(it\)-flows if, for all \(t\),

If IntertwinesIt holds (all four states faithful), then the Petz map recovers the input: \(P_{\sigma ,\Lambda }(\Lambda \rho )=\rho \).

An invariant subbundle is a measurable family of fibre subspaces \(W(x) \le \mathbb {R}^d\) that is \(A\)-equivariant a.e.: \(A(x)\, W(x) = W(Tx)\).

A finite measurable partition \(P\) is (one-sided) generating for \((\alpha ,T,\mu )\) if the forward-saturated \(\sigma \)-algebra it generates is the ambient one:

where \(\sigma (P)\) is the \(\sigma \)-algebra generated by the cells of \(P\). This is the standard generator condition for a (possibly non-invertible) endomorphism: the whole measurable structure is recovered from the observable \(P\) and its forward time-translates.

For a measure-preserving automorphism \(e:\alpha \simeq \alpha \), a finite partition \(P\) is two-sided generating if the \(\sigma \)-algebra saturated under both time directions is the ambient one:

This is the correct condition for invertible systems: forward one-sided generation is strictly stronger and provably fails for genuine automorphisms such as the two-sided Bernoulli shift.

The two-sided saturation of a finite partition \(P\) under an automorphism \(e\) is the \(\sigma \)-algebra \(\bigvee _{n\in \mathbb {Z}} e^{-n}\sigma (P)\) generated by the two-sided \(P\)-itinerary. The partition two-sidedly generates \((\alpha , e, \mu )\) mod \(0\) when the ambient \(\sigma \)-algebra is contained in the \(\mu \)-completion of the saturation — every measurable set is recovered from the itinerary up to a null set. This mod-\(0\) form (not the literal equality of \(\sigma \)-algebras) is the faithful conclusion of Krieger’s theorem. The \(\mathrm{Countable}\)-indexed analogue for a family of cells \(Q : \kappa \to \mathrm{Set}\, \alpha \) is .

If \(\nu \) charges two distinct symbols \(i \ne j\) with different masses (\(\nu \{ i\} \ne \nu \{ j\} \)), then the witness partition is heterogeneous: two of its cells carry distinct \(\hat\mu \)-mass (IsHeterogeneous, the honest non-uniformity predicate whose negation is exactly the equal-measure hypothesis of the monofractal degeneracy \(D_q \equiv \log N / (-\log \varepsilon )\)).

For a self-map \(T\) of \(\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) and a finite measurable partition \(\xi \), the predicate \(\texttt{IsInjectivityPartition}\, \mu \, T\, \xi \) packages the two hypotheses the conditional-expectation proof needs: \(T\) is injective on each cell of \(\xi \), and each cell is measurable. (These are literally the hypotheses of Mathlib’s change-of-variables lemma; no Markov condition and no generating condition are baked in.)

For a measure \(\mu \), map \(T\), generator \(A\), count \(k\), exponent list \(\lambda : \mathrm{Fin}\, k \to \mathbb {R}\) and flag \(V : \mathrm{Fin}(k+1) \to X \to \mathrm{Submodule}\), the predicate \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) asserts: \(\lambda \) is strictly antitone; each level \(V_i\) is a measurable subspace family; and \(\mu \)-a.e. \(x\) carries the strictly decreasing \(A\)-equivariant flag \(\mathbb {R}^d = V_0(x) \supsetneq \cdots \supsetneq V_k(x) = 0\) with exact growth rate \(\lambda _i\) on the stratum \(V_i \setminus V_{i+1}\). This is byte-identical to the conclusion of the main theorem.

A sequence \(g : \mathbb {N}\to X \to \mathbb {R}\) is a subadditive cocycle over \(T\) when

For \(g_n = \log \left\lVert A^{(n)} \right\rVert \) this is submultiplicativity of the operator norm composed with the cocycle identity.

Assume \(\det A \neq 0\) everywhere and \(d \neq 0\). Then \(g_n(x) = \log \left\lVert A^{(n)}(x) \right\rVert \) is a subadditive cocycle over \(T\):

Under the same hypotheses, \(g_n(x) = \log \left\lVert (A^{(n)}(x))^{-1} \right\rVert \) is a subadditive cocycle over \(T\).

\(\mathrm{restLog}\, A\, V\, T\) is an everywhere subadditive cocycle: for all \(m,n,x\), \(\mathrm{restLog}\, (m+n)\, x \le \mathrm{restLog}\, m\, x + \mathrm{restLog}\, n\, (T^{[m]}x)\).

Let \(E\) be a real vector space. A function \(g\colon E\to \mathbb {R}\) is an ultrametric growth function when it is scaling-invariant,

and non-Archimedean (strong triangle inequality),

The value \(g(0)\) is never used; the side conditions \(v\neq 0\) are carried explicitly to avoid extended-real arithmetic.

Under the hypotheses of 4.10, for a.e. \(x\) the function \(v\mapsto \bar\lambda (v)\) is an ultrametric growth function.

The level sets \(\{ x : 0 {\lt} \texttt{maxBirkhoff}\, T\, g\, N\, x\} \) are monotone in \(N\), and their union over all \(N\) is exactly \(\{ x : \exists n,\ 0 {\lt} \texttt{birkhoffSum}\, T\, g\, (n+1)\, x\} \).

On a probability space with \(0 {\lt} d\), any Oseledets filtration has \(0 {\lt} k\).

Let \(D = (D_{km})\) be a doubly stochastic \(K\times M\) matrix (\(D_{km}\ge 0\), all row sums and all column sums equal to \(1\)), let \(p\ge 0\) on \(K\) and \(s\ge 0\) on \(M\) have equal total mass \(\sum _k p_k = \sum _m s_m\), and assume the support condition \(s_m = 0\Rightarrow D_{km}p_k = 0\). Writing \(a_m = \sum _k D_{km}p_k\) for the column marginal,

A Kraus channel on \(\operatorname {Matrix}_n(\mathbb {C})\) is a finite family of Kraus operators \(K : \iota \to \operatorname {Matrix}_n(\mathbb {C})\) satisfying the completeness relation \(\sum _i K_i^{\dagger }K_i = 1\). Its Schrödinger action is \(\Lambda (X)=\sum _i K_i\, X\, K_i^{\dagger }\) (Lean: toMat, restricted to states as toDM), and its Heisenberg (Hilbert–Schmidt) adjoint is \(\Lambda ^{\dagger }(X)=\sum _i K_i^{\dagger }X\, K_i\) (Lean: adj).

A Kraus channel is trace preserving, \(\operatorname{tr}(\Lambda X)=\operatorname{tr}X\) for every \(X\); consequently the adjoint is unital, \(\Lambda ^{\dagger }(1)=1\) (Lean: adj_unital).

Let \(e\) be an ergodic, aperiodic (: every set of \(n\)-periodic points, \(n \ne 0\), is \(\mu \)-null), measure-preserving automorphism of a probability space, and let \(k \in \mathbb {N}\) satisfy

where \(h(e)\) is the Kolmogorov–Sinai entropy of the system. If the Krieger coding construction supplies a coding datum (Definition 10.17), then \(e\) admits a finite two-sided generator of size \(\le k\), mod \(0\): a partition \(P\) indexed by \(\operatorname {Fin}k\) with \(\mathrm{IsGeneratingTwoSidedMod0}\ e\ P\). The entropy threshold is pinned to the genuine \(h(e)\), so the hypothesis is a real entropy constraint. Interface disclosure: the coding datum has no in-repo constructor — the tower-painting combinatorics that would discharge it from the dynamical hypotheses alone are not formalized — so this is the honest conditional form of Krieger’s theorem, with the dynamical hypotheses retained as the faithful classical interface that the upstream layers (Theorem 10.11, Theorem 10.12, Theorem 10.13 and Theorem 10.16) are designed to feed.

Given a Krieger coding datum \(D\) for \((e, \mu , k)\), there exists a partition \(P\) into at most \(k\) cells that two-sidedly generates \((\alpha , e, \mu )\) mod \(0\). No entropy, ergodicity or aperiodicity hypotheses enter: those are consumed upstream, in producing \(D\). This is the pure recovery content of Krieger’s theorem.

For an automorphism \(e\) and \(k \in \mathbb {N}\), a Krieger coding datum bundles: the measure-preservation of \(e\); a countable index type \(\kappa \) with measurable cells \(Q : \kappa \to \mathrm{Set}\, \alpha \) two-sidedly generating mod \(0\); and a \(\operatorname {Fin}k\)-valued partition \(P\) that codes \(Q\) two-sidedly mod \(0\) (): the two-sided \(P\)-itinerary recovers each \(Q\)-cell up to a \(\mu \)-null set. This is exactly the object the Krieger construction produces when \(\log k\) exceeds the entropy: \(Q\) from Theorem 10.16, and \(P\) from the column coding of the \(\le k^{N}\) good names (Theorem 10.12 and Theorem 10.13) along refining Rokhlin towers (Theorem 10.11).

For faithful states \(\rho ,\sigma \), with (vectorised) relative modular operator \(\Delta =\sigma \otimes (\rho ^{-1})^{\top }\) and cyclic vector \(\xi =\operatorname {vec}(\rho ^{1/2})\),

The Kolmogorov–Sinai entropy of the system is the supremum of the partition-relative entropies over all finite measurable partitions,

taken in the complete lattice \(\overline\mathbb {R}=[-\infty ,+\infty ]\) (EReal) so that the definition is total even when the entropy is infinite. The supremum ranges over \(\operatorname {Fin}n\)-indexed partitions for every \(n\in \mathbb {N}\), which by reindexing invariance realizes the full partition supremum; each \(h(T,\alpha )\) is below \(h(T)\) (), and \(h(T)\ge 0\), witnessed by the trivial one-cell partition.

The Kolmogorov–Sinai entropy (Definition 9.13) of the time-\(1\) map of the Bernoulli suspension flow equals the single-symbol Shannon entropy:

In particular the flow’s metric entropy (defined as the entropy of its time-\(1\) map) is \(H(\nu )\), strictly positive for a genuinely biased \(\nu \).

Let \(T\) be a measure-preserving transformation of a standard Borel probability space and \(P\) a one-sided generating finite partition. Then the entropy of the system is attained on \(P\):

No ergodicity is required; standard Borelness and the probability hypothesis feed the kernel disintegration, and the saturation supplied by the generating hypothesis is load-bearing.

Let \(e\) be a measure-preserving automorphism of a standard Borel probability space and \(P\) a two-sided generating finite partition. Then

Under the same positivity hypothesis, the full CNT dynamical entropy of \(\mathrm{adPerm}\, \sigma \) in the state \(\rho _\mu \) — the supremum over all operational partitions — dominates the classical Kolmogorov–Sinai entropy:

The Kolmogorov–Sinai entropy of \(T\) relative to a finite partition \(\alpha \) is the Fekete limit of the subadditive iterated-join entropy sequence,

packaged through Mathlib’s \(\texttt{Subadditive.lim}\) (an infimum of the averaged terms, so the definition is total).

For the binary partition \(\alpha = \{ [0,\tfrac 12), [\tfrac 12,1)\} \) of the circle (), the partition-relative Kolmogorov–Sinai entropy under the doubling map is exactly \(\log 2\).

On a standard Borel space (with \(\iota \) nonempty), the Kolmogorov–Sinai entropy of the pair equals the conditional entropy of \(P\) given the \(\sigma \)-algebra of the strict future:

This is the integral-level statement of the sharp SMB rate: the precise constant the pointwise theorem converges to. No ergodicity is needed.

Let \(T\) be a measure-preserving, differentiable self-map of \(\mathbb {R}^d\) with \(\mu \ll \mathrm{vol}\), everywhere-nonsingular derivative, a one-sided generating finite partition \(\xi \) on whose cells \(T\) is injective, and \(\mu \)-integrable \(\log \rho \) (\(\rho \) the density \(d\mu /d\mathrm{vol}\)) and \(\log \left\lvert \det DT \right\rvert \). Then the per-partition entropy is the integrated volume distortion:

Together with the determinant identity of Theorem 6.20, the right-hand side is the sum \(\sum _i\lambda _i\) of all Lyapunov exponents of the derivative cocycle — so for expanding maps (all exponents positive) this saturates the Margulis–Ruelle bound, giving Pesin’s entropy formula in that regime.

Let \(T\) preserve a probability measure and let \(P\) be a finite partition indexed by a type of cardinality \(b\) such that for every \(n\), every cell of the \(n\)-fold join \(\bigvee _{k=0}^{n-1}T^{-k}P\) has measure exactly \(b^{-n}\). Then \(h(P,T) = \log b\).

The iterated-join entropy sequence of \((T,\alpha )\) is

the Shannon entropy of the flat \(n\)-fold join. Its term at \(0\) is \(0\), and every term is nonnegative.

On a standard Borel space, the \(n\)-step join entropy telescopes into conditional entropies:

where the \(k\)-th conditioning \(\sigma \)-algebra is generated by the cells of the \(T\)-pullback of the \(k\)-step join.

For a measure-preserving \(T\) on a probability space and all \(n,m\),

For a measure-preserving \(T\) and a finite measurable partition \(\alpha \), the iterated join \(\bigvee _{k=0}^{n-1}T^{-k}\alpha \) is realized as the partition indexed by the flat function type \(\operatorname {Fin}n\to \iota \), whose cell at \(f\) is the intersection \(\bigcap _{k{\lt}n} T^{-k}\bigl(\alpha _{f(k)}\bigr)\). Cells are measurable as finite intersections of preimages under the iterates \(T^k\), pairwise a.e. disjoint (two distinct indices disagree at some coordinate \(k\), where measure-preservation of \(T^k\) transports the disjointness of \(\alpha \)), and cover the space. For \(n=0\) this is the trivial one-cell partition.

The upper Lyapunov growth function is the \(\limsup \) of the growth sequence,

For nonzero \(v,w,v+w\), if the three growth sequences are bounded, then \(\bar\lambda (v+w)\le \max (\bar\lambda (v),\bar\lambda (w))\).

On the good set, if \(v\in \mathrm{vflag}(A,T,x)(i)\) but \(v\notin \mathrm{vflag}(A,T,x)(i{+}1)\), then \(\bar\lambda _x(v)=\mathrm{specList}(i)=\lambda _i\).

Under the same hypotheses, for a.e. \(x\) and every \(v\neq 0\),

Assume \(T\) ergodic on a probability space, \(A\) measurable and invertible, with \(\log \left\lVert A \right\rVert \) and \(\log \left\lVert A^{-1} \right\rVert \) integrable. Then there exist \(\lambda _{\mathrm{bot}}\le \lambda _{\mathrm{top}}\) such that for a.e. \(x\) and every \(v\neq 0\), \(\bar\lambda (v)\in [\lambda _{\mathrm{bot}},\lambda _{\mathrm{top}}]\).

For \(c\neq 0\) and \(v\neq 0\), \(\bar\lambda (c\cdot v)=\bar\lambda (v)\).

The sublevel subspace at threshold \(t\),

is the submodule 4.6 of \(\bar\lambda _x\) at \(t\) on the good set, and \(\bot \) off it.

For a subadditive cocycle and \(n : \mathbb {N}\), one has \(g\, (n+1)\, x \le \texttt{birkhoffSum}\, T\, (g\, 1)\, (n+1)\, x\); more generally, for any decomposition of \([0,N)\) into \(k+1\) consecutive blocks of lengths \(\ell _0, \dots , \ell _k\), the cocycle is dominated by the sum of the block values along the orbit at the frontiers \(T^{[\sum _{j{\lt}i}\ell _j]}x\).

For thresholds \(c\le c'\) with limit band projectors \(P,P'\), if \(Pv=0\) then \(P'v=0\).

The pointwise limsup \(x \mapsto \limsup _n \texttt{birkhoffAverage}\, \mathbb {R}\, T\, g\, n\, x\) is a.e. \(T\)-invariant.

For a finite measure, measure-preserving \(T\), an integrable subadditive cocycle with normalized integrals bounded below, the limsup envelope \(f_+(x) = \limsup _n \texttt{cdiv}\, g\, n\, x\) (and likewise the liminf envelope \(f_-\)) is a.e. \(T\)-invariant.

There is a forward top value \(\lambda _1^+\) (the a.e. limit of \(\tfrac 1n\log ^+\left\lVert A^{(n)} \right\rVert \)) such that, whenever \(\lambda _1^+ {\gt} 0\), \(\mu \)-a.e. the genuine log-norm \(\limsup \) is exactly \(\lambda _1^+\):

The positivity hypothesis is essential; in the contracting case \(\lambda _1^+ = 0\) the genuine growth may tend to \(-\infty \) and equality fails.

Under the same singular hypotheses there is \(\lambda _1^+\) with, \(\mu \)-a.e.,

The \(\limsup \) is taken in \(\mathrm{EReal}\) so the bound is unconditional even when the growth tends to \(-\infty \); this is one-sided only.

For ergodic \(T\) and a possibly-singular generator with \(\log ^+\left\lVert A \right\rVert \in L^1\), there is a constant \(\Gamma _k^+\) with, \(\mu \)-a.e.,

The top-\(k\) volume growth is bounded above unconditionally (the \(\mathrm{EReal}\) \(\limsup \) allows volume collapse), again one-sided only.

This lemma belonged to a superseded determinant/volume-squeeze route and has no counterpart in the current Lean development; the statement is kept for exposition and the label only so that cross-references resolve. Given a volume cocycle whose top, slow and remaining log-exponent sequences satisfy a sum law \(\mathrm{vol} = \mathrm{slow} + \mathrm{rest}\) with the appropriate limits, the slow restricted-operator-norm exponent obeys \(\limsup _n \tfrac 1n\log (\mathrm{slow}_n) \le \lambda _i\).

If \(g\) is an ultrametric growth function and \(v\colon \iota \to E\) is a family of nonzero vectors with \(g\circ v\) injective, then \(v\) is linearly independent over \(\mathbb {R}\).

For a measure \(\mu \) on a (pseudo-)metric measurable space \(E\) and a point \(x\), the upper local (pointwise) dimension is

the \(\limsup \) along the filter \(r \to 0^+\) of the closed-ball mass quotient. Where the genuine limit exists (as in the absolutely-continuous case below), this \(\limsup \) is the honest local dimension.

For an ergodic, log-integrable, differentiable uniformly expanding map with constant \(K {\gt} 1\) (and \(d\ge 1\)), each Lyapunov exponent of the tangent cocycle satisfies \(\log K \le \lambda _i\).

If \(P^{c}_n(x)\to P\) with \(c{\gt}0\) and \(Pv\neq 0\), and the cocycle growth sequence is cobounded, then

For \(\det A \neq 0\) everywhere and \(d \neq 0\),

Under the same hypotheses,

Let \(p : \iota \to \mathbb {R}\) satisfy \(p_i \ge 0\) for all \(i\) and \(p_i {\gt} 0\) for some \(i\). Then \(q \mapsto \log Z_q\) is convex on all of \(\mathbb {R}\). This is the cumulant-convexity / Hölder property, the mathematical core of the multifractal theory.

The Lyapunov spectrum at \(x\) is the finite set of realized values

defined as a Finset via 4.5 on the good set where \(\bar\lambda _x\) is an ultrametric growth function, and as \(\emptyset \) off it. A value lies in it iff it is realized by some nonzero vector.

Given a.e. that every realized value of the upper growth function is a deterministic exponent (upper inclusion) and every deterministic exponent is attained (lower inclusion), for \(\mu \)-a.e. \(x\),

If at \(x\) every realized exponent is a deterministic one and every deterministic exponent is attained, then \(\mathrm{lyapunovSpectrum}(x) = \mathrm{distinctExp}\, \lambda ^0\, d\).

Let \(T\) be an ergodic self-map of \(\mathbb {R}^d\) with everywhere-nonsingular derivative cocycle and one-sided log-integrable derivative data (Definition 2.4 for \(DT\) and \(DT^{-1}\)), and suppose the geometric atom-counting bound holds: every finite partition \(\alpha \) satisfies \(h(T,\alpha )\le \sum _{\lambda _i{\gt}0}\lambda _i\), the sum of the strictly positive Lyapunov exponents of the derivative cocycle (a deterministic constant, the spectrum being a.e. constant by ergodicity). Then the system entropy obeys

Same setting (ergodic \(T\) on \(\mathbb {R}^d\), nonsingular log-integrable derivative cocycle). Assume only the honest non-compactness input — the Mañé/Katok geometric atom count: for every finite partition \(P\) there are \(\varepsilon {\gt}0\) and \(C\ge 0\) such that, \(\mu \)-a.e., the number of atoms of the \(n\)-fold refinement meeting an orbit eventually satisfies

the \(\varepsilon \)-covering number of the image ellipsoid. Then

Some such distortion hypothesis is unavoidable on the noncompact phase space: the bare inequality is false in general (Riquelme 2017).

The mass exponent of the family \(p\) at scale \(\varepsilon \) is

defined for every \(q\) with no case split. For a probability family \(\tau (1) = 0\), since \(Z_1 = 1\).

Under the same hypotheses on \(p\), for a scale \(0 {\lt} \varepsilon {\lt} 1\) the mass exponent \(q \mapsto \tau (q) = \log Z_q / \log \varepsilon \) is concave on \(\mathbb {R}\).

For a measurable \(T\), a function \(g : X \to \mathbb {R}\), \(N : \mathbb {N}\) and \(x\), the maximal function is

the nonempty Finset.sup’ of the Birkhoff partial sums over \(k \in \texttt{range}\, (N+1)\). Since the \(k = 0\) term equals \(\texttt{birkhoffSum}\, T\, g\, 0\, x = 0\), the maximal function is its own positive part.

On the set where the maximal function is positive, for every \(x\) with \(0 {\lt} \texttt{maxBirkhoff}\, T\, g\, N\, x\),

For all \(g, N, x\) one has \(0 \le \texttt{maxBirkhoff}\, T\, g\, N\, x\).

For all \(g, N, x\),

For a fixed real polynomial \(q\), the map \(a\mapsto q(a)\) on \(\mathrm{Mat}_{d\times d}(\mathbb {R})\) is measurable.

Let \(M\) be measurable with each \(M x\) self-adjoint, and \(f\colon \mathbb {R}\to \mathbb {R}\) continuous. Then \(x\mapsto \mathrm{cfc}\, f\, (M x)\) is measurable.

Let \(M\colon X\to \mathrm{Mat}_{d\times d}(\mathbb {R})\) be measurable with each \(M x\) self-adjoint, and let \(g\colon \mathbb {R}\to \mathbb {R}\). If a fixed polynomial \(q\) agrees with \(g\) on the spectrum of every \(M x\), then \(x\mapsto \mathrm{cfc}\, g\, (M x)\) is measurable.

If \(A\) and \(T\) are measurable then for each \(n\) the iterate \(x \mapsto A^{(n)}(x)\) is measurable for the entrywise structure 2.1.

The determinant \(M \mapsto \det M\) is measurable.

The inverse \(M \mapsto M^{-1}\) is measurable on the entrywise structure.

The map \(M \mapsto \left\lVert M \right\rVert \) on \(\operatorname {Matrix}(\operatorname {Fin}d)(\operatorname {Fin}d)\, \mathbb {R}\) is measurable.

For fixed \(v\), the map \(x\mapsto \bar\lambda _x(v)\) is measurable.

A subspace-valued map \(V\colon X\to \mathrm{Submodule}\, \mathbb {R}\, \mathbb {R}^d\) is a measurable family of subspaces when \(x\mapsto \mathrm{orthProjMatrix}(V x)\) is measurable. Equivalently (measurable_orthProjMatrix_iff), for each standard basis index \(j\) the \(\mathbb {R}^d\)-valued map \(x\mapsto (V x).\mathtt{starProjection}(e_j)\) is measurable.

For a finite measure, measure-preserving \(T\), integrable \(g\) and \(\varepsilon {\gt} 0\), the superlevel set where the limsup of the Birkhoff averages exceeds \(\mu [g\mid \mathcal I] + \varepsilon \) is null.

A finite measurable partition of \((\alpha ,\mu )\) is a structure bundling a Fintype-indexed family of cells \(A_i\subseteq \alpha \) together with proofs that each cell is measurable, that the cells are pairwise almost-everywhere disjoint, and that they cover the whole space, \(\bigcup _i A_i=\alpha \).

\(\operatorname {catTorus}\) preserves the Haar probability measure on \(\mathbb {T}^2\).

A measure-preserving one-parameter flow on a measurable space \( X \) for a measure \( \mu \) is a family \( \varphi : \mathbb {R}\to X \to X \) together with the data \( \varphi (0) = \mathrm{id} \), \( \varphi (s+t) = \varphi (s) \circ \varphi (t) \) for all \( s, t \in \mathbb {R}\), and a proof that each time-\( t \) map \( \varphi (t) \) preserves \( \mu \). No topology on \( X \) is assumed; in particular no joint continuity in \( (t, x) \) is required.

Unconditionally, for a faithful ancilla \(\alpha \), a unitary dilation \(U\), and faithful \(\sigma \),

This is the data-processing inequality for the faithful-ancilla mixed-Stinespring family; that family does not contain every CPTP channel (amplitude damping lies outside it, since its exact dilation needs a pure, non-faithful ancilla), so it is not an in-repo DPI for a general Kraus channel.

If a nonnegative sequence \(a\) obeys a one-step recursion fed by finitely many source sequences each decaying geometrically with ratio \(\rho {\lt}1\), then \(a_n\) is bounded by a fixed multiple of the summed source envelopes for all \(n\).

For a measure-preserving flow \( \varphi \) and \( n \in \mathbb {N}\), the integer-time map of the flow is the \( n \)-fold iterate of its time-one map: \( \varphi (n) = (\varphi (1))^{[n]} \).

Under the same hypotheses,

If a map \(R\) satisfies the faithful data-processing inequality and inverts a coarse-graining \(\Lambda \) on the pair \(\rho ,\sigma \) (\(R(\Lambda \rho ) = \rho \), \(R(\Lambda \sigma ) = \sigma \) with \(\Lambda \sigma \) faithful), then a strict drop \(S(\Lambda \rho \| \Lambda \sigma ) {\lt} S(\rho \| \sigma )\) is impossible.

Unconditionally: a strict relative-entropy drop under a coarse-graining \(\Lambda \) (an endomorphism of the input space) rules out any Stinespring recovery channel \(R\, x = \operatorname{Tr}_E(U(x\otimes \alpha )U^{*})\) inverting \(\Lambda \) on \(\rho ,\sigma \).

Assume \(\det A(x) \neq 0\) for all \(x\) and \(d \neq 0\). Then \(0 {\lt} \left\lVert A^{(n)}(x) \right\rVert \) for every \(n, x\). The analogous statement \(\texttt{norm\_ inv\_ cocycle\_ pos}\) holds for the inverse iterates \(\left\lVert (A^{(n)}(x))^{-1} \right\rVert \).

When \(d \neq 0\), \(\left\lVert (1 : \operatorname {Matrix}(\operatorname {Fin}d)(\operatorname {Fin}d)\, \mathbb {R}) \right\rVert = 1\) for the L2 operator norm.

For a self-adjoint matrix \(M\) and any function \(g\),

where \(\mu _j\) ranges over the sorted eigenvalues of \(M\).

\((P_K\, P_L\, P_K)\, v = v\) if and only if \(v \in K \sqcap L\).

An operational partition of unity of size \(k\) is a family \((x_i)_{i{\lt}k}\) of operators in \(\operatorname {Matrix}_d(\mathbb {C})\) satisfying the partition-of-unity relation \(\sum _i x_i^{\dagger }x_i=1\). This is the noncommutative analogue of a measurable partition of the state space.

The function \(x\mapsto -\log x\) is operator convex on \((0,\infty )\): for every matrix dimension its continuous functional calculus is convex in the Loewner order on the self-adjoint matrices with spectrum in \((0,\infty )\).

For \(f:\mathbb {R}\to \mathbb {R}\) and matrices \(L,R\) with \(R\) positive definite, the operator perspective is

with the functional calculus and real powers supplied by the continuous functional calculus.

Let \(f\) be operator convex on \(I\), let \(R_1,R_2\) be positive definite with the sandwiched arguments \(R_i^{-1/2}L_iR_i^{-1/2}\) self-adjoint and with spectra in \(I\), and let \(c\in [0,1]\). Then

The same formula \(P_f(L,R) = R^{1/2}f(R^{-1/2}LR^{-1/2})R^{1/2}\) for matrices indexed by an arbitrary finite type \(m\) (rather than \(\operatorname {Fin}N\)).

Under the same hypotheses as Theorem 13.19, joint convexity of \(\mathrm{opPersp}\, f\) holds over an arbitrary finite index type \(m\).

For positive-definite \(\rho ,\sigma \), the perspective of \(-\log \) at the commuting pair \(L = 1\otimes \sigma ^{\top }\), \(R = \rho \otimes 1\) has the closed form

For \(K\le \mathbb {R}^d\), \(\mathrm{orthProjMatrix}(K)\) is the matrix of the orthogonal projection onto \(K\), namely the preimage of \(K.\mathtt{starProjection}\) under the star-algebra isomorphism \(\mathtt{toEuclideanCLM}\). A subspace is determined by this matrix, which lives in a space carrying the Borel/Pi measurable structure. Its \((i,j)\) entry equals the \(i\)-th coordinate of the projection applied to the standard basis vector \(e_j\) (orthProjMatrix_apply).

Let \(\mu \) be a probability measure, \(T:X\to X\) ergodic measure-preserving, and \(A:X\to \mathrm{Mat}_{d\times d}(\mathbb {R})\) measurable with \(\det (A x)\neq 0\) and \(\log ^{+}\left\lVert A \right\rVert ,\, \log ^{+}\left\lVert A^{-1} \right\rVert \in L^1(\mu )\). Then there are \(k\) distinct Lyapunov exponents \(\lambda :\mathrm{Fin}\, k\to \mathbb {R}\), strictly decreasing, and a measurable family of subspaces

with each \(x\mapsto V_i\, x\) measurable, such that for \(\mu \)-a.e. \(x\): \(V_0\, x=\top \), \(V_k\, x=\bot \); the flag is strictly decreasing, \(V_{i+1}\, x {\lt} V_i\, x\); it is \(A\)-equivariant, \(A(x)\, V_i\, x = V_i\, (Tx)\); and along it the cocycle grows at the exact rate \(\lambda _i\):

Under the standing hypotheses (ergodic \(T\), invertible measurable \(A\) with \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1\)), there exist \(k, \lambda , V\) with \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\).

Let \(\mu \) be a probability measure on \(E = \operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) and let \(T\) be ergodic for \(\mu \), differentiable, with everywhere nonvanishing Jacobian determinant \(\det (\operatorname {derivativeCocycle}\, T\, x)\ne 0\) and with the log-integrability \(\log ^{+}\left\lVert D_xT \right\rVert ,\ \log ^{+}\bigl\lVert (D_xT)^{-1} \bigr\rVert \in L^1(\mu )\) (stated for the matrix generator and its matrix inverse; by the isometry these are exactly the \(\operatorname {fderiv}\) conditions). Then:

1. for every \(n\) and \(x\), the cocycle iterate represents \(D_x(T^{[n]})\) — the cocycle is the genuine tangent cocycle; and

2. there exist \(k\le d\), strictly decreasing exponents \(\lambda _1 {\gt} \dots {\gt} \lambda _k\), and a measurable family of subspaces \(E = V_0(x) \supsetneq V_1(x) \supsetneq \dots \supsetneq V_k(x) = 0\), a.e. equivariant under \(D_xT\), such that for every \(v\in V_{i-1}(x)\setminus V_i(x)\),

   \[ \frac1n\, \log \bigl\lVert D_x\bigl(T^{[n]}\bigr)v \bigr\rVert \; \longrightarrow \; \lambda _i . \]

Under the one-sided hypotheses (with \([\mathrm{NeZero}\, d]\)) there exist a decreasing exponent sequence \(\mathrm{lam0} : \mathbb {N}\to \mathbb {R}\) realizing the a.e. per-index singular-value limits, and a measurable filtration \(V : \mathrm{Fin}(k+1) \to X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\) where \(k = \mathrm{numExp}\, \mathrm{lam0}\, d\), such that for a.e. \(x\): \(V_0 x = \top \), \(V_k x = \bot \), \(V\) is strictly decreasing and \(A\)-equivariant, every \(v \in V_{i}x \setminus V_{i+1}x\) grows at rate \(\mathrm{expEnum}\, \mathrm{lam0}\, d\, i\), and

Under the standing ergodic, invertible, log-integrable hypotheses, and assuming the top-gap envelope \(\mathrm{TopGapMassEnvelope}\) quantified over \(\lambda ^0\), the full Oseledets filtration conclusion holds.

Assume the per-vector spectral upper bound on the slow flag, the reverse slow-flag inclusion, the two spectrum inclusions, and the band-projector convergence datum. Then there exist \(k\), strictly decreasing \(\lambda :\mathrm{Fin}\, k\to \mathbb {R}\), and a measurable family \(V\) forming a.e. a strictly decreasing \(A\)-equivariant flag along which \(\tfrac 1n\log \left\lVert A^{(n)}(x)v \right\rVert \to \lambda _i\) on each stratum.

Under the standing hypotheses there exist \(k, \lambda , V\) and a strictly decreasing \(m\) with \(m_0 = d\), \(m_k = 0\), such that \(\mathrm{IsOseledetsFiltration}\ \mu \ T\ A\ k\ \lambda \ V\) holds and \(\mu \)-a.e. \(\mathrm{finrank}\, V_i(x) = m_i\).

Let \( \mu \) be a probability measure on \( X \), let \( \varphi \) be a measure-preserving one-parameter flow whose time-one map \( \varphi (1) \) is \( \mu \)-ergodic, and let \( A \) be a continuous-time linear cocycle over \( \varphi \) valued in invertible \( d \times d \) real matrices. Suppose \( g, g' \in L^1(\mu ) \) satisfy, for all \( s \in [0,1] \) and all \( x \),

Then there exist \( k \in \mathbb {N}\), a strictly decreasing sequence of exponents \( \lambda : \mathrm{Fin}\, k \to \mathbb {R}\), and a measurable family of subspaces \( V : \mathrm{Fin}(k+1) \to X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathrm{EuclideanSpace}\, \mathbb {R}\, (\mathrm{Fin}\, d)) \) such that:

• \( \lambda \) is strictly decreasing and each \( V_i \) is a measurable subspace family;

• (full flow equivariance) for every \( t \in \mathbb {R}\), almost every \( x \) has \( A(t,x) \cdot V_i\, x = V_i\, (\varphi (t)x) \) for all \( i \);

• almost every \( x \) carries the strict flag \( \top = V_0\, x \supsetneq \cdots \supsetneq V_k\, x = \bot \), and on each stratum \( v \in V_i\, x \setminus V_{i+1}\, x \) the continuous-time growth rate is exactly \( \lambda _i \):

  \[ t^{-1}\log \left\lVert A(t,x)v \right\rVert \to \lambda _i \quad (t \to \infty ). \]

Let \(T : X \simeq _m X\) be an invertible ergodic measure-preserving transformation of a probability space, and let \(A : X \to \mathrm{Matrix}\, (\mathrm{Fin}\, d)\, (\mathrm{Fin}\, d)\, \mathbb {R}\) be measurable with \(\det A(x) \neq 0\) for all \(x\) and \(\log ^+\left\lVert A \right\rVert , \log ^+\left\lVert A^{-1} \right\rVert \in L^1(\mu )\). Then there exist \(k \in \mathbb {N}\), a strictly decreasing \(\lambda : \mathrm{Fin}\, k \to \mathbb {R}\), and measurable subspace families \(E : \mathrm{Fin}\, k \to X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\) such that for \(\mu \)-a.e. \(x\):

• \(\mathbb {R}^d = \bigoplus _{i} E_i(x)\) is an internal direct sum with every \(E_i(x) \neq \bot \);

• each \(E_i\) is \(A\)-equivariant: \(\bigl(A(x)\bigr)\bigl(E_i(x)\bigr) = E_i(Tx)\);

• for every nonzero \(v \in E_i(x)\),

  \[ \tfrac {1}{n}\log \bigl\lVert A^{(n)}(x)\, v \bigr\rVert \to \lambda _i \qquad \text{and}\qquad \tfrac {1}{n}\log \bigl\lVert \bigl(A^{(n)}(T^{-n}x)\bigr)^{-1}\, v \bigr\rVert \to -\lambda _i. \]

Any constant \(c\) to which \(\tfrac 1n\log \left\lVert A^{(n)}(x) \right\rVert \) converges \(\mu \)-a.e. (e.g. the Furstenberg–Kesten constant) equals \(\lambda _0\).

\(\Lambda (x) := (\, \lim _n (q_n(x))_{ij}\, )_{ij}\) is the entrywise real \(\limsup \)/limit of the matrix entries of \(q_n(x)\); it is a total, measurable function of \(x\).

For \(\mu \)-a.e. \(x\), \(\Lambda (x)\) is self-adjoint and positive semidefinite.

Under the same entropy-preservation hypothesis, the amplified output modular \(it\)-cocycle equals the input one, for all \(t\in \mathbb {R}\):

If the partial-trace relative entropy is preserved, \(S(\operatorname {Tr}_B\omega \| \operatorname {Tr}_B\tau )=S(\omega \| \tau )\), then the rectangular \(-\log \) operator-Jensen gap for the Petz isometry \(W\) annihilates the output cyclic vector \(\xi =\operatorname {vec}((\operatorname {Tr}_B\omega )^{1/2})\):

For an operator \(M\) on a bipartite system \(\mathbb {C}^{n_A}\otimes \mathbb {C}^{n_B}\), the partial trace over the \(B\) factor is

an operator on \(\mathbb {C}^{n_A}\). (The left partial trace \(\operatorname{Tr}_A\) is defined symmetrically.)

For any state \(\rho \) and any ancilla state \(\alpha \), \(\operatorname{Tr}_E(\rho \otimes \alpha ) = \rho \).

For a finite weight family \(p : \iota \to \mathbb {R}\) and \(q \in \mathbb {R}\), the generalized partition function is

the sum over the occupied cells only. The positivity guard is load-bearing at \(q = 0\): it forces empty cells (\(p_i = 0\)) to contribute \(0\) rather than \(0^0 = 1\), so that \(Z_0\) counts the occupied cells. For \(q \ne 0\) the guard is removable (\(0^q = 0\)), and for a probability family (\(p_i \ge 0\), \(\sum _i p_i = 1\)) one has \(Z_1 = 1\).

At a fixed cut strictly inside a gap of width \(\ge G\), the one-step band-mass increment is the current mass damped by \(e^{-G}\) plus a tempered source term; iterating produces the per-stratum leakage envelope.

For an ergodic, absolutely continuous (\(\mu \ll \operatorname {volume}\)), differentiable, uniformly expanding self-map of \(\operatorname {EuclideanSpace}\, \mathbb {R}\, (\operatorname {Fin}d)\) with everywhere-nonsingular derivative, log-integrable derivative data, a one-sided generating injectivity partition, and integrable \(\log \rho \) and \(\log \left\lvert \det DT \right\rvert \):

Honest disclosure: this is a correct implication whose hypothesis bundle has no model on the non-compact space \(\mathbb {R}^d\) — a globally uniformly expanding map of \(\mathbb {R}^d\) admits no ergodic absolutely continuous invariant probability measure (uniform expansion forces mass to escape to infinity; for \(T = c\cdot \operatorname {id}\) the nested preimages of a ball force an atom at the fixed point). The theorem is therefore vacuously true as stated on \(\mathbb {R}^d\), and is disclosed as such; the instantiated Pesin/Rokhlin equality lives on the compact circle (Theorem 12.18).

For a state \(\sigma \) and a channel \(\Lambda \), the Petz (transpose) recovery map is

realised through the continuous functional calculus (CFC.conjSqrt for the \(\sqrt{\cdot }\)-conjugations and the ring inverse for \((\Lambda \sigma )^{-1/2}\)).

Let \(\Lambda \) be any Kraus channel and \(\rho ,\sigma \) states with all four of \(\rho ,\sigma ,\Lambda \rho ,\Lambda \sigma \) positive definite. If data processing is saturated,

then the Petz recovery map reconstructs the input state,

No injectivity of the channel (or of the vectorised Petz map) is assumed; the result holds for information-losing channels such as the completely depolarising channel.

If the channel output \(\Lambda \sigma \) is positive definite, then the Petz map recovers \(\sigma \) from \(\Lambda \sigma \):

Let \(\Lambda \) and \(R\) be maps on states, each monotone under relative entropy (each satisfies the data-processing inequality against positive-definite second arguments). If \(R\) is a recovery section for the pair \(\rho ,\sigma \), i.e. \(R(\Lambda \rho )=\rho \) and \(R(\Lambda \sigma )=\sigma \) (with \(\sigma ,\Lambda \sigma \) positive definite), then the data-processing inequality is saturated:

If \(M\) is positive semidefinite then so is \(\operatorname{Tr}_B M\).

For a cell map \(c:\operatorname {Fin}d\to \operatorname {Fin}k\), the diagonal projection partition is \(\{ \operatorname {diag}\mathbf1_{c^{-1}(i)}\} _{i{\lt}k}\); it is an operational partition of unity encoding the measurable partition \(c^{-1}(\cdot )\) of \(\operatorname {Fin}d\).

Let \(W:\mathbb {C}^q\to \mathbb {C}^p\) be an isometry (\(W^{\dagger }W=1\)) and \(X\) self-adjoint with spectrum in \((0,\infty )\). Then

Given a dynamics \(\Phi \) and an operational partition \(X=(x_i)\), the time-ordered refinement of depth \(n\) along a word \(f\in (\operatorname {Fin}k)^{\operatorname {Fin}n}\) is the operator

defined by the telescoping recursion \(\mathrm{refine}(n+1,f)=x_{f_0}\cdot \Phi \! \bigl(\mathrm{refine}(n,\mathrm{tail}\, f)\bigr)\) with \(\mathrm{refine}(0,\cdot )=1\). It records the observable measured along the first \(n\) steps of the orbit under \(\Phi \).

Let \(p, q : \mathbb {N}\to \mathbb {R}\) be antitone on \([0,d)\). If \(\# \{ p \le a\} + \# \{ q \le b\} \le d\) whenever \(a + b {\lt} 0\), and \(\sum _{j{\lt}d} q\, j = -\sum _{j{\lt}d} p\, j\), then \(q\, j = -p\, (d-1-j)\) for all \(j {\lt} d\).

The Umegaki relative entropy of \(\rho \) with respect to \(\sigma \) is \(S(\rho \| \sigma ) = \operatorname{Tr}\rho (\log \rho - \log \sigma )\). It is defined in the concrete spectral/overlap form

where \((p_k,e_k)\) are the eigenvalues/eigenvectors of \(\rho \) and \((q_m,f_m)\) those of \(\sigma \). The definition is total: with the convention \(\log 0 = 0\) the \(\sigma \)-singular columns contribute \(0\).

Tensoring both arguments with a common faithful ancilla \(\alpha \) leaves the relative entropy unchanged: for faithful \(\sigma \) and faithful \(\alpha \), \(S(\rho \otimes \alpha \, \| \, \sigma \otimes \alpha ) = S(\rho \| \sigma )\).

For any unitary \(W\), \(\; S(W\rho W^{*}\, \| \, W\sigma W^{*}) = S(\rho \| \sigma )\), where \(W\rho W^{*}\) denotes the density matrix obtained by conjugating \(\rho \).

For states \(\rho ,\sigma \) on \(n\), a faithful ancilla \(\alpha \) on \(e\), a unitary \(U\) on \(n\times e\), and faithful \(\sigma \),

For faithful (positive definite) \(\sigma \), the spectral definition agrees with the textbook trace form

where \(\log \rho ,\log \sigma \) are the Hermitian continuous functional calculus of the real logarithm.

For faithful (positive definite) \(\sigma \), \(\; 0\le S(\rho \| \sigma )\).

\(S(\rho \| \rho ) = 0\) for every density matrix \(\rho \).

For matrices \(\rho ,\sigma \), the trace-form relative entropy is \(\mathrm{relEntropyMat}(\rho ,\sigma ) = \Re \, \operatorname{Tr}\bigl(\rho \, (\log \rho - \log \sigma )\bigr)\), the logarithms taken through the continuous functional calculus.

For a finite convex combination of faithful states — weights \(w_i\ge 0\) with \(\sum _i w_i = 1\) and positive-definite \(\rho _i,\sigma _i\) —,

For density matrices \(\rho ,\sigma \) with \(\sigma \) faithful (positive definite), \(\mathrm{relEntropyMat}(\rho ,\sigma ) = S(\rho \| \sigma )\), the Umegaki relative entropy.

For positive-definite \(\rho _1,\rho _2,\sigma _1,\sigma _2\) and \(c\in [0,1]\),

The proposition RelEntropyMonotoneUnderPartialTrace holds: the faithfulness hypothesis on \(\rho \) is unnecessary, so \(S(\operatorname{Tr}_E\rho \| \operatorname{Tr}_E\sigma )\le S(\rho \| \sigma )\) for every \(\rho \) and every faithful \(\sigma \).

For positive-definite states \(\rho ,\sigma \) on \(n_A\times n_E\),

RelEntropyMonotoneUnderPartialTrace is the proposition that for all finite index types \(n_A, n_E\) and all states \(\rho ,\sigma \) on \(n_A\times n_E\) with \(\sigma \) faithful (positive definite), tracing out the \(E\)-factor does not increase relative entropy,

The index types are quantified over Type (universe \(0\)): finite-dimensional quantum information lives in universe \(0\), and pinning the universe lets this Prop be used as a reusable hypothesis whose subsystems unify with any consumer’s.

The positive linear functional \(M\mapsto \langle \mathrm{vec}\, 1,\, M\, \mathrm{vec}\, 1\rangle \) recovers the trace-form relative entropy from the perspective:

The Rényi (generalized) dimension of \(p\) at scale \(\varepsilon \) is

At \(q = 1\) the general formula is the indeterminate \(0/0\), so the L’Hôpital value — the information dimension — is supplied directly as a separate branch. (By the Mathlib convention \(\log 0 = 0\), the \(q = 1\) numerator needs no positivity guard.)

Let \(p\) be a probability weight family (\(p_i \ge 0\), \(\sum _i p_i = 1\), at least one \(p_i {\gt} 0\)) and \(0 {\lt} \varepsilon {\lt} 1\). Then \(q \mapsto D_q\) is non-increasing (Antitone) on all of \(\mathbb {R}\) — including across the information-dimension branch point \(q = 1\).

For a measure-preserving flow \(\varphi \) with invariant probability measure \(\mu \) (Definition 8.1), a partition \(P\), and \(\varepsilon , q\), the Rényi dimension of the flow’s invariant measure is \(D_q(\varphi , P, \varepsilon ) = D_q(\mu , P, \varepsilon )\). The flow is an explicit (unused) argument whose type documents that \(\mu \) is flow-invariant; the multifractal API consumes any invariant probability measure.

For a measure-preserving flow \(\varphi \) of a probability measure \(\mu \), a partition \(P\), and \(0 {\lt} \varepsilon {\lt} 1\), the flow Rényi dimension \(q \mapsto D_q(\varphi , P, \varepsilon )\) is non-increasing in \(q\).

Let \(\alpha _0\) consist of exactly two symbols \(i \ne j\), let \(\nu \) charge both with positive but different masses (\(\nu \{ i\} \ne \nu \{ j\} \) after toReal), and let \(0 {\lt} \varepsilon {\lt} 1\). Then the Rényi dimension of the suspension flow’s invariant measure on the witness partition takes different values at two exponents:

The exhibited exponents are the explicit \(q_1 = 0\), \(q_2 = 1\) (renyiDimFlow_bernSuspension_zero_ne_one): concretely \(D_0 = \log 2 / (-\log \varepsilon )\) (both cells occupied) while \(D_1 = H(\nu )/(-\log \varepsilon )\) (the information dimension), and these differ precisely because the bias forces the strict inequality \(H(\nu ) {\lt} \log 2\). The witness is therefore non-vacuous: the \(q\)-dependence is driven by the genuine bias of \(\nu \), not satisfied trivially.

For a measure \(\mu \) on \(\alpha \), a finite measurable partition \(P\) of \(\mu \) indexed by \(\iota \), and \(\varepsilon , q \in \mathbb {R}\), the Rényi dimension of \(\mu \) at partition scale \(\varepsilon \) is the abstract \(D_q\) of the cell-mass family \(i \mapsto \mu (P_i)\) (real-valued via toReal). The companion definitions partitionFunctionMeasure and massExponentMeasure specialize \(Z_q\) and \(\tau \) in the same way.

For a probability measure \(\mu \), a finite measurable partition \(P\), and a scale \(0 {\lt} \varepsilon {\lt} 1\), the Rényi dimension \(q \mapsto D_q(\mu , P, \varepsilon )\) is non-increasing in \(q\).

For a probability measure \(\mu \), a partition \(P\), and any \(\varepsilon \),

where \(H(P) = \sum _i \operatorname {negMulLog}\bigl(\mu (P_i)\bigr) = -\sum _i \mu (P_i)\log \mu (P_i)\) is the Shannon entropy of the partition. For \(0 {\lt} \varepsilon {\lt} 1\) this is the familiar \(D_1 = H(P)/\log (1/\varepsilon )\).

For a measurable family \(V : X \to \mathrm{Submodule}\, \mathbb {R}\, (\mathbb {R}^d)\), set \(\mathrm{restGen}\, A\, V\, x = A(x)\cdot P_{V(x)}\) (with \(P_K\) the orthogonal projector onto \(K\)), \(\mathrm{sFloor}\, A\, T\, n\, x = \prod _{j{\lt}n}\left\lVert (A(T^{[j]}x))^{-1} \right\rVert ^{-1}\), and

Kingman applied to \(\mathrm{restLog}\) over \(T\) yields a constant \(\chi _V\); the orbit-reversed cocycle \(h_n(x) = \mathrm{restLog}_n(T^{-n}x)\) is subadditive over \(T^{-1}\) with the same integral means, hence converges a.e. to the same \(\chi _V\).

For the forward level \(V_i\), the restricted Kingman constant equals the \(i\)-th exponent: \(\chi _{V_i} = \mathrm{expEnum}\, \mathrm{lam0}\, d\, i\).

At each ambient flag level, the dimension captured by the subbundle is bounded by the ambient dimension: \(\dim \big(W(x) \cap V_i(x)\big) \le \dim V_i(x)\), so the restricted multiplicities are a sub-multiset of the ambient ones.

For ergodic \(T\), invertible \(A\), and an invariant subbundle \(W\), collapsing the constant-dimension levels of \(i \mapsto W \cap V_i\) yields a genuine strict Oseledets filtration inside \(W\): a strictly antitone \(\lambda '\) and a measurable family \(V'\) with, \(\mu \)-a.e., \(V'_0(x) = W(x)\), \(V'_{k'}(x) = 0\), strictly descending and \(A\)-equivariant, with exact growth rate \(\lambda '_i\) per stratum and all levels \(\le W(x)\).

For the doubling map and the binary partition,

the genuinely instantiated Pesin/Rokhlin equality on a real expanding system (in contrast to the vacuous-on-\(\mathbb {R}^d\) assembly Theorem 12.12). The integrand is the honest log-Jacobian: the generator \((2)\) is proved to be the Fréchet derivative of the doubling map’s linear lift \(x\mapsto 2x\) to the universal cover (), and the covering projection \(\mathbb {R}\to \mathbb {T}\) intertwines that lift with the doubling map () — so \((2)\) genuinely is \(DT\), not an arbitrary constant of the right determinant.

Let \(e\) be an ergodic measure-preserving automorphism of a standard Borel probability space with non-atomic \(\mu \). For every height \(N \ge 1\) and every \(\varepsilon {\gt} 0\) there is a measurable base \(B\) whose first \(N\) iterates \(B, eB, \dots , e^{N-1}B\) are pairwise disjoint and whose union covers all but \(\varepsilon \) of the space:

(Ergodicity plus non-atomicity supplies the aperiodicity the classical statement assumes.)

For a measure-preserving \(T\) and an integrable \(f : X \to \mathbb {R}\),

For a measure-preserving \(T\) and a measurable integrable \(g\), and every \(N : \mathbb {N}\),

Under the reflection \(\mathrm{mu0}\, j = -\mathrm{lam0}\, (d-1-j)\), the backward count of distinct exponents equals the forward one, and the index \(\mathrm{sidx}\, i = \mathrm{cast}\, (\mathrm{Fin.rev}\, i)\) satisfies \(\mathrm{expEnum}\, \mathrm{mu0}\, d\, (\mathrm{sidx}\, i) = -\mathrm{expEnum}\, \mathrm{lam0}\, d\, i\).

The singularity spectrum of \(p\) at scale \(\varepsilon \) is the Legendre transform of the mass exponent,

It is an infimum: since \(\tau \) is concave (Theorem 11.6), the supremum of \(q\alpha - \tau (q)\) would be \(+\infty \).

Write \(k=\mathrm{specCard}(A,T,x)\) for the number of distinct exponents (the cardinality of the spectrum). The exponent list \(\mathrm{specList}\colon \mathrm{Fin}\, k\to \mathbb {R}\) enumerates the spectrum in strictly descending order, \(\lambda _0{\gt}\lambda _1{\gt}\cdots {\gt}\lambda _{k-1}\), obtained from the order embedding of the finset composed with index reversal. It is strictly antitone, every \(\mathrm{specList}(i)\) lies in the spectrum, and every spectrum value is \(\mathrm{specList}(i)\) for a unique \(i\).

For \(\mu \)-a.e. \(x\), every index \(i\) and every vector \(v\) in the \(i\)-th stratum \(\mathrm{vflag}\, i.\mathrm{castSucc}\setminus \mathrm{vflag}\, i.\mathrm{succ}\) one has

For every \(n\), \(x\): \(\mathrm{sprod}\, A\, T\, d\, n\, x = \left\lvert \det A^{(n)}(x) \right\rvert \).

Let \(\mathrm{stepVal}\, \lambda ^0\, D\) be the step function \(e^{\lambda ^0_{D-1}} + \sum _{k=1}^{D-1}(e^{\lambda ^0_{k-1}}-e^{\lambda ^0_k})\, \mathbf1_{(c_k,\infty )}\) with thresholds \(c_k = e^{(\lambda ^0_k+\lambda ^0_{k-1})/2}\) strictly inside the \(k\)-th gap. If \(\lambda ^0\) is antitone on \([0,D)\) and \(j{\lt}D\), then \(\mathrm{stepVal}\, \lambda ^0\, D\, (e^{\lambda ^0_j}) = e^{\lambda ^0_j}\).

Given the partial-trace DPI (Definition 13.29), every Stinespring-dilated channel \(\Lambda \rho = \operatorname{Tr}_E\bigl(U(\rho \otimes \alpha )U^{*}\bigr)\) — adjoin a faithful ancilla \(\alpha \), conjugate by a unitary dilation \(U\), then trace out the ancilla — is relative-entropy monotone on faithful states: \(S(\Lambda \rho \| \Lambda \sigma )\le S(\rho \| \sigma )\).

For an ultrametric growth function \(g\) and threshold \(t\in \mathbb {R}\), the sublevel set

is a submodule of \(E\): it contains \(0\); closure under addition is the non-Archimedean inequality together with \(\max (g v,g w)\le t\); closure under scaling is scaling-invariance. These submodules are monotone in \(t\) (sublevel_mono).

Any exponent sequence \(\mathrm{lam0}\) realizing the a.e. singular-value limits satisfies \(\sum _{j{\lt}d}\mathrm{lam0}\, j = \int _X \log \left\lvert \det A(x) \right\rvert \, d\mu \).

For a backward exponent sequence \(\mathrm{mu0}\), \(\sum _{j{\lt}d}\mathrm{mu0}\, j = -\sum _{j{\lt}d}\mathrm{lam0}\, j\).

Let \(g\) be an ultrametric growth function, \(s\) a nonempty finite index set, and \(v\colon s\to E\) a family of nonzero vectors with \(g\circ v\) injective on \(s\). Then \(\sum _{i\in s} v_i \neq 0\) and \(g\bigl(\sum _{i\in s} v_i\bigr) = \sup _{i\in s} g(v_i)\).

The refinement of an operational partition of unity is again an operational partition of unity: for every \(n\),

The sum of all Lyapunov exponents equals the integral of \(\log \left\lvert \det \right\rvert \) of the generator:

Writing \(k_+ = \# \{ i : 0 {\lt} \mathrm{exponents}_i\} \), the positive-exponent sum equals the partial sum \(\Gamma _{k_+} = \sum _{i{\lt}k_+}\mathrm{exponents}_i\).

For an ergodic, log-integrable, differentiable uniformly expanding self-map \(T\), the sum of the strictly positive Lyapunov exponents — the Pesin / Margulis–Ruelle right-hand side — equals the integrated volume distortion — the Rokhlin right-hand side:

This is the honest foliation-free instance of the identity between the two right-hand sides; it is not a claim of the full Pesin entropy formula (no entropy appears in the statement).

For a uniformly expanding map the positive-part exponent sum is the full exponent sum: \(\sum \lambda ^{+} = \sum _i\lambda _i\) (with multiplicity).

The sum \(\mathrm{sumPosExp}\) of the strictly positive exponents is nonnegative, vanishes iff all exponents are \(\le 0\), and is strictly positive iff some exponent is positive (and dually \(\mathrm{sumNegExp} \le 0\) with the mirror characterizations).

If \(T\) is measure-preserving and \(g\in L^1(\mu )\), then for \(\mu \)-a.e. \(x\), \(\tfrac 1n\, g(T^n x)\to 0\).

If \(\sum _i \mathrm{exponents}_i {\lt} 0\) then \(\mu \)-a.e. \(\left\lvert \det A^{(n)}(x) \right\rvert \to 0\).

For a finite measure, a measure-preserving \(T\) and an integrable \(g\), the Birkhoff averages converge \(\mu \)-a.e. to the conditional expectation of \(g\) onto the invariant \(\sigma \)-algebra:

For an ergodic \(T\) on a probability space and integrable \(g\), the Birkhoff averages converge \(\mu \)-a.e. to the space average \(\int g\, d\mu \).

If \(P^{c}_n(x)\to P\) with \(Pv\neq 0\), then \(\tfrac 1n\log \left\lVert P^{c}_n(x)\, v \right\rVert \to 0\).

For a finite measure, a measure-preserving \(T\), an integrable subadditive cocycle \(g\) whose normalized integrals are bounded below, there is a \(T\)-invariant integrable \(G\) with

For an ergodic \(T\) on a probability space, an integrable subadditive cocycle with normalized integrals bounded below, there is a constant \(c\) with \(n^{-1}\, g\, n\, x \to c\) for \(\mu \)-a.e. \(x\).

Under the hypotheses of the ergodic Kingman theorem, there is a constant \(c\) with

The averaged iterated-join entropies converge: \(\frac1n H\bigl(\bigvee _{k{\lt}n}T^{-k}\alpha \bigr)\to h(T,\alpha )\) as \(n\to \infty \).

Fix a flow \( \varphi \), a flow cocycle \( A \) with uniform forward/inverse one-step controls \( g, g' \) on \( [0,1] \), a point \( x \), and a nonzero vector \( v \). Suppose the integer fluctuation error vanishes and the integer-time average converges, \( n^{-1}\log \left\lVert A(n,x)v \right\rVert \to L \). Then the continuous-time average converges to the same limit:

On a probability space, with \(A\) invertible and \(0 {\lt} k\), \(\mu \)-a.e. the operator-norm growth rate of the cocycle converges to the top exponent:

For \(k \le d\) and \(\mu \)-a.e. \(x\), the operator-norm growth of the compound cocycle converges to \(\Gamma _k\): \(\tfrac 1n\log \left\lVert C_k(A^{(n)}(x)) \right\rVert \to \Gamma _k\), the \(k\)-dimensional volume growth rate.

For each sorted index \(i\) and \(\mu \)-a.e. \(x\), the singular-value exponents of the inverse-matrix cocycle are the negated, reversed exponents of \(A\):

For \(\mu \)-a.e. \(x\), \(q_n(x)\to \Lambda (x)\) in the matrix metric, and \(\Lambda \) is measurable.

For subspaces \(K, L\) of \(\mathbb {R}^d\), with \(P_K, P_L\) the orthogonal projectors,

For \(\mu \)-a.e. \(x\) the approximants \(q_n(x)\) converge in the matrix metric to a single matrix \(\Lambda (x)\).

For ergodic \(T\) and a possibly-singular measurable generator with only \(\log ^+\left\lVert A \right\rVert \in L^1\) (no invertibility, no inverse integrability), the normalized positive-part log-norms \(\tfrac 1n\log ^+\left\lVert A^{(n)}(x) \right\rVert \) converge \(\mu \)-a.e. to a constant \(\lambda _1^+\).

For a flow cocycle \( A \) over \( \varphi \), every \( n \in \mathbb {N}\) and every \( x \),

i.e. at integer times the continuous-time cocycle equals the discrete iterated cocycle generated by its time-one map \( A(1,\cdot ) \) over the time-one dynamics \( \varphi (1) \).

\(\mu \)-a.e. the largest exponent of the inverse cocycle is \(-\, \mathrm{exponents}_{d-1}\), the negative of the smallest forward exponent.

\(\mathrm{TopGapMassEnvelope}\, A\, T\, \lambda ^0\, x\) asserts the uniform geometric leakage of fast-band mass across each genuine gap: for every cut tolerance \(\delta \) there is a constant \(C\) controlling, eventually and uniformly, the band mass that crosses the top gap of each stratum.

For \(\mu \)-a.e. \(x\), the top-gap fast-band-mass envelope \(\mathrm{TopGapMassEnvelope}\, A\, T\, \lambda ^0\, x\) holds.

\(\operatorname{Tr}(\operatorname{Tr}_B M) = \operatorname{Tr}M\).

On a probability space, any two Oseledets filtration data \((k, \lambda , V)\) and \((k_2, \lambda _2, V_2)\) for the same cocycle agree: \(k = k_2\), the exponents coincide under the index cast, and \(\mu \)-a.e. the flags agree level by level.

A finite quantum dynamics is a map \(\Phi :\operatorname {Matrix}_d(\mathbb {C})\to \operatorname {Matrix}_d(\mathbb {C})\) that is additive, multiplicative, unital (\(\Phi (1)=1\)) and \(*\)-preserving (\(\Phi (x^{\dagger })=\Phi (x)^{\dagger }\)). Additivity is carried as part of the datum: it is automatic for a \(*\)-homomorphism of matrix algebras, and it is exactly what lets \(\Phi \) commute with the finite sums appearing in the telescoping identity below.

For ergodic \(T\), the in-measure SMB upper bound holds: for every \(\varepsilon {\gt} 0\),

This McMillan-type form is exactly what the name-count covering bound below consumes.

The limsup flag at \(x\) is the family \(\mathrm{vflag}(A,T,x)\colon \mathrm{Fin}\, (k+1)\to \mathrm{Submodule}\) with

With the descending enumeration, level \(j\) is the sublevel set at \(\lambda _j\), so the flag decreases from the whole space down to \(\bot \).

Under the standing hypotheses, for a.e. \(x\) the spectrum is invariant, \(\mathrm{lyapunovSpectrum}(A,T,x)=\mathrm{lyapunovSpectrum}(A,T,Tx)\) (lyapunovSpectrum_equivariant_ae), and the action of \(A x\) maps each flag level (each sublevel subspace) at \(x\) onto the corresponding level at \(Tx\):

On the good set, \(\mathrm{vflag}(A,T,x)(i{+}1) \subsetneq \mathrm{vflag}(A,T,x)(i)\) for each interior index \(i\).

On the good set, \(\mathrm{vflag}(A,T,x)(0)=\top \); and unconditionally \(\mathrm{vflag}(A,T,x)(\mathrm{last})=\bot \) (vflag_last).

The von Neumann entropy of a density matrix \(\rho \) with eigenvalues \(\lambda _i\) is

using Mathlib’s \(\operatorname {negMulLog}(x) = -x\log x\), so the convention \(0\log 0 = 0\) is built in.

On the abelian corner the correlation matrix is diagonal, carrying the masses of the classical \(n\)-fold join on its diagonal; hence its von Neumann entropy equals the classical iterated-join Shannon entropy of the system \((\operatorname {Fin}d,\mu ,\sigma )\):

\(S(\rho )\ge 0\) for every density matrix \(\rho \).

For a bipartite density matrix \(\rho \) on \(n_A\otimes n_B\) with reduced density matrices \(\rho _A = \operatorname{Tr}_B\rho \) and \(\rho _B = \operatorname{Tr}_A\rho \), the von Neumann entropy is subadditive:

Under the spectral upper bound and the reverse inclusion, for \(\mu \)-a.e. \(x\) and every \(t\),

On the ultrametric-growth good set, every vector \(v\) of the \(\Lambda \)-slow band \(\mathrm{vslow}(e^t)\) with \(\limsup _n\tfrac 1n\log \left\lVert A^{(n)}v \right\rVert \le t\) lies in the growth sublevel \(\{ v:\overline\lambda (x,v)\le t\} \).