Derivative-free. The midpoint inequality \(Z_{aq_1 + bq_2} \le Z_{q_1}^{\, a}\, Z_{q_2}^{\, b}\) (for \(a, b {\gt} 0\), \(a + b = 1\)) is exactly the two-term Hölder inequality with conjugate exponents \(1/a, 1/b\) applied on the support \(\{ i : p_i {\gt} 0\} \) (the lemma partitionFunction_holder). The positivity hypothesis gives \(Z_q {\gt} 0\) at every \(q\), so taking logarithms and using monotonicity of \(\log \) turns the multiplicative bound into the convexity inequality for \(\log \circ Z\).

Since \(0 {\lt} \varepsilon {\lt} 1\), the denominator \(\log \varepsilon \) is negative; multiplying the convex \(\log Z_q\) by the nonpositive constant \(1/\log \varepsilon \) flips convexity to concavity. Formally, \(c \cdot \log Z\) with \(c = -(\log \varepsilon )^{-1} \ge 0\) is convex, and \(\tau \) is its negation.

The classical secant-slope argument. Write \(h(q) = \log Z_q\); it is convex and \(h(1) = 0\) for a probability family, so the secant slope \(g(q) = h(q)/(q-1)\) anchored at \(1\) is non-decreasing on \(\{ q \ne 1\} \) (ConvexOn.secant_mono). For \(q \ne 1\), \(D_q = g(q)/\log \varepsilon \), and \(\log \varepsilon {\lt} 0\) flips monotone to antitone. The subtle point is gluing in \(q = 1\): the information-dimension numerator \(\sum _i p_i \log p_i\) is exactly the derivative \(h'(1)\) (each occupied summand \(q \mapsto p_i^{\, q}\) is a real exponential), and the convex supporting-line inequalities give \(g(q) \le h'(1) \le g(q')\) for \(q {\lt} 1 {\lt} q'\); dividing by \(\log \varepsilon {\lt} 0\) inserts \(D_1\) into the antitone family.

Apply Theorem 12.7 to the cell-mass family: nonnegativity is \(\texttt{ENNReal.toReal} \ge 0\), the normalization is the partition identity \(\sum _i \mu (P_i) = 1\), and at least one cell has positive mass because the total mass is \(1\).

Unfold the \(q = 1\) branch of \(D_q\): its numerator \(\sum _i \mu (P_i)\log \mu (P_i)\) is term-by-term the negation of the \(\operatorname {negMulLog}\) sum defining \(H(P)\).

renyiDimFlow unfolds to renyiDimMeasure, so this is Theorem 12.9 verbatim.

Pure measure differentiation, no dynamics. Besicovitch differentiation gives \(\mu (\bar B(x,r))/\nu (\bar B(x,r)) \to (d\mu /d\nu )(x)\) as \(r \to 0^+\), \(\mu \)-a.e., with the Radon–Nikodym density finite and positive \(\mu \)-a.e. (from \(\mu \ll \nu \)). The Haar ball-volume scaling \(\nu (\bar B(x,r)) = r^{d}\, \nu (\bar B(0,1))\) with \(d = \operatorname {finrank}_{\mathbb {R}} E\) factorizes the ball mass as \(\text{ratio}(r) \cdot r^d \cdot C\) with \(\text{ratio}(r) \to L {\gt} 0\) and \(C {\gt} 0\); a logarithm-limit lemma then shows the quotient is \((\log \text{ratio}(r) + \log C)/\log r + d \to d\), since \(\log r \to -\infty \) kills the bounded numerator.

Where the genuine limit of Theorem 12.14 exists, the \(\limsup \) defining \(\bar d_\mu \) returns that limit.

Two mass-distribution arguments over a bare metric space. Lower bound (Frostman): for each \(a {\lt} \alpha \), the pointwise limit yields on a positive-measure measurable piece of \(s\) a uniform upper ball bound \(\mu (\bar B(x,r)) \le r^a\) at small radii; then \(\mu \! \restriction _A \le \mu _H^a\) (any small-diameter set meeting \(A\) sits in a controlled ball), so \(\mu _H^a(s) {\gt} 0\) and \(a \le \dim _H s\); let \(a \uparrow \alpha \). Upper bound (Billingsley): for \(a {\gt} \alpha \), the limit produces at arbitrarily small radii the lower bound \(\mu (\bar B(x,r)) \ge r^a\) (the positive limit forces positive ball masses); a Vitali enlargement of a disjoint subfamily of such balls covers \(s\) with \(\sum (\operatorname {diam})^a \le (2\tau )^a \mu (E) {\lt} \infty \), so \(\mu _H^a(s) {\lt} \infty \) and \(\dim _H s \le a\); let \(a \downarrow \alpha \). The pointwise (not merely a.e.) hypothesis is essential for the upper bound, since a \(\mu \)-null subset can carry extra Hausdorff dimension.

The upper bound is monotonicity: \(\dim _H s \le \dim _H E = \operatorname {finrank}_{\mathbb {R}} E\). The lower bound is the Frostman direction of the bridge, fed by the a.e. local-dimension limit of Theorem 12.14.

Atoms are cylinders are dyadic closed balls, so the unconditional pointwise Shannon–McMillan–Breiman theorem gives the dyadic mass quotient \(\log \mu (\bar B(x,(1/2)^n)) / \log ((1/2)^n) \to h/\log 2\) \(\mu \)-a.e., with \(h\) the coordinate-partition entropy (ksEntropyPartition, Definition 10.11). An ultrametric sandwich (balls are constant on each dyadic gap, and \(\log r \to -\infty \)) upgrades the dyadic limit to the continuum limit \(r \to 0^+\). Feeding the conull carrier of that pointwise limit into Theorem 12.16 with \(\alpha = h/\log 2 {\gt} 0\) gives \(\dim _H s = h / \log 2\); finally the coordinate partition is a generator, so the Kolmogorov–Sinai generator theorem identifies \(h\) with the system entropy \(h_\mu (\sigma )\).

Ergodicity of the shift for \(\operatorname {bern}\nu \) is Kolmogorov’s 0–1 law applied to the tail-measurable invariant sets (ergodic_shiftMap_bern). The coordinate-partition entropy equals \(H(\nu )\), which is strictly positive because the two charged symbols force \(\nu \{ i\} \in (0,1)\) (Hnu_pos). Theorem 12.18 then applies, and the system entropy identity \(h_{\operatorname {bern}\nu }(\sigma ) = H(\nu )\) (ksEntropy_bern_eq, via the generator theorem) rewrites the dimension.

Lift \(A\) through the quotient map \(\pi (x,s) = [x,s]\). Invariance under all vertical translations shows membership of \([x,s]\) depends only on the base point, so the lift is a cylinder \(B \times \mathbb {R}\) with \(B = \{ x : [x,0] \in A\} \). The identification generator \((x,s) \mapsto (Tx, s-1)\) fixes \(\pi \), so \(B\) is shift-invariant; it is measurable, and the constant-roof box computation gives \(\hat\mu (A) = \operatorname {bernZ}\nu (B)\). Base ergodicity’s zero–one law finishes.

The fundamental-domain equivalence onto \(\alpha _0^{\mathbb {Z}} \times [0,1)\) conjugates \(\zeta _1\) to the frozen product \(T \times \operatorname {id}\) and carries \(\hat\mu \) to \(\operatorname {bernZ}\nu \otimes \text{Leb}\! \restriction _{[0,1)}\). Conjugacy invariance of \(h\), the frozen-factor product identity \(h(T \times \operatorname {id}) = h(T)\), and the two-sided Bernoulli system-entropy identity \(h(T) = H(\nu )\) (generator theorem on the two-sided coordinate partition) chain together.

By the mass identity, the cells indexed by \(i\) and \(j\) carry masses \(\nu \{ i\} \) and \(\nu \{ j\} \), which differ by hypothesis (the toReal coercion is injective on finite masses).

A transfer argument. The flow witness’s cell masses agree, up to the \(\alpha _0 \simeq \operatorname {Fin}(\operatorname {card}\alpha _0)\) reindex, with those of the one-sided base coordinate partition under \(\operatorname {bern}\nu \); since the Rényi dimension depends only on the cell-mass family, the flow spectrum equals the base spectrum at every \(q\) (renyiDimFlow_bernSuspension_eq_base). On the base, \(D_0\) is the box-counting value \(\log 2 / (-\log \varepsilon )\) (two occupied cells) and \(D_1\) is the information dimension \(H(\nu )/(-\log \varepsilon )\) (Theorem 12.10); the strict two-point entropy bound \(H(\nu ) {\lt} \log 2\) for a biased law separates them.

The two-element bounds \(x^q + y^q \le (x+y)^q\) (for \(q \ge 1\), Real.add_rpow_le_rpow_add) and \((x+y)^q \le x^q + y^q\) (for \(0 \le q \le 1\), Real.rpow_add_le_add_rpow) are promoted to arbitrary fibres by \(\mathrm{Finset.induction}\), then summed over the fibre partition of \(\iota \) indexed by \(\kappa \).

For \(q \ge 1\) the partition function grows (Lemma 12.28) and the prefactor \((1-q)^{-1} {\lt} 0\) flips the growth to a drop in \(H_q\); for \(0 \le q {\lt} 1\) the partition function shrinks and the positive prefactor \((1-q)^{-1} {\gt} 0\) again gives a drop. The strict form runs the same sign bookkeeping on the strict two-point inequality (strict monotonicity of \(\mathrm{rpow}\) in the base, both atoms of positive mass).

The mechanism is entirely per length \(n\), so no stationarity or shift-invariance of \(\mu \) is used: measure additivity over the word fibre identifies the pushed masses with \(\mathrm{mergedWeights}\, (\mathrm{wordMap}\, \varphi \, n)\) of the cylinder masses, and Theorem 12.29 applies to that merge.

Divide the per-length DPI (Theorem 12.32) by \(n\) and pass to \(\limsup \)/\(\liminf \); the uniform bounds \(0 \le H_q^{(n)}(\mu )/n \le C_q\) make the normalized sequences order-bounded, so the limit operations preserve the inequality. No existence of the rate limit is required.

Everything factorizes over coordinates. The length-\(n\) cylinder mass of a word is the product \(\prod _k (\nu \{ w_k\} )\) (cylinderMass_bern, by the product-measure evaluation), so the length-\(n\) partition function factors as \(Z_q^{(n)} = (Z_q)^n\) (partitionFunction_cylinderMass_bern, a sum-over-words / product-over-coordinates swap). Hence \(H_q^{(n)}(\mathrm{bern}\, \nu ) = n\, H_q(\nu )\) (renyiEntropySeq_bern, via \(\log (Z_q^n) = n\log Z_q\)), the normalized sequence is eventually constant \(H_q(\nu )\), and both rates return that value.

map_blockCode_bern is the coordinatewise pushforward of a product measure, checked on measurable boxes; its mapped marginals are the merged weights. The strict two-atom form of the static DPI then separates the rates. For the uniform \(\operatorname {Fin}3 \to \operatorname {Fin}2\) witness the two rates are concrete logarithms and \(q = 2\) is a compile-time inequality.