Documentation

Oseledets.Multifractal.BernoulliHeterogeneous

Genuine q-dependence of the Rényi spectrum of a biased Bernoulli measure (issue #19) #

The downstream WITNESS of issue #19 needs the q-dependence of the Rényi (generalized) dimension spectrum to be genuinely non-vacuous — not a bare existential ∃ q₁ q₂, D q₁ ≠ D q₂ that could be satisfied trivially by a degenerate (uniform / monofractal) measure whose whole spectrum is a single point. This file supplies the pure measure-theoretic prerequisites that make the witness real, for the load-bearing biased 2-symbol Bernoulli measure.

The chain is:

Main results #

Item 1 — the strict single-symbol entropy bound Hnu ν < log 2 #

source
theorem Oseledets.Multifractal.negMulLog_add_negMulLog_lt_log_two {p p' : ℝ} (hp : 0 < p) (hp' : 0 < p') (hsum : p + p' = 1) (hbias : p ≠ p') :
p.negMulLog + p'.negMulLog < Real.log 2

Two-point Shannon entropy is strictly below log 2. For a probability split p + p' = 1 with p ≠ p' and both p, p' > 0, the sum negMulLog p + negMulLog p' < log 2. This is the strict-concavity bound on the binary entropy: applying the strict concavity of Real.negMulLog (Real.strictConcaveOn_negMulLog) to the distinct points p ≠ p' at the midpoint weights 1/2, 1/2 gives (1/2) negMulLog p + (1/2) negMulLog p' < negMulLog ((1/2) p + (1/2) p'), whose right-hand argument is 1/2; since 2 · negMulLog (1/2) = log 2, doubling yields the claim.

source
theorem Oseledets.Multifractal.Hnu_lt_log_two {α₀ : Type u_1} [Fintype α₀] [DecidableEq α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {ν : MeasureTheory.Measure α₀} [MeasureTheory.IsProbabilityMeasure ν] {i j : α₀} (hij : i ≠ j) (huniv : Finset.univ = {i, j}) (hbias : (ν {i}).toReal ≠ (ν {j}).toReal) (hi : 0 < (ν {i}).toReal) (hj : 0 < (ν {j}).toReal) :
Hnu ν < Real.log 2

The load-bearing strict bound (2-symbol case): Hnu ν < log 2. For a probability law ν on an alphabet with exactly two symbols i ≠ j (Finset.univ = {i, j}) that is biased ((ν {i}).toReal ≠ (ν {j}).toReal) with both masses positive, the single-symbol Shannon entropy is strictly below the uniform maximum log 2 = log (Fintype.card α₀). The entropy unfolds (over the two-element universe) to negMulLog (ν {i}).toReal + negMulLog (ν {j}).toReal with the masses summing to 1 (disjoint singletons covering the universe), so the claim is the strict two-point entropy bound negMulLog_add_negMulLog_lt_log_two.

Item 2 — base heterogeneity of the biased Bernoulli measure #

source
theorem Oseledets.Multifractal.measure_coordPartition_cell_bern {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] (i : α₀) :
(bern ν) ((coordPartition (bern ν)).cells i) = ν {i}

Marginal identity for the coordinate partition of a Bernoulli measure. The mass that the i.i.d. product measure bern ν assigns to the 0-th coordinate cell {x | x 0 = i} is the single-symbol mass ν {i}: the cell is the preimage (Function.eval 0) ⁻¹' {i}, and the coordinate evaluation eval 0 is measure-preserving from bern ν = Measure.infinitePi (fun _ => ν) to its 0-th marginal ν (measurePreserving_eval_infinitePi).

source
theorem Oseledets.Multifractal.isHeterogeneous_coordPartition_bern {α₀ : Type u_1} [Fintype α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] (ν : MeasureTheory.Measure α₀) [MeasureTheory.IsProbabilityMeasure ν] {i j : α₀} (hbias : ν {i} ≠ ν {j}) :
IsHeterogeneous (bern ν) (coordPartition (bern ν))

Base heterogeneity of a biased Bernoulli measure. If the single-symbol law ν charges two distinct symbols i ≠ j with different masses (ν {i} ≠ ν {j}), the coordinate-partition cell masses of bern ν differ, so IsHeterogeneous (bern ν) (coordPartition (bern ν)). Immediate from the marginal identity measure_coordPartition_cell_bern: the cell mass at i is (ν {i}).toReal, so distinct atom masses give distinct cell masses.

Item 3 — explicit q-dependence of the Rényi spectrum #

source
theorem Oseledets.Multifractal.partitionFunctionMeasure_coordPartition_bern_zero {α₀ : Type u_1} [Fintype α₀] [DecidableEq α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {ν : MeasureTheory.Measure α₀} [MeasureTheory.IsProbabilityMeasure ν] {i j : α₀} (hij : i ≠ j) (huniv : Finset.univ = {i, j}) (hi : 0 < (ν {i}).toReal) (hj : 0 < (ν {j}).toReal) :
partitionFunctionMeasure (bern ν) (coordPartition (bern ν)) 0 = 2

The partition function of bern ν at q = 0 (2-symbol case) counts the two occupied cells: Z₀ = 2. Both atoms have positive mass, so each occupied guard contributes (mass)^0 = 1, and there are exactly two cells.

source
theorem Oseledets.Multifractal.renyiDimMeasure_q_dependent_bern {α₀ : Type u_1} [Fintype α₀] [DecidableEq α₀] [MeasurableSpace α₀] [MeasurableSingletonClass α₀] {ν : MeasureTheory.Measure α₀} [MeasureTheory.IsProbabilityMeasure ν] {i j : α₀} (hij : i ≠ j) (huniv : Finset.univ = {i, j}) (hbias : (ν {i}).toReal ≠ (ν {j}).toReal) (hi : 0 < (ν {i}).toReal) (hj : 0 < (ν {j}).toReal) {ε : ℝ} (hε0 : 0 < ε) (hε1 : ε < 1) :
∃ (q₁ : ℝ) (q₂ : ℝ), renyiDimMeasure (bern ν) (coordPartition (bern ν)) ε q₁ ≠ renyiDimMeasure (bern ν) (coordPartition (bern ν)) ε q₂

The non-vacuity core: genuine q-dependence of the Rényi spectrum of a biased Bernoulli measure. For a scale 0 < ε < 1 and a biased 2-symbol law ν (exactly two symbols i ≠ j, both of positive mass, with (ν {i}).toReal ≠ (ν {j}).toReal), the Rényi (generalized) dimension of bern ν for the coordinate partition takes different values at q = 0 and q = 1. Concretely D₀ = log 2 / (-log ε) (both atoms occupied, so Z₀ counts the two cells) and D₁ = -Hnu ν / log ε = Hnu ν / (-log ε) (the information dimension), and these differ precisely because Hnu ν < log 2 — the strict bound Hnu_lt_log_two (item 1). This is a non-vacuous witness: the inequality is not a bare existential, it is driven by the genuine bias of ν.