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 11.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 11.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 11.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 11.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 9.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 11.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 11.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 11.10); the strict two-point entropy bound \(H(\nu ) {\lt} \log 2\) for a biased law separates them.