Pointwise local dimension: the absolutely-continuous case

This file delivers the absolutely-continuous (a.c.) special case of issue #16, item 5: for a probability measure μ on a finite-dimensional real normed space that is absolutely continuous with respect to the Haar (= Lebesgue) measure, the pointwise local dimension d_μ(x) = lim_{r→0⁺} log μ(B(x,r)) / log r exists and equals the ambient dimension finrank ℝ E, for μ-almost every x.

This is the standard Lebesgue-density / measure-differentiation result and uses no dynamics: the proof assembles

• the Besicovitch differentiation theorem Besicovitch.ae_tendsto_rnDeriv — μ(closedBall x r) / ν(closedBall x r) → (dμ/dν)(x) as r → 0⁺, ν-a.e.;
• the Radon–Nikodym density is finite and positive μ-a.e. (Measure.rnDeriv_lt_top, Measure.rnDeriv_pos) when μ ≪ ν;
• the Haar ball-volume scaling Measure.addHaar_real_closedBall' — ν(closedBall x r) = r ^ (finrank ℝ E) · ν(closedBall 0 1);
• a real-analytic logarithm limit (proved here as logBall_div_log_tendsto): if μ.real(B(x,r)) = ratio(r) · r^d · C with ratio(r) → L > 0 and C > 0, then log μ.real(B(x,r)) / log r = (log ratio(r) + log C) / log r + d → d, because log r → -∞ kills the bounded numerator log ratio(r) + log C while d · log r / log r = d.

Main results

• Oseledets.Multifractal.localDimension — the upper local/pointwise dimension d̄_μ(x), defined as the limsup of log μ.real(B(x,r)) / log r as r → 0⁺. In the a.c. case below the genuine limit exists, so this limsup is the honest local dimension.
• Oseledets.Multifractal.ae_tendsto_localDimension_of_absolutelyContinuous — the headline a.e.-convergence of the local-dimension quotient to finrank ℝ E.
• Oseledets.Multifractal.ae_localDimension_eq_finrank — the corollary localDimension μ x = finrank ℝ E for μ-a.e. x.

Scope (what is, and is NOT, formalized here)

This is only the absolutely-continuous case, a pure measure-differentiation statement with no dynamics. The general singular / SRB exact-dimensionality theory — the Ledrappier–Young formula and the absolute continuity of the conditional measures on unstable manifolds — is the deep research frontier shared with issue #10's Pesin SRB measures and is deliberately not formalized here.

noncomputable def Oseledets.Multifractal.localDimension {E : Type u_1} [PseudoMetricSpace E] [MeasurableSpace E] (μ : MeasureTheory.Measure E) (x : E) : ℝ

The upper local (pointwise) dimension d̄_μ(x) of a measure μ at a point x: the limsup as r → 0⁺ of log μ.real(closedBall x r) / log r (where μ.real s = (μ s).toReal). For the absolutely-continuous case treated in this file the genuine limit exists, so this limsup coincides with the honest local dimension lim_{r→0⁺} log μ(B(x,r)) / log r.

Equations

• Oseledets.Multifractal.localDimension μ x = Filter.limsup (fun (r : ℝ) => Real.log (μ.real (Metric.closedBall x r)) / Real.log r) (nhdsWithin 0 (Set.Ioi 0))

theorem Oseledets.Multifractal.logBall_div_log_tendsto {d : ℕ} {value ratio : ℝ → ℝ} {L C : ℝ} (hL : 0 < L) (hC : 0 < C) (hratio : Filter.Tendsto ratio (nhdsWithin 0 (Set.Ioi 0)) (nhds L)) (hval : ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0), value r = ratio r * (r ^ d * C)) : Filter.Tendsto (fun (r : ℝ) => Real.log (value r) / Real.log r) (nhdsWithin 0 (Set.Ioi 0)) (nhds ↑d)

The logarithm limit. Suppose value : ℝ → ℝ factors, for r near 0⁺, as value r = ratio r · (r ^ d · C) with ratio r → L, 0 < L, and 0 < C. Then log (value r) / log r → d as r → 0⁺. Indeed log (value r) = log (ratio r) + d · log r + log C, so the quotient is (log (ratio r) + log C) / log r + d; as r → 0⁺ the factor (log r)⁻¹ → 0 kills the convergent numerator while the d term survives.

theorem Oseledets.Multifractal.ae_tendsto_localDimension_of_absolutelyContinuous {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] [ν.IsAddHaarMeasure] (hμν : μ.AbsolutelyContinuous ν) : ∀ᵐ (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))

Local dimension of an absolutely-continuous probability measure (a.e. convergence). Let μ be a probability measure on a finite-dimensional real inner-product space E, absolutely continuous with respect to a Haar measure ν (e.g. ν = volume). Then for μ-almost every x the local-dimension quotient log μ.real(B(x,r)) / log r converges, as r → 0⁺, to the ambient dimension finrank ℝ E.

This is the standard Lebesgue-density / measure-differentiation result: Besicovitch differentiation gives μ(B(x,r))/ν(B(x,r)) → (dμ/dν)(x) ∈ (0,∞) μ-a.e.; the Haar ball-volume scaling ν(B(x,r)) = r^(finrank) · ν(B(0,1)) then turns the logarithm of μ.real(B(x,r)) into log((dμ/dν)(x)) + finrank · log r + log ν.real(B(0,1)) + o(1), whose ratio to log r → -∞ is finrank.

theorem Oseledets.Multifractal.ae_localDimension_eq_finrank {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ ν : MeasureTheory.Measure E} [MeasureTheory.IsProbabilityMeasure μ] [ν.IsAddHaarMeasure] (hμν : μ.AbsolutelyContinuous ν) : ∀ᵐ (x : E) ∂μ, localDimension μ x = ↑(Module.finrank ℝ E)

Local dimension of an absolutely-continuous probability measure (value). For μ-almost every x, the upper local dimension localDimension μ x equals the ambient dimension finrank ℝ E. This is the corollary of ae_tendsto_localDimension_of_absolutelyContinuous: where the genuine limit exists, the limsup defining localDimension returns that limit.