Foundation for Rokhlin's formula for an expanding map #
This module freezes the interface on which the proof of Rokhlin's entropy formula
h_μ(T, ξ) = ∫ log |det Dₓ T| dμ for an absolutely continuous, uniformly expanding self-map
T : EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d) rests. It contains two small,
near-trivial pieces that later (harder) nodes consume verbatim, so the signatures here are
chosen to match exactly the hypotheses those nodes need.
The absolutely-continuous density layer #
When μ ≪ volume (and μ is finite, hence has a Lebesgue decomposition w.r.t. volume), the
Radon–Nikodym density ρ := μ.rnDeriv volume recovers μ as volume.withDensity ρ, and ρ is
strictly positive μ-almost everywhere. These are thin wrappers over
MeasureTheory.Measure.withDensity_rnDeriv_eq and MeasureTheory.Measure.rnDeriv_pos.
We deliberately do not record any log ρ ∈ L¹ integrability statement here: the C¹
absolutely continuous case can fail it, so log-density integrability is carried as a separate
hypothesis by the later nodes.
The injectivity-partition predicate #
IsInjectivityPartition μ T ξ packages the three hypotheses Coudène's conditional-expectation
proof of Rokhlin's formula needs from a finite measurable partition ξ:
Tis injective on each cell (Set.InjOn),- each cell is measurable (
MeasurableSet), - the union of the cell frontiers is
μ-null.
The first two fields are literally the hypotheses hf and hs of Mathlib's change-of-
variables lemma MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul, which the next
node feeds them into. We deliberately do not include a Markov condition (T '' ξᵢ a union of
cells) — the conditional-expectation argument needs only injectivity — and we do not bake in
IsGenerating, which is a separate hypothesis of the final formula.
Main definitions #
Oseledets.IsInjectivityPartition— the injectivity/measurability/null-boundary predicate on a finite measurable partition.
Main results #
Oseledets.withDensity_rnDeriv_volume_eq—volume.withDensity (μ.rnDeriv volume) = μfor an absolutely continuous finite measure.Oseledets.rnDeriv_volume_pos— the Radon–Nikodym density isμ-a.e. strictly positive.
N5.1 — the absolutely-continuous density layer #
For a finite measure μ absolutely continuous w.r.t. Lebesgue volume, the
Radon–Nikodym density ρ := μ.rnDeriv volume recovers μ:
volume.withDensity (μ.rnDeriv volume) = μ. A thin wrapper over
MeasureTheory.Measure.withDensity_rnDeriv_eq (μ is finite, hence has a Lebesgue
decomposition w.r.t. volume).
The Radon–Nikodym density μ.rnDeriv volume of an absolutely continuous finite measure is
strictly positive μ-almost everywhere. A thin wrapper over
MeasureTheory.Measure.rnDeriv_pos.
N5.2 — the injectivity-partition predicate #
An injectivity partition for a self-map T and a finite measurable partition ξ:
the three hypotheses Coudène's conditional-expectation proof of Rokhlin's formula needs.
inj:Tis injective on each cellξ.cells i;meas: each cell is measurable;boundaryNull: the union of the cell frontiers isμ-null.
The inj and meas fields are exactly the hypotheses (hf, hs) consumed by Mathlib's
change-of-variables lemma MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul. No
Markov condition and no IsGenerating hypothesis are included here.
Tis injective on each cell of the partition.- meas (i : ι) : MeasurableSet (ξ.cells i)
Each cell of the partition is measurable.
The union of the cell frontiers is
μ-null.
Instances For
Each individual cell frontier is μ-null, extracted from boundaryNull via monotonicity.
N5.3 — the per-cell Jacobian–measure identity #
The change-of-variables crux of Rokhlin's formula (per-cell version).
For an absolutely continuous finite measure μ ≪ volume with density ρ := μ.rnDeriv volume, a
differentiable self-map T with non-vanishing Jacobian on the cell ξ.cells i, and an
injectivity partition ξ, the measure μ (ξᵢ ∩ T⁻¹' B) is recovered as the integral over the
image T '' ξᵢ ∩ B of the per-branch transfer density
ρ (g⁻¹ y) / |det Dₓ T|ₓ₌g⁻¹ y, where g⁻¹ = Function.invFunOn T (ξ.cells i) is the branch of the
inverse of T on the cell.
The orientation of the density ratio is pinned by the change-of-variables identity itself: writing
S := ξᵢ ∩ T⁻¹' B, we have μ S = ∫_S ρ ∂volume and, by
MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul applied to T on S with the
transfer density as the integrand, ∫_{T '' S} (transfer) = ∫_S |det DT_x| · (transfer ∘ T). On
S ⊆ ξᵢ the inverse branch collapses (invFunOn T ξᵢ (T x) = x), so the integrand becomes
|det DT_x| · ρ x / |det DT_x| = ρ x, recovering μ S. The non-vanishing Jacobian hypothesis
hdet is exactly what makes this cancellation hold: where det DT_x = 0 the ratio would undercount
ρ, so it cannot be dropped.
N5.4 — the conditional-entropy = Jacobian-integral identity (Coudène Prop 12.1) #
The per-branch transfer density on the cell ξ.cells i:
transferDensity ξ i T y = ρ(branchᵢ y) / ofReal|det DT(branchᵢ y)|, where branchᵢ = invFunOn T (ξ.cells i) is the inverse branch of T on the cell. This is the integrand of N5.3.
Equations
- Oseledets.transferDensity ξ i T y = μ.rnDeriv MeasureTheory.volume (Function.invFunOn T (ξ.cells i) y) / ENNReal.ofReal |(fderiv ℝ T (Function.invFunOn T (ξ.cells i) y)).det|
Instances For
The per-image branch weight wᵢ y = (T''ξᵢ).indicator (transferDensity / ρ) y. On the
image T''ξᵢ it is the relative weight of the i-th preimage branch; off it, 0. Postcomposed
with T this is the candidate for the conditional probability E(1_{ξᵢ}|comap T mα).
Equations
- Oseledets.branchWeight ξ i T y = (T '' ξ.cells i).indicator (fun (y : EuclideanSpace ℝ (Fin d)) => Oseledets.transferDensity ξ i T y / μ.rnDeriv MeasureTheory.volume y) y
Instances For
The inner density a ↦ ρ a / ofReal|det DT a| is measurable: a quotient of the measurable
Radon–Nikodym density by the measurable determinant data.
The image cell T '' ξ.cells i is measurable: T is continuous and injective on the
measurable cell ξ.cells i, so the image is Borel by the Lusin–Souslin theorem
(MeasurableSet.image_of_continuousOn_injOn).
On the image cell T '' ξ.cells i, the transferDensity agrees with the measurable extension
Function.extend (ξᵢ.restrict T) (a ↦ ρ a / ofReal|det DT a|) 0: the embedding
e = ξᵢ.restrict T is injective and hits y at the subtype point ⟨invFunOn T ξᵢ y, _⟩, so
extend evaluates the inner density at that preimage — exactly the transfer integrand.
branchWeight is measurable: it is the indicator on the (measurable) image cell of the
quotient of the measurable extension of the transfer integrand by the density ρ.
The set {ρ = 0} carries no μ-mass: μ {ρ = 0} = ∫⁻_{ρ=0} ρ ∂volume = 0, since ρ = 0
on that set and μ = volume.withDensity ρ.
The heart sub-lemma (N5.4 core change of variables). For a measurable set B, the
μ-integral of the per-image branch weight over B recovers the measure of the slice of the
i-th cell that maps into B:
∫⁻ y in B, branchWeight ξ i T y ∂μ = μ (ξ.cells i ∩ T⁻¹' B).
Route: rewrite the μ-integral as a volume-integral of ρ · branchWeight
(setLIntegral_rnDeriv_mul); on the image cell ρ · branchWeight = transferDensity volume-a.e.
(the density ratio ρ · (transfer / ρ) collapses where 0 < ρ < ∞, and the discarded {ρ = 0}
part carries no transfer mass by N5.3 applied to {ρ = 0}, while {ρ = ∞} is volume-null);
finally ∫⁻_{T''ξᵢ ∩ B} transferDensity = μ (ξᵢ ∩ T⁻¹B) is exactly N5.3.
The conditional probability candidate condProb ξ i T x, the real value
(branchWeight ξ i T (T x)).toReal of the per-image branch weight at the image point. By the heart
sub-lemma this is the conditional probability of ξᵢ given the comap-of-T σ-algebra.
Equations
- Oseledets.condProb ξ i T x = (Oseledets.branchWeight ξ i T (T x)).toReal
Instances For
The branch weight is μ-a.e. finite (its μ-integral over the whole space is μ ξᵢ ≤ 1).
The set-integral of condProb over a generator T⁻¹' B recovers μ.real (ξᵢ ∩ T⁻¹B):
push the μ-integral of (branchWeight ∘ T).toReal through integral_toReal to the lintegral
∫⁻_{T⁻¹B} branchWeight (T ·) ∂μ, change variables by measure-preservation (setLIntegral_map,
map T μ = μ) to ∫⁻_B branchWeight ∂μ = μ (ξᵢ ∩ T⁻¹B) (the heart sub-lemma).
condProb is integrable on any μ-finite measurable set (it is nonnegative and bounded in
L¹ by the kernel mass; here we use that it is a bounded-by-(branchWeight∘T).toReal, finite-
integral function — its global μ-integral is μ ξᵢ ≤ 1).
N5.4 — conditional probability identification. The regular-conditional kernel mass of the
cell ξᵢ given the comap-of-T σ-algebra equals, μ-a.e., the branch-weight candidate
condProb. The candidate is comap T mα-measurable (a measurable function of T x) and, on every
generator T⁻¹' B, has the right set-integral μ (ξᵢ ∩ T⁻¹B) by the heart sub-lemma; uniqueness of
the conditional expectation (ae_eq_condExp_of_forall_setIntegral_eq) and
condExpKernel_ae_eq_condExp then pin the kernel mass to condProb.
The density-ratio orientation, pinned on the cell ξᵢ. For x ∈ ξ.cells i, the branch
weight evaluated at the image collapses (the inverse branch returns x):
branchWeight ξ i T (T x) = (ρ x / ofReal|det DT x|) / ρ (T x). The numerator density ρ sits at
x, the denominator ρ at T x — the orientation that makes ∫ (log ρ∘T − log ρ) telescope to
0 under T-invariance.
The log density-ratio identity on ξᵢ. For x ∈ ξ.cells i with ρ x, ρ (T x) > 0,
log (condProb ξ i T x) = log (ρ x).toReal − log |det DT x| − log (ρ (T x)).toReal.
The Jacobian log-cocycle jacLog T x = log |det DT x| + log ρ(Tx) − log ρ(x). Its μ-mean
is ∫ log|det DT| dμ, because the bracket ∫ (log ρ∘T − log ρ) telescopes to 0 under
T-invariance (the orientation pinned by log_condProb_eq_on_cell).
Equations
Instances For
The μ-integral of the Jacobian log-cocycle is the integral of log|det DT|: the
log ρ∘T − log ρ bracket telescopes to 0 by T-invariance (integral_map with map T μ = μ),
using hlogρ : log ρ ∈ L¹(μ) (load-bearing — without it the bracket is ∞ − ∞) and
hlogdet : log|det DT| ∈ L¹(μ).
jacLog is μ-integrable (sum of log|det DT|, log ρ∘T, log ρ, each in L¹).
The per-cell pull-out identity. For each cell i, the μ-mean of negMulLog (condProb i)
equals the set-integral of the Jacobian log-cocycle over the cell:
∫ negMulLog (condProb ξ i T x) ∂μ = ∫_{ξᵢ} jacLog T μ x ∂μ.
Pull-out: condProb i = E(1_{ξᵢ} | comap T mα) a.e., and log (condProb i) is
comap T mα-measurable, so ∫ condProb i · log (condProb i) = ∫ 1_{ξᵢ} · log (condProb i)
(condExp_mul_of_stronglyMeasurable_left + integral_condExp). On ξᵢ,
log (condProb i) = −jacLog (log_condProb_eq_on_cell, the pinned orientation), and
negMulLog t = −t · log t, so the term becomes ∫_{ξᵢ} jacLog.
N5.4 — the conditional-entropy = Jacobian-integral identity (Coudène Prop 12.1).
For an absolutely continuous, differentiable, injectivity-partitioned self-map T with
everywhere-nonsingular derivative and μ-integrable log ρ and log|det DT|, the conditional
Shannon entropy of ξ given the comap-of-T σ-algebra equals the integral of log|det DT|:
H(ξ | comap T mα) = ∫ log|det DT| dμ.
This is partition-independent (no IsGenerating). The proof: the condEntropy integrand
∑ᵢ negMulLog (κ ω ξᵢ).toReal has each kernel mass identified with the branch-weight candidate
condProb i (condExpKernel_cell_ae_eq_condProb); the per-cell pull-out
(integral_negMulLog_condProb_eq) turns each summand into ∫_{ξᵢ} jacLog; the cells partition the
space a.e. so the sum is ∫ jacLog; and ∫ jacLog = ∫ log|det DT| (integral_jacLog_eq, the
log ρ∘T − log ρ bracket telescoping to 0 by T-invariance — the pinned orientation).
N5.3.5 — the σ-algebra glue identifying the strict-future filtration #
The strict-future filtration is the T-comap of the ambient σ-algebra (for a generator).
For a measure-preserving system with a one-sided generating finite partition ξ, the supremum of
the increasing filtration k ↦ σ((⋁₀ᵏ⁻¹ T⁻ʲξ) pulled back by T) — the σ-algebra of the strict
future σ(⋁_{j≥1} T⁻ʲξ) — equals the comap of the ambient σ-algebra under T:
⨆ k, σ((ksJoin ξ k).pullback) = comap T mα.
The σ-algebra chain: σ((ksJoin ξ k).pullback) = comap T (σ(ksJoin ξ k))
(generatedSigmaAlgebra_pullback_eq_pulledBack then comap_generatedSigmaAlgebra_pulledBack);
commute comap T out of the supremum (comap_iSup); collapse the inner supremum
⨆ k, σ(ksJoin ξ k) = ⨆ k, comap (T^[k]) σ(ξ) (iSup_generatedSigmaAlgebra_ksJoin_eq); and
apply the generator hypothesis ⨆ k, comap (T^[k]) σ(ξ) = mα.
The ContinuousLinearMap determinant of fderiv ℝ T x equals the matrix determinant of the
derivative cocycle generator derivativeCocycle T x: the generator is the matrix representing
Dₓ T through toEuclideanCLM, whose LinearMap-coercion is toEuclideanLin, whose determinant
(LinearMap.det_toLin against the standard basis) is the matrix determinant.
N5.5 — the per-partition Rokhlin formula #
N5.5 — the per-partition Rokhlin formula. For an absolutely continuous, differentiable,
uniformly injectivity-partitioned self-map T with a one-sided generating partition ξ,
everywhere-nonsingular derivative, and μ-integrable log ρ and log|det DT|, the
Kolmogorov–Sinai entropy of T relative to ξ equals the integrated volume distortion:
h(T, ξ) = ∫ log |det (derivativeCocycle T x)| dμ.
Assembled from the sharp-rate identity
ksEntropyPartition hT ξ = condEntropy μ (⨆ k, σ((ksJoin ξ k).pullback)) ξ.cells
(ksEntropyPartition_eq_condEntropy_iSup), the σ-algebra glue
⨆ k, σ((ksJoin ξ k).pullback) = comap T mα (strictFuture_eq_comap_of_generating, using hgen),
and N5.4 (condEntropy_comap_eq_integral_log_abs_det). The integrand bridge
|det (fderiv ℝ T x)| = |det (derivativeCocycle T x)| (det_fderiv_eq_det_derivativeCocycle) puts
the right-hand side in the verbatim shape of sumPosExp_eq_integral_log_abs_det_of_expanding.
Note: like pesin_formula_expanding, the finite generating injectivity partition this requires
has no model on the non-compact EuclideanSpace ℝ (Fin d), so this is a correct implication that is
un-instantiated here; the genuine instance is rokhlin_equality_doublingMap
(Oseledets/Examples/Rokhlin/DoublingEquality.lean) on the compact circle.
Pesin — the unconditional expanding-map entropy formula #
Pesin's entropy formula for an absolutely-continuous uniformly-expanding map. For an
ergodic, absolutely-continuous (μ ≪ volume), differentiable, uniformly expanding self-map T of
EuclideanSpace ℝ (Fin d) with everywhere-nonsingular derivative and μ-integrable log-norm data,
together with a one-sided generating injectivity partition ξ and μ-integrable log ρ and
log|det DT|, the Kolmogorov–Sinai entropy equals the sum of the (all positive) Lyapunov exponents:
h_μ(T) = ∑ λ⁺ = ∫ log |det Df| dμ.
This is the placeholder-free assembly of the implication: the SRB property is supplied by the
genuine absolute-continuity hypothesis μ ≪ volume, not an opaque SRB axiom. The proof composes
three on-branch theorems: ksEntropy_eq_ksEntropyPartition_of_generating (the Kolmogorov–Sinai
generator theorem), ksEntropyPartition_eq_integral_log_abs_det (Rokhlin's per-partition formula,
N5.5), and sumPosExp_eq_integral_log_abs_det_of_expanding (the Pesin = Rokhlin right-hand-side
identity); the two det hypotheses are aligned by det_fderiv_eq_det_derivativeCocycle. The
StandardBorelSpace (EuclideanSpace ℝ (Fin d)) instance is the derived standardBorel_of_polish
instance — not assumed.
Vacuity caveat (honest disclosure). This is a correct implication, but its hypothesis bundle
has no model on the non-compact space EuclideanSpace ℝ (Fin d) = ℝ^d, so the theorem is
vacuously true — the EuclideanSpace assembly of the implication, not an exhibited instance.
A globally uniformly expanding (K > 1) self-map of ℝ^d admits no ergodic absolutely-continuous
invariant probability measure: e.g. for T = c • id (c > 1) the nested preimages
T⁻ⁿ(closedBall 0 R) have constant μ-mass, forcing an atom at the fixed point 0, contradicting
μ ≪ volume; in general uniform expansion on a non-compact space forces mass to escape to infinity
(every existence theorem for a.c. invariant measures of uniformly expanding maps is on a compact
manifold). The intended models live on a torus. A genuinely instantiated Pesin/Rokhlin equality
h_μ(T) = ∫ log|det DT| dμ = log 2 is Oseledets.Examples.Rokhlin.rokhlin_equality_doublingMap, on
the compact circle UnitAddCircle. A non-vacuous EuclideanSpace-style statement would require
porting the derivative-cocycle / expanding / Lyapunov-exponent layer to the torus (currently
EuclideanSpace-only).