Effective stochasticity: when a coarse-grained deterministic orbit is approximately Markov

Category: 1-Mathlib. Nothing here mentions CSD; this is elementary measure theory about deterministic dynamics and a coarse-graining. BACKLOG #100.

A deterministic map Φ on a probability space, observed only through a finite coarse-graining C : Ω → X, produces a stochastic-looking process n ↦ C (Φ^[n] ω). This file says when that process is approximately Markov, and with what error.

The shape of the statement, and why it is not circular

The hypothesis and the conclusion are about different objects:

• MicroDecoupled μ C Φ ε is about the microstate: conditioning on the whole coarse history up to step n moves the law of the microstate at step n by at most ε, uniformly over measurable sets, compared with conditioning on the present coarse value alone. It is a property of the triple (μ, Φ, C);
• the conclusions are about the coarse process: its one-step transition probabilities, and its path probabilities.

Assuming instead that the coarse process forgets its history would be assuming the conclusion. That is the trap this file is written to avoid, and it is why the hypothesis quantifies over microstate events rather than coarse ones.

What is proved

• condProb — conditional probability as a real number, scale-invariant in μ and 0 on null conditions, with condProb_nonneg and condProb_le_one;
• coarseAt, coarseEvent, historyEvent — the coarse process, its one-step events and its cylinder events, the last defined by recursion so the path arguments are inductions;
• ★★ abs_condProb_coarseEvent_sub_le — the one-step Markov error is at most ε: the next coarse value's probability given the whole history differs from its probability given the present by at most ε. The coarse future event is a microstate event pulled back along Φ^[n], which is exactly the instance of the hypothesis it needs;
• ★ measure_historyEvent_toReal_eq_prod — the exact chain rule: a path probability is the initial probability times the product of its own conditionals, with no hypothesis beyond non-degeneracy;
• ★★★ abs_measure_historyEvent_sub_markov_le — the path probability factorises up to n · ε: replacing every history-conditional by the corresponding one-step transition probability costs at most n · ε in total. This is "approximately Markovian with an explicit error";
• ★ abs_prod_sub_prod_le_sum — the elementary product comparison the path bound runs on;
• ★★ condProb_coarseEvent_succ_of_autonomous — non-vacuity: when the coarse variable is autonomous (C ∘ Φ = T ∘ C) the transition probabilities are 0/1 indicators and the error is 0 with no hypothesis at all, so the bounds above are attainable;
• ★★ cex_not_microDecoupled — the hypothesis is load-bearing. A four-point rotation coarse-grained into two cells has P(C₂ = 1 ∣ C₁ = 0, C₀ = 0) = 1 but P(C₂ = 1 ∣ C₁ = 0) = 1/2, so its coarse process is not Markov and no ε < 1/2 is available for it. Without this the theorems above could have been vacuous.

Honest scope

⚠️ The decoupling is a hypothesis, and nothing here supplies it. No dynamics is shown to satisfy MicroDecoupled with a small ε. That is deliberate and is forced: for the finite unitary dynamics the CSD corpus cares about, mixing is unavailable in principle (not_hasCorrelationDecay_blockPop_of_unitary), so a statement of this kind can only be conditional — exactly as the corpus's ETH-conditional results are.

⚠️ It is not the corpus's HasCorrelationDecay. That predicate bounds the two-point correlation of a single scalar observable; a Markov error is about conditional laws. Neither implies the other and this file does not connect them.

⚠️ The error is additive in the number of steps and is not claimed uniform in n. n · ε is useless once n ≳ 1/ε: this bounds a finite horizon, and no stationary or infinite-horizon Markov approximation is claimed. Nothing here is an invariant-measure or convergence statement.

⚠️ The coarse-graining is a parameter. C is arbitrary measurable; no particular coarse-graining is singled out, and in particular nothing here identifies C with any macroscopic or spacetime projection. Picking C is a separate question that this file deliberately leaves open.

⚠️ No randomness is derived. The process is a deterministic orbit throughout; what is bounded is how far its coarse marginals sit from those of a Markov chain. In particular this is not a derivation of the Born rule, and it says nothing about where probabilities come from — only about how a deterministic orbit can look stochastic when observed coarsely.

⚠️ Non-degeneracy hypotheses are real. The chain rule and the path bound need the history events to have non-zero finite measure; on a null history the conditionals are 0 by convention and the statements are about nothing.

References

Mathlib/Dynamics/CorrelationDecay.lean (the two-point predicate this is not); specs/BACKLOG.md #100; specs/future-work.md.

The coarse process and its events

def MeasureTheory.coarseAt {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (n : ℕ) : Ω → X

The coarse value after n steps.

Equations

• MeasureTheory.coarseAt C Φ n ω = C (Φ^[n] ω)

@[simp]

theorem MeasureTheory.coarseAt_zero {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) : coarseAt C Φ 0 = C

def MeasureTheory.coarseEvent {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (n : ℕ) (x : X) : Set Ω

The event that the coarse process takes the value x after n steps.

Equations

• MeasureTheory.coarseEvent C Φ n x = MeasureTheory.coarseAt C Φ n ⁻¹' {x}

@[simp]

theorem MeasureTheory.mem_coarseEvent {Ω : Type u_1} {X : Type u_2} {C : Ω → X} {Φ : Ω → Ω} {n : ℕ} {x : X} {ω : Ω} : ω ∈ coarseEvent C Φ n x ↔ C (Φ^[n] ω) = x

theorem MeasureTheory.coarseEvent_succ_eq {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (n : ℕ) (x : X) : coarseEvent C Φ (n + 1) x = Φ^[n] ⁻¹' C ∘ Φ ⁻¹' {x}

A coarse future event is a microstate event pulled back along the flow. The bridge that lets a hypothesis about microstates speak about the coarse process.

def MeasureTheory.historyEvent {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) : ℕ → Set Ω

The cylinder event that the coarse process follows the history h for its first n + 1 values. Defined by recursion, so the path arguments below are plain inductions.

Equations

• MeasureTheory.historyEvent C Φ h 0 = MeasureTheory.coarseEvent C Φ 0 (h 0)
• MeasureTheory.historyEvent C Φ h n.succ = MeasureTheory.historyEvent C Φ h n ∩ MeasureTheory.coarseEvent C Φ (n + 1) (h (n + 1))

@[simp]

theorem MeasureTheory.historyEvent_zero {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) : historyEvent C Φ h 0 = coarseEvent C Φ 0 (h 0)

@[simp]

theorem MeasureTheory.historyEvent_succ {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) (n : ℕ) : historyEvent C Φ h (n + 1) = historyEvent C Φ h n ∩ coarseEvent C Φ (n + 1) (h (n + 1))

theorem MeasureTheory.historyEvent_subset_coarseEvent {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) (n : ℕ) : historyEvent C Φ h n ⊆ coarseEvent C Φ n (h n)

theorem MeasureTheory.historyEvent_antitone {Ω : Type u_1} {X : Type u_2} (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) (n : ℕ) : historyEvent C Φ h (n + 1) ⊆ historyEvent C Φ h n

theorem MeasureTheory.measurableSet_coarseEvent {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] [MeasurableSingletonClass X] {C : Ω → X} {Φ : Ω → Ω} (hC : Measurable C) (hΦ : Measurable Φ) (n : ℕ) (x : X) : MeasurableSet (coarseEvent C Φ n x)

Conditional probability as a real number

noncomputable def MeasureTheory.condProb {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) (H B : Set Ω) : ℝ

The conditional probability of B given H, as a real number: μ (H ∩ B) / μ H. Invariant under rescaling μ, and 0 when H is null or infinite, so no non-degeneracy hypothesis is needed to write it.

Equations

• MeasureTheory.condProb μ H B = (μ (H ∩ B)).toReal / (μ H).toReal

theorem MeasureTheory.condProb_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) (H B : Set Ω) : 0 ≤ condProb μ H B

theorem MeasureTheory.condProb_le_one {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) (H B : Set Ω) (hfin : μ H ≠ ⊤) : condProb μ H B ≤ 1

theorem MeasureTheory.condProb_mem_Icc {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) (H B : Set Ω) (hfin : μ H ≠ ⊤) : condProb μ H B ∈ Set.Icc 0 1

theorem MeasureTheory.condProb_mul_eq {Ω : Type u_1} [MeasurableSpace Ω] (μ : Measure Ω) {H : Set Ω} (B : Set Ω) (h0 : μ H ≠ 0) (hfin : μ H ≠ ⊤) : condProb μ H B * (μ H).toReal = (μ (H ∩ B)).toReal

On a condition of non-zero finite measure, condProb is the ratio it looks like.

The decoupling hypothesis

def MeasureTheory.MicroDecoupled {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] (μ : Measure Ω) (C : Ω → X) (Φ : Ω → Ω) (ε : ℝ) : Prop

Microscopic decoupling at strength ε. Conditioning on the whole coarse history up to step n, rather than on the present coarse value alone, moves the law of the microstate at step n by at most ε, uniformly over measurable sets.

⚠️ This is a property of (μ, Φ, C) and says nothing directly about the coarse process; assuming the coarse process forgets its history would be assuming the conclusions below.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.abs_condProb_coarseEvent_sub_le {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] [MeasurableSingletonClass X] {μ : Measure Ω} {C : Ω → X} {Φ : Ω → Ω} {ε : ℝ} (hC : Measurable C) (hΦ : Measurable Φ) (hdec : MicroDecoupled μ C Φ ε) (h : ℕ → X) (n : ℕ) (z : X) : |condProb μ (historyEvent C Φ h n) (coarseEvent C Φ (n + 1) z) - condProb μ (coarseEvent C Φ n (h n)) (coarseEvent C Φ (n + 1) z)| ≤ ε

★★ The one-step Markov error. Under microscopic decoupling, the probability that the coarse process takes the value z next differs by at most ε between conditioning on the whole history and conditioning on the present coarse value. The proof is the bridge coarseEvent_succ_eq: a coarse future event is a microstate event pulled back along the flow.

The exact chain rule

theorem MeasureTheory.measure_historyEvent_toReal_eq_prod {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] (μ : Measure Ω) (C : Ω → X) (Φ : Ω → Ω) (h : ℕ → X) (n : ℕ) : (∀ m ≤ n, μ (historyEvent C Φ h m) ≠ 0) → (∀ m ≤ n, μ (historyEvent C Φ h m) ≠ ⊤) → (μ (historyEvent C Φ h n)).toReal = (μ (historyEvent C Φ h 0)).toReal * ∏ m ∈ Finset.range n, condProb μ (historyEvent C Φ h m) (coarseEvent C Φ (m + 1) (h (m + 1)))

★ The chain rule for a coarse path probability, with no hypothesis beyond non-degeneracy of the prefixes: the path probability is the initial probability times the product of the path's own history-conditionals.

The path probability factorises, up to n · ε

theorem MeasureTheory.abs_prod_sub_prod_le_sum (a b : ℕ → ℝ) (n : ℕ) : (∀ m < n, a m ∈ Set.Icc 0 1) → (∀ m < n, b m ∈ Set.Icc 0 1) → |∏ m ∈ Finset.range n, a m - ∏ m ∈ Finset.range n, b m| ≤ ∑ m ∈ Finset.range n, |a m - b m|

★ The elementary product comparison: replacing each factor of a product of numbers in [0,1] costs at most the sum of the changes.

theorem MeasureTheory.abs_measure_historyEvent_sub_markov_le {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [MeasurableSpace X] [MeasurableSingletonClass X] {μ : Measure Ω} [IsProbabilityMeasure μ] {C : Ω → X} {Φ : Ω → Ω} {ε : ℝ} (hC : Measurable C) (hΦ : Measurable Φ) (hdec : MicroDecoupled μ C Φ ε) (h : ℕ → X) (n : ℕ) (h0 : ∀ m ≤ n, μ (historyEvent C Φ h m) ≠ 0) : |(μ (historyEvent C Φ h n)).toReal - (μ (historyEvent C Φ h 0)).toReal * ∏ m ∈ Finset.range n, condProb μ (coarseEvent C Φ m (h m)) (coarseEvent C Φ (m + 1) (h (m + 1)))| ≤ ↑n * ε

★★★ The coarse path probability factorises up to n · ε. Replacing every history-conditional by the one-step transition probability from the present coarse value changes the path probability by at most n · ε. This is "the coarse process is approximately Markovian with an explicit error", for a deterministic orbit and a hypothesis about microstates.

⚠️ Additive in n: useless once n ≳ 1/ε, and no infinite-horizon statement is implied.

Non-vacuity: an autonomous coarse variable is exactly Markov

theorem MeasureTheory.condProb_coarseEvent_succ_of_autonomous {Ω : Type u_1} {X : Type u_2} [MeasurableSpace Ω] [DecidableEq X] {μ : Measure Ω} {C : Ω → X} {Φ : Ω → Ω} {T : X → X} (hT : ∀ (ω : Ω), C (Φ ω) = T (C ω)) {H : Set Ω} (n : ℕ) (y z : X) (hH : H ⊆ coarseEvent C Φ n y) (h0 : μ H ≠ 0) (hfin : μ H ≠ ⊤) : condProb μ H (coarseEvent C Φ (n + 1) z) = if z = T y then 1 else 0

★★ With an autonomous coarse variable the error is zero, with no hypothesis. If C ∘ Φ factors through C then the next coarse value is determined by the present one, so every conditional transition probability is the same 0/1 indicator however much history is conditioned on. The bounds above are therefore attainable.

The hypothesis is load-bearing: a coarse process that is not Markov

def MeasureTheory.cexFlow : Fin 4 → Fin 4

The four-point rotation.

Equations

• MeasureTheory.cexFlow n = n + 1

def MeasureTheory.cexCoarse : Fin 4 → Fin 2

The two-cell coarse-graining of the four-point rotation.

Equations

• MeasureTheory.cexCoarse n = if ↑n < 2 then 0 else 1

theorem MeasureTheory.cexHistory_eq : historyEvent cexCoarse cexFlow (fun (x : ℕ) => 0) 1 = {0}

theorem MeasureTheory.cexPresent_eq : coarseEvent cexCoarse cexFlow 1 0 = {3, 0}

theorem MeasureTheory.cexFuture_eq : coarseEvent cexCoarse cexFlow 2 1 = {0, 1}

theorem MeasureTheory.cex_condProb_history : condProb Measure.count (historyEvent cexCoarse cexFlow (fun (x : ℕ) => 0) 1) (coarseEvent cexCoarse cexFlow 2 1) = 1

Given the history C₀ = 0, C₁ = 0, the next coarse value is 1 with certainty.

theorem MeasureTheory.cex_condProb_present : condProb Measure.count (coarseEvent cexCoarse cexFlow 1 0) (coarseEvent cexCoarse cexFlow 2 1) = 1 / 2

Given only the present value C₁ = 0, the next coarse value is 1 with probability 1/2.

theorem MeasureTheory.cex_not_microDecoupled {ε : ℝ} (hε : ε < 1 / 2) : ¬MicroDecoupled Measure.count cexCoarse cexFlow ε

★★ The hypothesis is load-bearing. The four-point rotation coarse-grained into two cells has a coarse process that is not Markov — the history changes the next step's probability from 1/2 to 1 — so no ε < 1/2 is available for it, and the theorems above are not vacuous.