Documentation

Oseledets.Multifractal.RefiningLimit

Coarse-grained multifractal analysis: the refining-partition limit (degenerate case) #

This file discharges the degenerate (uniform / monofractal) case of the refining-partition limit of issue #16, item 6: for the uniform (Haar / Lebesgue) measure the multifractal Rényi spectrum degenerates to a single point, recovered exactly in the refining limit ε → 0.

Concretely, partition d-dimensional space at scale ε ∈ (0, 1) into a uniform grid of N = ε ^ (-d) cells of equal weight p i = N⁻¹ (the dyadic-grid scaling of d-dimensional Lebesgue measure). Then Degeneracy.renyiDim_equalMeasure gives, for every q, D_q = log N / (-log ε), and feeding the count N = ε ^ (-d) in collapses this to D_q = d, exactly, for every ε ∈ (0, 1) and every q (Real.log_rpow turns log (ε ^ (-d)) into (-d) · log ε, which cancels against -log ε ≠ 0). The per-resolution value is therefore the constant d, so the refining limit ε → 0 is the trivial limit of a constant: Tendsto (fun ε => renyiDim (p ε) ε q) (𝓝[Set.Ioo 0 1] 0) (𝓝 d).

Main results #

Scope (what is, and is NOT, formalized here) #

This is only the degenerate uniform / monofractal case, where the per-resolution dimension is constant in ε and the limit is trivial. The pointwise local dimension itself is defined, and its absolutely-continuous case proved, in Oseledets.Multifractal.LocalDimension (item 5). What stays the genuine frontier is the general non-uniform refining limit (item 6 for a genuinely multifractal measure) and general exact-dimensionality — a.e.-constancy of the local dimension for a singular / SRB measure, and the Young / Ledrappier–Young identity. These need the absolute continuity of conditional measures on unstable manifolds (the Ledrappier–Young core), the same Mathlib-absent ingredient that blocks the library's Pesin–SRB work (issue #10), not any missing metric or ergodic theorem (the Lyapunov exponents, entropy, Margulis–Ruelle inequality, and a pointwise Birkhoff theorem are all already present). See the issue for the research-grade statement.

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

Per-resolution monofractal value. For a uniform partition into N = Fintype.card ι cells of equal weight p i = N⁻¹, with the count tuned to the d-dimensional dyadic-grid scaling N = ε ^ (-d) (so the cells model d-dimensional Lebesgue measure at scale ε), the Rényi (generalized) dimension is exactly d for every q and every ε ∈ (0, 1). Indeed renyiDim_equalMeasure gives D_q = log N / (-log ε), and log N = log (ε ^ (-d)) = (-d) log ε cancels the denominator -log ε ≠ 0.

source
theorem Oseledets.Multifractal.renyiDim_uniform_tendsto_dim {ι : ℝ → Type u_1} [(ε : ℝ) → Fintype (ι ε)] [∀ (ε : ℝ), Nonempty (ι ε)] {p : (ε : ℝ) → ι ε → ℝ} {d : ℝ} (huniform : ∀ (ε : ℝ) (i : ι ε), p ε i = (↑(Fintype.card (ι ε)))⁻¹) (hcard : ∀ ε ∈ Set.Ioo 0 1, ↑(Fintype.card (ι ε)) = ε ^ (-d)) (q : ℝ) :
Filter.Tendsto (fun (ε : ℝ) => renyiDim (p ε) ε q) (nhdsWithin 0 (Set.Ioo 0 1)) (nhds d)

Refining-partition limit (degenerate / monofractal case). Take a refining family of uniform partitions: at each scale ε ∈ (0, 1) an index type ι ε of Fintype.card (ι ε) = ε ^ (-d) cells, each carrying the equal weight (Fintype.card (ι ε))⁻¹ (the dyadic-grid model of d-dimensional Lebesgue measure). By renyiDim_uniform_eq_dim the per-resolution Rényi dimension equals the constant d for every such ε and every q, so the refining limit ε → 0 recovers the single spectral point d exactly: Tendsto (fun ε => renyiDim (p ε) ε q) (𝓝[Set.Ioo 0 1] 0) (𝓝 d). This is the degenerate case of issue #16, item 6.

source
theorem Oseledets.Multifractal.renyiDimMeasure_uniform_eq_dim {α : Type u_1} {ι : Type u_2} [MeasurableSpace α] [Fintype ι] [Nonempty ι] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : Entropy.MeasurePartition μ ι) {ε d : ℝ} (huniform : ∀ (i : ι), (μ (P.cells i)).toReal = (↑(Fintype.card ι))⁻¹) (hε0 : 0 < ε) (hε1 : ε < 1) (hcard : ↑(Fintype.card ι) = ε ^ (-d)) (q : ℝ) :
renyiDimMeasure μ P ε q = d

Measure-level mirror of the monofractal value. For a probability measure μ and a uniform partition P with each cell of equal measure (Fintype.card ι)⁻¹ and the count tuned to the d-dimensional scaling Fintype.card ι = ε ^ (-d), the Rényi dimension of μ is exactly d for every q and every ε ∈ (0, 1). This is renyiDimMeasure_equalMeasure fed the count N = ε ^ (-d).