The local-dimension → Hausdorff-dimension bridge

This file connects the pointwise local dimension d_μ(x) of an absolutely-continuous probability measure (formalized in Oseledets/Multifractal/LocalDimension.lean) to the Hausdorff dimension dimH s of a full-measure carrier set s.

The headline result is:

• Oseledets.Multifractal.dimH_eq_finrank_of_ae_full_of_absolutelyContinuous — if μ is a probability measure on a finite-dimensional real inner-product space E, absolutely continuous w.r.t. a Haar measure, then every set s of full μ-measure has Hausdorff dimension equal to the ambient dimension finrank ℝ E.

The Frostman lower-bound machinery and the Billingsley upper bound are formulated over a bare metric space (MetricSpace + Borel + second-countable), so the general bridge dimH_eq_of_localDimension_eq applies to non-Euclidean ambient spaces — e.g. a symbolic shift.

Proof outline

• Upper bound dimH s ≤ finrank ℝ E. Immediate from s ⊆ univ, monotonicity dimH_mono, and the Mathlib computation Real.dimH_univ_eq_finrank.
• Lower bound finrank ℝ E ≤ dimH s. This is the mass-distribution / Frostman direction. We package a self-contained mass-distribution principle (le_dimH_of_uniform_ball_bound): if on a set A the measure satisfies a uniform ball bound μ.real (closedBall x r) ≤ r ^ a for all x ∈ A and all small r > 0, and μ A > 0, then a ≤ dimH A. The uniform sets A come from the a.e. local-dimension statement ae_tendsto_localDimension_of_absolutelyContinuous: for a < finrank, the limit log μ.real(B(x,r)) / log r → finrank forces, μ-a.e., a radius below which μ.real(B(x,r)) ≤ r ^ a. A countable exhaustion of s by such uniform sets then has positive measure on at least one piece, giving a ≤ dimH s; finally we let a → finrank.

Metric-space machinery

The Frostman lower bound, the Billingsley upper bound and the general bridge only ever use generic metric-space facts (dist, Metric.closedBall, ediam, the Vitali enlargement covering, and the Hausdorff-measure/dimH API). We therefore prove them over a genuine metric space with a Borel second-countable structure, so they are usable on non-inner-product ambient spaces.

theorem Oseledets.Multifractal.le_dimH_of_uniform_ball_bound {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {a : NNReal} (ha : 0 < a) {A : Set E} (hA : MeasurableSet A) {δ : ℝ} (hδ : 0 < δ) (hbound : ∀ x ∈ A, ∀ (r : ℝ), 0 < r → r ≤ δ → μ.real (Metric.closedBall x r) ≤ r ^ ↑a) {t : Set E} (hts : t ⊆ A) (hpos : 0 < μ t) : ↑a ≤ dimH t

Mass-distribution / Frostman principle (single uniform bound). Let μ be a finite measure on E, 0 < a, and A a set on which a uniform ball bound holds: there is a radius δ > 0 such that μ.real (closedBall x r) ≤ r ^ a for every x ∈ A and every 0 < r ≤ δ. If 0 < μ A, then a ≤ dimH A.

The proof is the classical mass-distribution argument: the restricted measure μ.restrict A is dominated by the a-dimensional Hausdorff measure (any small-diameter set either misses A — then carries no restricted mass — or contains a point of A, in which case it lies inside a small ball and the uniform bound applies). Evaluating that domination on A itself shows μH[a] A ≥ μ A > 0, hence dimH A ≥ a.

theorem Oseledets.Multifractal.exists_uniform_ball_bound_of_tendsto {E : Type u_1} [MetricSpace E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {x : E} {a d : ℝ} (had : a < d) (hx : Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)) : ∃ δ > 0, ∀ (r : ℝ), 0 < r → r ≤ δ → μ.real (Metric.closedBall x r) ≤ r ^ a

From the local-dimension limit to a uniform ball bound near a point. If at x the local-dimension quotient log μ.real(B(x,r)) / log r tends to d and a < d, then there is a radius δ > 0 below which μ.real (closedBall x r) ≤ r ^ a.

theorem Oseledets.Multifractal.measurable_measure_closedBall (E : Type u_1) [MetricSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] (r : ℝ) : Measurable fun (x : E) => μ (Metric.closedBall x r)

Measurability of the ball-mass function. For a finite measure μ and a fixed radius r, the map x ↦ μ (closedBall x r) is measurable.

theorem Oseledets.Multifractal.le_dimH_of_ae_tendsto_quotient {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] {d : ℝ} {s : Set E} (hs : μ sᶜ = 0) (hae : ∀ᵐ (x : E) ∂μ, Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)) : ENNReal.ofReal d ≤ dimH s

Lower bound from an a.e. local-dimension limit (Frostman direction). If μ is a probability measure and, μ-a.e., the local-dimension quotient log μ.real(B(x,r)) / log r tends to a real value d, then every set s of full μ-measure has Hausdorff dimension at least d (more precisely ENNReal.ofReal d ≤ dimH s).

This packages the mass-distribution argument: for each a < d the a.e. limit yields, on a positive-measure measurable piece of s, a uniform upper ball bound μ.real(B(x,r)) ≤ r ^ a, and le_dimH_of_uniform_ball_bound upgrades it to a ≤ dimH s; letting a → d finishes.

The Billingsley upper bound

The companion to the Frostman lower bound le_dimH_of_uniform_ball_bound. Where Frostman gives a ≤ dimH from an upper ball bound μ(B(x,r)) ≤ r ^ a, the Billingsley principle gives dimH ≤ a from a lower ball bound μ(B(x,r)) ≥ r ^ a available at arbitrarily small radii (a fine cover). The proof is a Vitali τ-enlargement covering argument: a disjoint subfamily of such balls whose enlargements cover A controls the a-dimensional Hausdorff pre-measure by a fixed multiple of μ (univ), which is finite; feeding coverings of vanishing diameter into hausdorffMeasure_le_liminf_tsum shows μH[a] A < ∞, whence dimH A ≤ a.

theorem Oseledets.Multifractal.dimH_le_of_fine_cover_mass_lower {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {a : ℝ} (ha : 0 ≤ a) {A : Set E} (hfine : ∀ x ∈ A, ∀ (ε : ℝ), 0 < ε → ∃ (r : ℝ), 0 < r ∧ r ≤ ε ∧ ENNReal.ofReal (r ^ a) ≤ μ (Metric.closedBall x r)) : dimH A ≤ ENNReal.ofReal a

Billingsley upper bound on the Hausdorff dimension (fine-cover form). Let μ be a finite measure on E, 0 ≤ a, and A a set on which a lower ball bound holds at arbitrarily small scales: for every x ∈ A and every ε > 0 there is a radius r ∈ (0, ε] with ENNReal.ofReal (r ^ a) ≤ μ (closedBall x r). Then dimH A ≤ a.

This is the classical mass-distribution argument run "in reverse": a Vitali τ-enlargement of a disjoint subfamily of such balls covers A while ∑ diam ^ a ≤ (2 τ) ^ a · μ (univ) < ∞.

theorem Oseledets.Multifractal.exists_fine_ball_lower_of_tendsto {E : Type u_1} [MetricSpace E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {x : E} {a d : ℝ} (had : d < a) (hxsupp : ∀ (r : ℝ), 0 < r → 0 < μ (Metric.closedBall x r)) (hx : Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)) (ε : ℝ) : 0 < ε → ∃ (r : ℝ), 0 < r ∧ r ≤ ε ∧ ENNReal.ofReal (r ^ a) ≤ μ (Metric.closedBall x r)

From the local-dimension limit to a fine lower ball bound near a point. If at x every closed ball of positive radius has positive μ-mass (i.e. x is in the support of μ) and the local-dimension quotient log μ.real(B(x,r)) / log r tends to d with d < a, then for every ε > 0 there is a radius r ∈ (0, ε] with ENNReal.ofReal (r ^ a) ≤ μ (closedBall x r).

This is the "reverse" of exists_uniform_ball_bound_of_tendsto, feeding the Billingsley upper bound. Because the genuine limit is < a, the quotient is eventually < a, which (as log r < 0 and the ball mass is positive) becomes a lower bound μ.real(B(x,r)) ≥ r ^ a for all small r. The support hypothesis rules out the degenerate μ(B(x,r)) = 0 case (where log 0 = 0 makes the quotient vanish and no positive lower bound can hold).

theorem Oseledets.Multifractal.ball_mass_pos_of_tendsto_pos {E : Type u_1} [MetricSpace E] [MeasurableSpace E] {μ : MeasureTheory.Measure E} {x : E} {d : ℝ} (hd : 0 < d) (hx : Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds d)) (r : ℝ) : 0 < r → 0 < μ (Metric.closedBall x r)

A positive local-dimension limit forces positive ball masses. If the local-dimension quotient log μ.real(B(x,r)) / log r tends to a positive value d, then every closed ball around x of positive radius has positive μ-mass. Otherwise some ball would be μ-null, and by monotonicity all smaller balls too, making the quotient identically 0 near 0 (as log 0 = 0), contradicting d > 0.

theorem Oseledets.Multifractal.dimH_eq_of_localDimension_eq {E : Type u_1} [MetricSpace E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] {α : NNReal} (hα : 0 < α) {s : Set E} (hs : μ sᶜ = 0) (h : ∀ x ∈ s, Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑α)) : dimH s = ↑α

The local-dimension → Hausdorff-dimension bridge (general form). Let μ be a probability measure on a metric space E, 0 < α, and s a set of full μ-measure on which the local-dimension quotient log μ.real(B(x,r)) / log r tends, as r → 0⁺, to the constant α for every x ∈ s. Then dimH s = α.

Both inequalities use a single hypothesis. The lower bound α ≤ dimH s is the Frostman direction le_dimH_of_ae_tendsto_quotient, fed by the limit holding μ-a.e. (it holds everywhere on the conull s). The upper bound dimH s ≤ α is the Billingsley direction dimH_le_of_fine_cover_mass_lower: for any a > α the pointwise limit produces, at arbitrarily small radii, a lower ball bound μ(B(x,r)) ≥ r ^ a (the positive limit α guarantees the balls have positive mass), so dimH s ≤ a; letting a ↓ α finishes.

The pointwise (not merely a.e.) limit on s is essential for the upper bound: a μ-null subset of s can carry Hausdorff dimension larger than α, so an a.e.-only hypothesis cannot bound dimH s from above. The positivity 0 < α is needed both for Frostman (le_dimH_of_uniform_… requires a positive exponent) and to force the ball masses positive.

The Euclidean (finite-dimensional inner-product) specializations

These results genuinely need the inner-product / finite-dimensional structure: they speak of the ambient dimension finrank ℝ E, of Haar measures, and of the absolutely-continuous local-dimension computation ae_tendsto_localDimension_of_absolutelyContinuous. They reuse the metric machinery above (a finite-dimensional inner-product space is a Borel, second-countable metric space).

theorem Oseledets.Multifractal.dimH_le_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (s : Set E) : dimH s ≤ ↑(Module.finrank ℝ E)

Upper bound on the Hausdorff dimension of any set. In a finite-dimensional real inner-product space the Hausdorff dimension of any set is bounded by the ambient dimension.

theorem Oseledets.Multifractal.dimH_eq_finrank_of_ae_full_of_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] [ν.IsAddHaarMeasure] (hμν : μ.AbsolutelyContinuous ν) {s : Set E} (hs : μ sᶜ = 0) : dimH s = ↑(Module.finrank ℝ E)

The local-dimension → Hausdorff-dimension bridge (headline). Let μ be a probability measure on a finite-dimensional real inner-product space E, absolutely continuous with respect to a Haar measure ν. Then every set s of full μ-measure has Hausdorff dimension equal to the ambient dimension finrank ℝ E.

The upper bound is the trivial dimH s ≤ dimH univ = finrank. The lower bound is the mass-distribution argument packaged in le_dimH_of_ae_tendsto_quotient, fed by the a.e. local-dimension limit ae_tendsto_localDimension_of_absolutelyContinuous.

theorem Oseledets.Multifractal.dimH_eq_finrank_carrier_of_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] [ν.IsAddHaarMeasure] (hμν : μ.AbsolutelyContinuous ν) (hpos : 0 < Module.finrank ℝ E) : dimH {x : E | Filter.Tendsto (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑(Module.finrank ℝ E))} = ↑(Module.finrank ℝ E)

Tie-back: the absolutely-continuous case via the general bridge. When the ambient dimension is positive, the headline a.c. result is recovered through dimH_eq_of_localDimension_eq on the specific conull carrier s₀ = {x | log μ.real(B(x,r))/log r → finrank}, on which the local dimension equals finrank for every point (so the pointwise Billingsley hypothesis is met). This is a sanity check that the general bridge subsumes the a.c. computation.