Coarse-grained multifractal analysis: log-convexity of the partition function

This file proves the mathematical heart of the coarse-grained multifractal theory: the log-convexity of the generalized partition function Z_q = ∑_{p i > 0} (p i) ^ q of a finite weight family p : ι → ℝ as a function of the parameter q, and the corresponding concavity of the mass exponent τ(q) = log Z_q / log ε (for 0 < ε < 1).

The proof is the classical Hölder / cumulant-convexity argument, with no derivatives. The midpoint convexity inequality Z_{a q₁ + b q₂} ≤ (Z q₁) ^ a · (Z q₂) ^ b (for nonnegative weights a, b with a + b = 1) is exactly the two-term Hölder inequality with conjugate exponents 1/a, 1/b; taking logarithms and using monotonicity of log turns it into the convexity inequality for log ∘ Z.

Main results

• Oseledets.Multifractal.partitionFunction_holder: the multiplicative Hölder inequality Z_{a q₁ + b q₂} ≤ (Z q₁) ^ a · (Z q₂) ^ b.
• Oseledets.Multifractal.logPartitionFunction_convexOn: q ↦ log Z_q is convex on ℝ.
• Oseledets.Multifractal.massExponent_concaveOn: for 0 < ε < 1, the mass exponent q ↦ τ(q) = log Z_q / log ε is concave on ℝ (the negative factor 1 / log ε flips convex to concave).

theorem Oseledets.Multifractal.partitionFunction_holder {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) {a b q₁ q₂ : ℝ} (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) : partitionFunction p (a * q₁ + b * q₂) ≤ partitionFunction p q₁ ^ a * partitionFunction p q₂ ^ b

Multiplicative Hölder inequality for the partition function. For nonnegative weights a, b with a + b = 1 and any exponents q₁, q₂, the partition function at the convex combination a q₁ + b q₂ is bounded by the weighted geometric mean of the partition functions at q₁ and q₂: Z_{a q₁ + b q₂} ≤ (Z q₁) ^ a · (Z q₂) ^ b. This is the two-term Hölder inequality with conjugate exponents 1/a, 1/b applied on the support {i : 0 < p i}.

theorem Oseledets.Multifractal.logPartitionFunction_convexOn {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hpos : ∃ (i : ι), 0 < p i) : ConvexOn ℝ Set.univ fun (q : ℝ) => Real.log (partitionFunction p q)

The logarithm of the partition function, q ↦ log Z_q, is convex on all of ℝ. This is the cumulant-convexity / Hölder property and is the mathematical core of the multifractal theory. The hypothesis ∃ i, 0 < p i guarantees Z_q > 0 so the logarithm is well behaved.

theorem Oseledets.Multifractal.massExponent_concaveOn {ι : Type u_1} [Fintype ι] {p : ι → ℝ} (hp : ∀ (i : ι), 0 ≤ p i) (hpos : ∃ (i : ι), 0 < p i) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) : ConcaveOn ℝ Set.univ fun (q : ℝ) => massExponent p ε q

For a scale 0 < ε < 1 the mass exponent q ↦ τ(q) = log Z_q / log ε is concave on ℝ. Since log ε < 0, dividing the convex log Z_q by log ε flips convexity to concavity.