Coarse-grained multifractal analysis: equal-measure degeneracy

This file records the equal-measure (uniform) degeneracy of the multifractal formalism: when every cell carries the same weight p i = N⁻¹ (with N = Fintype.card ι), the generalized dimension D_q collapses to a single, q-independent value, namely log N / (-log ε). This is the standard sanity check (issue #16, item 4c): a uniform measure is monofractal, so its whole Rényi spectrum is a single point, equal to the box-counting dimension log N / log (1/ε).

Main results

• Oseledets.Multifractal.partitionFunction_equalMeasure: for the uniform family, Z_q = N ^ (1 - q).
• Oseledets.Multifractal.renyiDim_equalMeasure: for the uniform family and 0 < ε < 1, D_q = log N / (-log ε) for every q — both the q = 1 information-dimension branch and the general q ≠ 1 branch are shown to agree on this common value.

theorem Oseledets.Multifractal.partitionFunction_equalMeasure {ι : Type u_1} [Fintype ι] [Nonempty ι] {p : ι → ℝ} (hp : ∀ (i : ι), p i = (↑(Fintype.card ι))⁻¹) (q : ℝ) : partitionFunction p q = ↑(Fintype.card ι) ^ (1 - q)

For the uniform (equal-measure) family p i = (Fintype.card ι)⁻¹, the generalized partition function is Z_q = N ^ (1 - q) with N = Fintype.card ι. Each of the N cells is occupied (N⁻¹ > 0), contributing (N⁻¹) ^ q, so Z_q = N • (N⁻¹) ^ q = N ^ (1 - q).

theorem Oseledets.Multifractal.renyiDim_equalMeasure {ι : Type u_1} [Fintype ι] [Nonempty ι] {p : ι → ℝ} (hp : ∀ (i : ι), p i = (↑(Fintype.card ι))⁻¹) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) (q : ℝ) : renyiDim p ε q = Real.log ↑(Fintype.card ι) / -Real.log ε

For the uniform (equal-measure) family p i = (Fintype.card ι)⁻¹ and 0 < ε < 1, the Rényi (generalized) dimension is q-independent: D_q = log N / (-log ε) for every q. This is the monofractal degeneracy of a uniform measure: the entire Rényi spectrum is the single point log N / log (1/ε). Both branches of renyiDim (the q = 1 information dimension and the general q ≠ 1 formula) are shown to evaluate to this common value.