Flow-refined partition and finite-resolution multifractal observables (issue #18)

This file builds the flow-transported coarse-grained partition and the finite-resolution (pre-limit) observable layer of issue #18, abstractly over a supplied measure-preserving flow φ : Oseledets.MeasurePreservingFlow μ. It is a definitions + interface layer on top of the existing entropy partition machinery (Oseledets.Entropy) and the coarse-grained multifractal measure layer of issue #16 (Oseledets.Multifractal.Measure); the heavy multifractal theorems are already proved there and are consumed, not re-derived, here.

The bridge is deliberately minimal: the entire #16 ↔ #18 interface is the cell-mass family cellMassFamily P : ι → ℝ, i ↦ (μ (P.cells i)).toReal. This is exactly the weight family consumed by Oseledets.Multifractal.partitionFunctionMeasure / renyiDimMeasure / renyiDimFlow, so none of Z_q, τ(q), D_q, f(α) is redefined here.

Main definitions

• Oseledets.Multifractal.dynamicalRefine: the depth-n flow-refined partition, the join over k = 0, …, n-1 of the pullbacks (φ (k • Δ))⁻¹ P of a supplied seed partition P, realized with the flat Fin n → ι index discipline of Oseledets.Entropy.ksJoin.
• Oseledets.Multifractal.cellMassFamily: the cell-mass family i ↦ (μ (P.cells i)).toReal, the whole #16 ↔ #18 interface.
• Oseledets.Multifractal.IsHeterogeneous: the honest non-uniformity hypothesis on P — two cells of distinct mass. Its failure is exactly the equal-measure monofractal degeneracy of #16.
• Oseledets.Multifractal.finiteTimePartitionEntropy: the depth-n (pre-limit) Shannon entropy of dynamicalRefine, distinct from its Kolmogorov–Sinai (Fekete) limit.
• Oseledets.Multifractal.finiteTimeFlowExponent: the finite-time (pre-limit) Lyapunov estimator log ‖coverCocycle (x, s) t‖ / t, the function inside the Tendsto of HasFlowExponent.

Main results

• Oseledets.Multifractal.cellMassFamily_sum_eq_one: the cell masses sum to 1 (genuine probabilities) — the non-vacuity of the interface.
• Oseledets.Multifractal.not_isHeterogeneous_iff_equalMeasure: ¬ IsHeterogeneous μ P iff all cell masses are equal — i.e. the equal-measure hypothesis of partitionFunction_equalMeasure / renyiDim_equalMeasure, the monofractal single-point spectrum that #16 characterizes.
• Oseledets.Multifractal.hasFlowExponent_iff_tendsto_finiteTimeFlowExponent: the finite-time estimator's atTop limit is HasFlowExponent (true by unfolding).
• Oseledets.Multifractal.RefiningLimitConvergesProp: the ε → 0 mesh-refinement convergence of the cell-mass family, stated (signature only) with a cross-reference to the #16 degenerate- uniform limit renyiDim_uniform_tendsto_dim; the general non-uniform refining limit stays #16's deferred content, so #18 does not re-request it.

N1 — flow-transported coarse-grained partition + cell-mass family

def Oseledets.Multifractal.dynamicalRefineCells {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (φ : MeasurePreservingFlow μ) (P : Entropy.MeasurePartition μ ι) (Δ : ℝ) (n : ℕ) (f : Fin n → ι) : Set X

The cell family of the depth-n flow-refined join: at an index f : Fin n → ι it is the intersection ⋂ₖ (φ (k • Δ))⁻¹ (P_{f k}) of the pullbacks of the chosen seed-cells P along the flow at the equally-spaced times 0, Δ, 2Δ, …, (n-1)Δ. This is the flow-transported analogue of Oseledets.Entropy.ksJoinCells, with the flow map φ (k • Δ) in place of the discrete iterate T^[k]; for n = 0 the empty intersection is the whole space.

Equations

• Oseledets.Multifractal.dynamicalRefineCells φ P Δ n f = ⋂ (k : Fin n), φ.toFun (↑k • Δ) ⁻¹' P.cells (f k)

noncomputable def Oseledets.Multifractal.dynamicalRefine {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (φ : MeasurePreservingFlow μ) (P : Entropy.MeasurePartition μ ι) (Δ : ℝ) (n : ℕ) : Entropy.MeasurePartition μ (Fin n → ι)

The depth-n flow-refined partition ⋁ₖ (φ (k • Δ))⁻¹ P, the join over the equally spaced flow times k • Δ (k = 0, …, n-1) of the pullbacks of a supplied seed partition P, indexed by Fin n → ι (the flat index discipline of Oseledets.Entropy.ksJoin). This is the flow-transported coarse-grained partition of issue #18; the seed P is supplied (not hardcoded), so the construction is abstract in the measurable space X. Each cell is a finite intersection of preimages of measurable cells under the measurable, measure-preserving flow maps φ (k • Δ); two distinct indices differ at some k, where the seed cells are almost-everywhere disjoint and the measure-preserving φ (k • Δ) keeps them a.e. disjoint after pullback; and the cells cover the space because at each coordinate k the point φ (k • Δ) x lies in some seed cell.

Equations

• Oseledets.Multifractal.dynamicalRefine φ P Δ n = { cells := Oseledets.Multifractal.dynamicalRefineCells φ P Δ n, measurable := ⋯, aedisjoint := ⋯, cover := ⋯ }

@[simp]

theorem Oseledets.Multifractal.dynamicalRefine_cells {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (φ : MeasurePreservingFlow μ) (P : Entropy.MeasurePartition μ ι) (Δ : ℝ) (n : ℕ) : (dynamicalRefine φ P Δ n).cells = dynamicalRefineCells φ P Δ n

noncomputable def Oseledets.Multifractal.cellMassFamily {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (P : Entropy.MeasurePartition μ ι) : ι → ℝ

The cell-mass family i ↦ (μ (P.cells i)).toReal of a finite measurable partition P. This ι → ℝ family is the entire #16 ↔ #18 interface: it is exactly the weight family consumed by Oseledets.Multifractal.partitionFunctionMeasure / renyiDimMeasure / renyiDimFlow. (So Z_q, τ(q), D_q, f(α) are not redefined here — they are the #16 functions on this family.)

Equations

• Oseledets.Multifractal.cellMassFamily P i = (μ (P.cells i)).toReal

@[simp]

theorem Oseledets.Multifractal.cellMassFamily_apply {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (P : Entropy.MeasurePartition μ ι) (i : ι) : cellMassFamily P i = (μ (P.cells i)).toReal

theorem Oseledets.Multifractal.cellMassFamily_sum_eq_one {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] [MeasureTheory.IsProbabilityMeasure μ] (P : Entropy.MeasurePartition μ ι) : ∑ i : ι, cellMassFamily P i = 1

Non-vacuity of the interface. The cell masses of a partition of a probability space are genuine probabilities summing to 1. A thin wrapper over Oseledets.Entropy.MeasurePartition.sum_toReal_measure_eq_one.

N4 — honest heterogeneity (non-uniform target)

def Oseledets.Multifractal.IsHeterogeneous {X : Type u_1} [MeasurableSpace X] {ι : Type u_2} [Fintype ι] (μ : MeasureTheory.Measure X) (P : Entropy.MeasurePartition μ ι) : Prop

Heterogeneity (non-uniformity) of a partition. IsHeterogeneous μ P holds when two cells carry distinct mass: ∃ i j, (μ (P.cells i)).toReal ≠ (μ (P.cells j)).toReal. This is a supplied hypothesis for the genuinely multifractal downstream of #18; it is false for a uniform (Haar / Lebesgue) measure, where all cells carry the same mass, so it is never asserted for an arbitrary μ. By not_isHeterogeneous_iff_equalMeasure, its failure is exactly the equal-measure hypothesis of the #16 monofractal degeneracy renyiDim_equalMeasure.

Equations

• Oseledets.Multifractal.IsHeterogeneous μ P = ∃ (i : ι) (j : ι), (μ (P.cells i)).toReal ≠ (μ (P.cells j)).toReal

theorem Oseledets.Multifractal.not_isHeterogeneous_iff_equalMeasure {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (P : Entropy.MeasurePartition μ ι) : ¬IsHeterogeneous μ P ↔ ∀ (i j : ι), (μ (P.cells i)).toReal = (μ (P.cells j)).toReal

Failure of heterogeneity is exactly the equal-measure hypothesis. ¬ IsHeterogeneous μ P holds iff all cell masses are equal, ∀ i j, (μ (P.cells i)).toReal = (μ (P.cells j)).toReal. This equal-mass condition is precisely the hypothesis of the #16 monofractal-degeneracy results Oseledets.Multifractal.partitionFunction_equalMeasure and renyiDim_equalMeasure (Oseledets/Multifractal/Degeneracy.lean): when it holds, the whole Rényi spectrum collapses to the single box-counting point log N / (-log ε). So the heterogeneity hypothesis is genuinely non-trivial — its negation is the single-point-spectrum monofractal case #16 characterizes.

N2b — finite-time observables (pre-limits, distinct from their asymptotic limits)

noncomputable def Oseledets.Multifractal.finiteTimePartitionEntropy {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (φ : MeasurePreservingFlow μ) (P : Entropy.MeasurePartition μ ι) (Δ : ℝ) (n : ℕ) : ℝ

The depth-n (finite-time) partition entropy of the flow-refined partition: the Shannon entropy H(⋁ₖ (φ (k • Δ))⁻¹ P) of the depth-n truncation dynamicalRefine φ P Δ n. This is the pre-limit observable, distinct from the Kolmogorov–Sinai (Fekete) limit ksEntropyPartition; the latter is the (1/n)-average limit of these as n → ∞.

Equations

• Oseledets.Multifractal.finiteTimePartitionEntropy φ P Δ n = Oseledets.Entropy.entropy μ (Oseledets.Multifractal.dynamicalRefine φ P Δ n).cells

@[simp]

theorem Oseledets.Multifractal.finiteTimePartitionEntropy_def {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Type u_2} [Fintype ι] (φ : MeasurePreservingFlow μ) (P : Entropy.MeasurePartition μ ι) (Δ : ℝ) (n : ℕ) : finiteTimePartitionEntropy φ P Δ n = Entropy.entropy μ (dynamicalRefine φ P Δ n).cells

noncomputable def Oseledets.Multifractal.finiteTimeFlowExponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (x : X) (s t : ℝ) : ℝ

The finite-time (pre-limit) flow Lyapunov estimator (FTLE) at a fixed finite flow time t: log ‖coverCocycle (x, s) t‖ / t, the function whose atTop limit defines Oseledets.HasFlowExponent. For each fixed t this is the finite-time exponent estimate; the asymptotic exponent L is its t → ∞ limit, related by hasFlowExponent_iff_tendsto_finiteTimeFlowExponent. This estimator is suspension-flow-specific (it reads the cover cocycle), the finite-time Lyapunov estimator the issue asks for.

Equations

• Oseledets.Multifractal.finiteTimeFlowExponent A T hτ hc hcpos x s t = Real.log ‖Oseledets.coverCocycle A T hτ hc hcpos (x, s) t‖ / t

theorem Oseledets.Multifractal.hasFlowExponent_iff_tendsto_finiteTimeFlowExponent {X : Type u_1} [MeasurableSpace X] {d : ℕ} (A : X → Matrix (Fin d) (Fin d) ℝ) (T : X ≃ᵐ X) {τ : X → ℝ} (hτ : Measurable τ) {c : ℝ} (hc : ∀ (x : X), c ≤ τ x) (hcpos : 0 < c) (q : SuspensionSpace T hτ) (x : X) (s : ℝ) (hmk : suspensionMk T hτ (x, s) = q) (L : ℝ) : Filter.Tendsto (fun (t : ℝ) => finiteTimeFlowExponent A T hτ hc hcpos x s t) Filter.atTop (nhds L) ↔ suspensionMk T hτ (x, s) = q ∧ Filter.Tendsto (fun (t : ℝ) => finiteTimeFlowExponent A T hτ hc hcpos x s t) Filter.atTop (nhds L)

The FTLE limit is the flow exponent. A growth rate L is HasFlowExponent-witnessed by a representative (x, s) of the orbit class q exactly when the finite-time estimator finiteTimeFlowExponent (x, s) · converges to L as the flow time t → ∞. This is true by unfolding: finiteTimeFlowExponent is defined to be the function inside the Tendsto of HasFlowExponent, so the right-hand Tendsto together with suspensionMk (x, s) = q is precisely the HasFlowExponent A T hτ hc hcpos q L witness carried by (x, s).

N3c — mesh-refinement convergence: statement + cross-reference to #16 (no proof)

The general ε → 0 mesh-refinement convergence of the cell-mass family (and hence of the Rényi dimension built on it) to the local-dimension spectrum is, for a genuinely multifractal (non-uniform) measure, the deferred research-grade content of issue #16, item 6 — it needs the Ledrappier–Young absolute continuity of conditional measures, the same Mathlib-absent ingredient blocking the Pesin–SRB work (issue #10); see the module docstring of Oseledets.Multifractal.RefiningLimit. So #18 does not re-request it: it records the convergence as a Prop-valued predicate with the honest cross-reference, and the one case that is provable — the degenerate uniform / monofractal case — is already discharged unconditionally by Oseledets.Multifractal.renyiDim_uniform_tendsto_dim (the Tendsto … (𝓝[Ioo 0 1] 0) limit), which this layer simply points at rather than duplicating.

def Oseledets.Multifractal.RefiningLimitConvergesProp {X : Type u_1} [MeasurableSpace X] {ι : ℝ → Type u_2} [(ε : ℝ) → Fintype (ι ε)] (μ : MeasureTheory.Measure X) (P : (ε : ℝ) → Entropy.MeasurePartition μ (ι ε)) (D : ℝ → ℝ) (q : ℝ) : Prop

Mesh-refinement convergence of the cell-mass spectrum (predicate, no proof). For a refining family of partitions P ε : MeasurePartition μ (ι ε) at scales ε ∈ (0, 1), the Rényi dimension renyiDimMeasure μ (P ε) ε q built on the cell-mass families cellMassFamily (P ε) converges, as ε → 0, to a limit dimension D q: Tendsto (fun ε => renyiDimMeasure μ (P ε) ε q) (𝓝[Set.Ioo 0 1] 0) (𝓝 (D q)).

This is stated only (as the Prop it asserts), with no proof, by design: the general non-uniform refining limit is the deferred content of issue #16, item 6 (the Ledrappier–Young / exact- dimensionality frontier; see Oseledets.Multifractal.RefiningLimit), so #18 does not re-request it. The degenerate uniform / monofractal case of this very convergence is already proved unconditionally as Oseledets.Multifractal.renyiDim_uniform_tendsto_dim (and its measure mirror renyiDimMeasure_uniform_eq_dim), where D q ≡ d is the constant box-counting dimension.

Equations

• Oseledets.Multifractal.RefiningLimitConvergesProp μ P D q = Filter.Tendsto (fun (ε : ℝ) => Oseledets.Multifractal.renyiDimMeasure μ (P ε) ε q) (nhdsWithin 0 (Set.Ioo 0 1)) (nhds (D q))

theorem Oseledets.Multifractal.refiningLimitConvergesProp_of_uniform {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : ℝ → Type u_2} [(ε : ℝ) → Fintype (ι ε)] [∀ (ε : ℝ), Nonempty (ι ε)] [MeasureTheory.IsProbabilityMeasure μ] (P : (ε : ℝ) → Entropy.MeasurePartition μ (ι ε)) {d : ℝ} (huniform : ∀ (ε : ℝ) (i : ι ε), (μ ((P ε).cells i)).toReal = (↑(Fintype.card (ι ε)))⁻¹) (hcard : ∀ ε ∈ Set.Ioo 0 1, ↑(Fintype.card (ι ε)) = ε ^ (-d)) (q : ℝ) : RefiningLimitConvergesProp μ P (fun (x : ℝ) => d) q

Discharge of the mesh-refinement convergence in the degenerate uniform case. When the refining family is uniform — each P ε has all cells of equal mass (Fintype.card (ι ε))⁻¹ with the d-dimensional dyadic-grid count Fintype.card (ι ε) = ε ^ (-d) — the mesh-refinement convergence predicate RefiningLimitConvergesProp holds with the constant limit D q ≡ d. This is exactly Oseledets.Multifractal.renyiDim_uniform_tendsto_dim transported to renyiDimMeasure via the cell-mass family, the only case of the general (deferred) refining limit provable unconditionally.