Documentation

Oseledets.Multifractal.Monotone

Coarse-grained multifractal analysis: monotonicity of the Rényi dimension #

This file proves that the Rényi (generalized) dimension D_q of a finite probability weight family p : ι → ℝ at a scale 0 < ε < 1 is non-increasing in q (issue item 4b).

The argument is the classical secant-slope argument. Let h q = log Z_q be the logarithm of the partition function; by logPartitionFunction_convexOn (file LogConvex.lean) it is convex on ℝ, and h 1 = 0 for a probability family. The secant slope anchored at 1, g q = (h q - h 1) / (q - 1) = h q / (q - 1), is therefore non-decreasing in q away from the anchor (ConvexOn.secant_mono). For q ≠ 1 the Rényi dimension is D_q = g q / log ε, and since log ε < 0 the division flips the monotone g to the antitone D.

The genuinely subtle point is the information-dimension singularity q = 1, where D_1 is defined directly as (∑ i, p i log p i) / log ε (the secant slope g itself takes a junk 0/0 = 0 value at the anchor, so one cannot route through it). The numerator ∑ i, p i log p i is exactly the derivative h'(1) of the convex function h, and the convex supporting-line inequalities ConvexOn.le_slope_of_hasDerivAt / ConvexOn.slope_le_of_hasDerivAt give g q ≤ h'(1) ≤ g q' for q < 1 < q'. Dividing by log ε < 0 glues D_1 into the monotone family, so antitonicity holds across q = 1 as well — i.e. the full Antitone over all of ℝ.

Main results #

source
theorem Oseledets.Multifractal.logPartitionFunction_secantSlope_monotoneOn {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hpos : ∃ (i : ι), 0 < p i) (hsum : ∑ i : ι, p i = 1) :
MonotoneOn (fun (q : ℝ) => Real.log (partitionFunction p q) / (q - 1)) {q : ℝ | q ≠ 1}

The secant slope of q ↦ log Z_q, anchored at the probability point q = 1 (where log Z_1 = 0), is monotone (non-decreasing) on {q | q ≠ 1}. This is the reusable core of the monotonicity of the Rényi dimension: for q ≠ 1, D_q = (this slope) / log ε, and log ε < 0 flips it to antitone.

Concretely q ↦ log Z_q / (q - 1) is non-decreasing as q ranges over {q | q ≠ 1} (away from the anchor, where the expression is the junk 0 / 0).

source
theorem Oseledets.Multifractal.hasDerivAt_partitionFunction {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (q : ℝ) :
HasDerivAt (fun (q : ℝ) => partitionFunction p q) (∑ i : ι, if 0 < p i then p i ^ q * Real.log (p i) else 0) q

The derivative of the partition function q ↦ Z_q = ∑_{p i > 0} (p i) ^ q at any point q is ∑_{p i > 0} (p i) ^ q * log (p i): each surviving summand q ↦ (p i) ^ q (for p i > 0) is a real exponential whose derivative is (p i) ^ q * log (p i), and the empty cells are constants.

source
theorem Oseledets.Multifractal.hasDerivAt_logPartitionFunction_one {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hsum : ∑ i : ι, p i = 1) :
HasDerivAt (fun (q : ℝ) => Real.log (partitionFunction p q)) (∑ i : ι, p i * Real.log (p i)) 1

The derivative of q ↦ log Z_q at the probability point q = 1 is the information-dimension numerator ∑ i, p i * log (p i). (At q = 1 the surviving summands give p i * log (p i), and the empty cells p i = 0 contribute 0 = 0 * log 0 automatically, by Real.log 0 = 0.)

source
theorem Oseledets.Multifractal.renyiDim_antitone {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hpos : ∃ (i : ι), 0 < p i) (hsum : ∑ i : ι, p i = 1) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
Antitone fun (q : ℝ) => renyiDim p ε q

Antitonicity of the Rényi (generalized) dimension. For a probability weight family p : ι → ℝ (0 ≤ p i, ∑ i, p i = 1, with at least one positive weight) at a scale 0 < ε < 1, the Rényi dimension q ↦ D_q is non-increasing in q. This is the secant-slope argument: the slope g q = log Z_q / (q - 1) of the convex log Z (anchored at q = 1) is non-decreasing, and D_q = g q / log ε with log ε < 0 flips it to antitone; the information-dimension point q = 1 is glued in by the convex supporting-line inequality (numerator h'(1) = ∑ i, p i log p i).