Coarse-grained multifractal analysis: core definitions

This file lays the abstract, measure-free foundation for the coarse-grained multifractal analysis of a finite weight family p : ι → ℝ (think p i = μ(cell i) for the cells of a partition at scale ε). All quantities are defined on a bare family p; the hypotheses one needs for the theory (0 ≤ p i, ∑ i, p i = 1, 0 < ε < 1) are carried on the lemmas, never baked into the definitions, so the algebra stays clean and the same definitions specialize to any measure.

The exponent ^ throughout is Real.rpow (real-base, real-exponent power), which is the right notion for the continuous parameter q : ℝ.

Main definitions

• Oseledets.Multifractal.partitionFunction: the generalized partition function Z_q = ∑_{i : p i > 0} (p i) ^ q. The guard 0 < p i is load-bearing at q = 0: it forces empty cells to contribute 0 (so Z_0 counts occupied cells) instead of Real.rpow 0 0 = 1.
• Oseledets.Multifractal.massExponent: the mass exponent τ(q) = log Z_q / log ε.
• Oseledets.Multifractal.renyiDim: the Rényi / generalized dimension D_q = τ(q) / (q - 1), with the q = 1 information-dimension branch (∑ i, p i log p i) / log ε supplied directly (the L'Hôpital limit), since the general formula is 0 / 0 there.
• Oseledets.Multifractal.singularitySpectrum: the singularity spectrum f(α) = ⨅ q, q α - τ(q), the Legendre transform of τ. This is an infimum: because τ is concave, the supremum would be +∞.

Main results

• Oseledets.Multifractal.partitionFunction_nonneg: Z_q ≥ 0 when 0 ≤ p i.
• Oseledets.Multifractal.partitionFunction_eq_sum_rpow: for q ≠ 0 the guard is removable, Z_q = ∑ i, (p i) ^ q, since Real.zero_rpow makes empty cells vanish anyway.
• Oseledets.Multifractal.partitionFunction_one_eq_one: Z_1 = 1 for a probability weight family.
• Oseledets.Multifractal.massExponent_one_eq_zero: τ(1) = 0 for a probability weight family.

noncomputable def Oseledets.Multifractal.partitionFunction {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (q : ℝ) : ℝ

The generalized partition function Z_q = ∑_{i : p i > 0} (p i) ^ q of a finite weight family p : ι → ℝ, with exponent ^ interpreted as Real.rpow. The guard 0 < p i is load-bearing at q = 0: it ensures empty cells (p i = 0) contribute 0 rather than Real.rpow 0 0 = 1, so that Z_0 counts the number of occupied cells.

Equations

• Oseledets.Multifractal.partitionFunction p q = ∑ i : ι, if 0 < p i then p i ^ q else 0

noncomputable def Oseledets.Multifractal.massExponent {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (ε q : ℝ) : ℝ

The mass exponent τ(q) = log Z_q / log ε of a finite weight family p at scale ε. This is defined for every q with no case split.

Equations

• Oseledets.Multifractal.massExponent p ε q = Real.log (Oseledets.Multifractal.partitionFunction p q) / Real.log ε

noncomputable def Oseledets.Multifractal.renyiDim {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (ε q : ℝ) : ℝ

The Rényi (generalized) dimension D_q of a finite weight family p at scale ε. For q ≠ 1 it is τ(q) / (q - 1). At q = 1 the general formula is the indeterminate 0 / 0, so the L'Hôpital value — the information dimension (∑ i, p i log p i) / log ε — is supplied directly. (By the Mathlib convention Real.log 0 = 0, the q = 1 numerator needs no guard: empty cells contribute 0 automatically.)

Equations

• Oseledets.Multifractal.renyiDim p ε q = if q = 1 then (∑ i : ι, p i * Real.log (p i)) / Real.log ε else Oseledets.Multifractal.massExponent p ε q / (q - 1)

noncomputable def Oseledets.Multifractal.singularitySpectrum {ι : Type u_1} [Fintype ι] (p : ι → ℝ) (ε α : ℝ) : ℝ

The singularity spectrum f(α) = ⨅ q, q α - τ(q) of a finite weight family p at scale ε, the Legendre transform of the mass exponent τ. This is an infimum: since τ is concave, the supremum of q α - τ(q) would be +∞.

Equations

• Oseledets.Multifractal.singularitySpectrum p ε α = ⨅ (q : ℝ), q * α - Oseledets.Multifractal.massExponent p ε q

theorem Oseledets.Multifractal.partitionFunction_nonneg {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (q : ℝ) : 0 ≤ partitionFunction p q

The generalized partition function of a nonnegative weight family is nonnegative.

theorem Oseledets.Multifractal.partitionFunction_eq_sum_rpow {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) {q : ℝ} (hq : q ≠ 0) : partitionFunction p q = ∑ i : ι, p i ^ q

For q ≠ 0 the positivity guard in the partition function is removable: empty cells (p i = 0) contribute Real.rpow 0 q = 0 anyway, so Z_q = ∑ i, (p i) ^ q.

theorem Oseledets.Multifractal.partitionFunction_one_eq_one {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hsum : ∑ i : ι, p i = 1) : partitionFunction p 1 = 1

For a probability weight family (0 ≤ p i and ∑ i, p i = 1), the partition function at q = 1 is 1. Occupied cells contribute (p i) ^ 1 = p i, empty cells contribute 0 either way.

theorem Oseledets.Multifractal.massExponent_one_eq_zero {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hsum : ∑ i : ι, p i = 1) (ε : ℝ) : massExponent p ε 1 = 0

For a probability weight family, the mass exponent at q = 1 vanishes, since Z_1 = 1 and log 1 = 0.

theorem Oseledets.Multifractal.partitionFunction_pos {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hpos : ∃ (i : ι), 0 < p i) (q : ℝ) : 0 < partitionFunction p q

If at least one weight is strictly positive, the partition function is strictly positive: the contributing cell i adds (p i) ^ q > 0 to a sum of nonnegative terms (each guarded summand is either a positive rpow of a positive base, or 0).