Finite-time empirical cell-mass observables of a measure-preserving flow

This file builds the finite-resolution empirical-mass observable layer for a measure-preserving one-parameter flow φ : Oseledets.MeasurePreservingFlow μ on a probability space (X, μ). The central object is the finite-time empirical cell mass

empiricalCellMass φ C T x = T⁻¹ · ∫_0^T 𝟙_C (φ t x) dt,

a continuous-time Birkhoff average measuring the fraction of the orbit segment of length T through x that lies in the cell C. This is exactly the dynamical analogue of the empirical-measure mass μ_T^x(C) whose T → ∞ limit (under ergodicity) recovers the true mass μ(C) — the input to coarse-grained multifractal analysis.

Main results

• Oseledets.Multifractal.empiricalCellMass (def): the finite-time empirical cell mass, a continuous-time Birkhoff average. The companion unitWindow φ C x = ∫_0^1 𝟙_C (φ s x) ds is the single-step (unit-window) observable.

• Oseledets.Multifractal.integral_empiricalCellMass_eq (the non-vacuity anchor): for every finite T > 0, the space average of the finite-time empirical mass equals the true mass, ∫_x empiricalCellMass φ C T x ∂μ = (μ C).toReal. This proves the scaffolding genuinely computes μ(C); the proof is a Fubini swap plus measure-preservation of each time-t map.

• Oseledets.Multifractal.empiricalCellMass_natCast_eq: at integer times the empirical mass is the discrete Birkhoff average of the unit-window observable under the time-1 map, empiricalCellMass φ C N x = birkhoffAverage ℝ (φ 1) (unitWindow φ C) N x. This reduces the continuous-time convergence to the repository's discrete pointwise ergodic theorem.

• Oseledets.Multifractal.integral_unitWindow_eq: the unit-window space average equals the true mass, ∫_x unitWindow φ C x ∂μ = (μ C).toReal (same Fubini computation, T = 1).

• Oseledets.Multifractal.tendsto_empiricalCellMass_ae: under an ergodicity hypothesis on the time-1 map and integrability of the unit window, the integer-time empirical masses converge μ-a.e. to the true mass μ.real C.

Honest hypotheses

MeasurePreservingFlow supplies only per-time measurability of φ t, not joint (t, x)-measurability, so t ↦ 𝟙_C (φ t x) is not known integrable. Every statement that integrates over time therefore carries the precise joint-integrability / interval-integrability hypothesis it needs (hjoint, hii, hint); none is fabricated from the structure.

Ergodic (φ 1) μ is likewise never derived: ergodicity of the time-1 map of a flow can genuinely fail (e.g. without roof aperiodicity for a suspension), so it is carried as a hypothesis in the convergence statement.

N2a — the finite-time empirical cell mass

noncomputable def Oseledets.Multifractal.empiricalCellMass {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (C : Set X) (T : ℝ) (x : X) : ℝ

The finite-time empirical cell mass of the flow φ for the cell C, horizon T, and base point x: a continuous-time Birkhoff average

empiricalCellMass φ C T x = T⁻¹ · ∫_0^T 𝟙_C (φ t x) dt,

the time-averaged fraction of the length-T orbit segment through x lying in C. The definition requires no hypothesis: intervalIntegral of a non-integrable integrand is junk-valued, which is acceptable for a definition.

Equations

• Oseledets.Multifractal.empiricalCellMass φ C T x = T⁻¹ * ∫ (t : ℝ) in 0..T, C.indicator (fun (x : X) => 1) (φ.toFun t x)

noncomputable def Oseledets.Multifractal.unitWindow {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (C : Set X) (x : X) : ℝ

The unit-window observable unitWindow φ C x = ∫_0^1 𝟙_C (φ s x) ds: the mass accumulated by the length-1 orbit segment through x. It is the single-step generator whose discrete Birkhoff average reproduces the integer-time empirical masses.

Equations

• Oseledets.Multifractal.unitWindow φ C x = ∫ (s : ℝ) in 0..1, C.indicator (fun (x : X) => 1) (φ.toFun s x)

A shared Fubini computation: the time-t inner integral is constant

theorem Oseledets.Multifractal.indicator_flow_apply {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (C : Set X) (t : ℝ) (x : X) : C.indicator (fun (x : X) => 1) (φ.toFun t x) = (φ.toFun t ⁻¹' C).indicator (fun (x : X) => 1) x

The cell indicator pulled back along a flow map is the indicator of the preimage: 𝟙_C (φ t x) = 𝟙_{φ t ⁻¹' C} x.

theorem Oseledets.Multifractal.integral_indicator_flow_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) {C : Set X} (hC : MeasurableSet C) (t : ℝ) : ∫ (x : X), C.indicator (fun (x : X) => 1) (φ.toFun t x) ∂μ = μ.real C

For each time t, the space average of the cell indicator along the flow is the true mass: ∫_x 𝟙_C (φ t x) ∂μ = μ.real C. Uses measure-preservation of φ t to identify μ.real (φ t ⁻¹' C) = μ.real C.

N3a — THE NON-VACUITY ANCHOR

theorem Oseledets.Multifractal.integral_empiricalCellMass_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) {C : Set X} (hC : MeasurableSet C) {T : ℝ} (hT : 0 < T) (hjoint : MeasureTheory.Integrable (Function.uncurry fun (t : ℝ) (x : X) => C.indicator (fun (x : X) => 1) (φ.toFun t x)) ((MeasureTheory.volume.restrict (Set.uIoc 0 T)).prod μ)) : ∫ (x : X), empiricalCellMass φ C T x ∂μ = (μ C).toReal

The non-vacuity anchor. For every finite horizon T > 0, the space average of the finite-time empirical cell mass equals the true mass of the cell:

∫_x empiricalCellMass φ C T x ∂μ = (μ C).toReal.

This is the campaign's vacuity guard: it certifies that the empirical-mass scaffolding genuinely computes μ(C), for every finite T, not merely in a limit.

The proof pulls out T⁻¹, swaps the order of integration by Fubini (intervalIntegral_integral_swap, which needs the joint integrability hypothesis hjoint), evaluates the now-inner space integral ∫_x 𝟙_C (φ t x) ∂μ = μ.real C (constant in t, via measure-preservation), and finishes with T⁻¹ · (T · μ.real C) = μ.real C.

The hypothesis hjoint is the honest joint-integrability requirement Fubini needs: the structure MeasurePreservingFlow supplies only per-time measurability, so (t, x) ↦ 𝟙_C(φ t x) is not known integrable from the structure and must be supplied.

theorem Oseledets.Multifractal.integral_unitWindow_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) {C : Set X} (hC : MeasurableSet C) (hjoint : MeasureTheory.Integrable (Function.uncurry fun (s : ℝ) (x : X) => C.indicator (fun (x : X) => 1) (φ.toFun s x)) ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod μ)) : ∫ (x : X), unitWindow φ C x ∂μ = (μ C).toReal

The unit-window space average equals the true mass: ∫_x unitWindow φ C x ∂μ = (μ C).toReal. Same Fubini computation as the non-vacuity anchor, specialized to T = 1.

N3b — reduction to the repository's discrete Birkhoff theorem

theorem Oseledets.Multifractal.integral_unit_slice_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (C : Set X) (k : ℕ) (x : X) : ∫ (t : ℝ) in ↑k..↑k + 1, C.indicator (fun (x : X) => 1) (φ.toFun t x) = unitWindow φ C ((φ.toFun 1)^[k] x)

The unit-window slice. For a natural index k, the time integral of the cell indicator over the unit interval [k, k+1] equals the unit-window observable evaluated at the k-th iterate of the time-1 map:

∫_k^{k+1} 𝟙_C (φ t x) dt = unitWindow φ C ((φ 1)^[k] x).

The substitution t = s + k (intervalIntegral.integral_comp_add_right) shifts the interval to [0, 1]; flow additivity φ (s + k) = φ s ∘ φ k and φ (k) = (φ 1)^[k] rewrite the integrand.

theorem Oseledets.Multifractal.empiricalCellMass_natCast_eq {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} (φ : MeasurePreservingFlow μ) (C : Set X) (N : ℕ) (x : X) (hii : ∀ k < N, IntervalIntegrable (fun (t : ℝ) => C.indicator (fun (x : X) => 1) (φ.toFun t x)) MeasureTheory.volume (↑k) (↑k + 1)) : empiricalCellMass φ C (↑N) x = birkhoffAverage ℝ (φ.toFun 1) (unitWindow φ C) N x

Integer-time identity. At integer horizons the finite-time empirical cell mass is the discrete Birkhoff average of the unit-window observable under the time-1 map:

empiricalCellMass φ C N x = birkhoffAverage ℝ (φ 1) (unitWindow φ C) N x.

The time integral over [0, N] is split into adjacent unit windows (intervalIntegral.sum_integral_adjacent_intervals), each identified with the unit window at the corresponding iterate (integral_unit_slice_eq); the resulting sum is the Birkhoff sum, and the leading N⁻¹ makes it the Birkhoff average.

The hypothesis hii is the honest per-window interval-integrability requirement (each ∫_k^{k+1} must be well-defined for the splitting lemma); it cannot be derived from MeasurePreservingFlow, which gives only per-time measurability.

theorem Oseledets.Multifractal.tendsto_empiricalCellMass_ae {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsProbabilityMeasure μ] (φ : MeasurePreservingFlow μ) {C : Set X} (hC : MeasurableSet C) (herg : Ergodic (φ.toFun 1) μ) (hint : MeasureTheory.Integrable (unitWindow φ C) μ) (hjoint : MeasureTheory.Integrable (Function.uncurry fun (s : ℝ) (x : X) => C.indicator (fun (x : X) => 1) (φ.toFun s x)) ((MeasureTheory.volume.restrict (Set.uIoc 0 1)).prod μ)) (hii : ∀ (x : X) (k : ℕ), IntervalIntegrable (fun (t : ℝ) => C.indicator (fun (x : X) => 1) (φ.toFun t x)) MeasureTheory.volume (↑k) (↑k + 1)) : ∀ᵐ (x : X) ∂μ, Filter.Tendsto (fun (N : ℕ) => empiricalCellMass φ C (↑N) x) Filter.atTop (nhds (μ.real C))

Convergence to the true mass. Under ergodicity of the time-1 map φ 1 and integrability of the unit-window observable, the integer-time empirical cell masses converge μ-a.e. to the true mass μ.real C:

∀ᵐ x, (fun N : ℕ => empiricalCellMass φ C N x) → μ.real C.

The proof feeds unitWindow φ C into the repository's pointwise ergodic theorem Oseledets.tendsto_birkhoffAverage_ae_integral, whose limit ∫ unitWindow φ C ∂μ equals μ.real C by integral_unitWindow_eq, then transports the limit across the integer-time identity empiricalCellMass_natCast_eq.

Ergodic (φ 1) μ is a hypothesis: it is never derived (it can genuinely fail for a flow without further structure). The interval-integrability data hii is the honest per-window requirement of the integer-time identity, and hjoint is the joint-integrability requirement of the unit-window average.