The coarse-grained arrow, for an arbitrary finite coarse-graining

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #18 / R-019, brick (a).

#109 proved an H-theorem for one coarse-graining — the record string on Σ — and the proof used nothing about records beyond measurability into a finite type. This file is that proof with the vocabulary abstracted: a probability measure π on α, a finite β, a measurable q : α → β, and a π-preserving F : α → α.

• coarseLaw π q = π.map q — the coarse-grained law;
• coarseStep/coarseKernel — the induced macro dynamics: from a cell v, condition π on that cell, push forward by F, and read off the cell. Null cells get dirac, so the kernel is Markov on the nose (isMarkovKernel_coarseKernel);
• ★★★ comp_coarseLaw — one step of the macro dynamics is the pushforward along q ∘ F;
• ★★★ comp_coarseLaw_of_measurePreserving — invariance of the fine measure makes the coarse law stationary. Nothing is chosen: the reference law the divergence is measured from is the coarse-grained law itself;
• ★★★ antitone_klDiv_coarseLaw — the coarse-grained H-theorem. Along the induced macro dynamics, every macro law's relative entropy from the coarse-grained law is non-increasing.
• ★★ monotone_measureEntropy_coarseLaw — the entropy form, when the cells carry equal weight.

What this is and is not

⚠️ The arrow is for the induced macro chain, not for coarse-graining the fine orbit. The statement is that iterating coarseKernel decreases divergence from the stationary law. It is not that klDiv (coarseLaw (π.map F^[n]) q) (coarseLaw π q) decreases — for a measure-preserving F that quantity is constant, by the data-processing inequality in both directions, and no theorem can make it decrease. The Markov property is the content of the coarse-graining step, which is why coarseStep is a definition here and not a hypothesis.

⚠️ Monotone is not convergent. Nothing here says the divergence tends to 0, and nothing here depends on the geometry of the cells — the H-theorem holds for any finite measurable coarse-graining, however coarse or lopsided. A rate, and hence relaxation, is where the cell size enters, and that half of the fibre relaxation H-theorem is open (RESIDUE(R-019)).

References: KlDivArrow.lean (#109, klDiv_comp_le_of_stationary, Measure.compIterate), FiniteEntropy.lean (#110), RecordLayer/MacrostateArrow.lean (#109's record instance, which this generalises); specs/BACKLOG.md #18, #109, #110; specs/residues.tsv R-019.

The coarse-grained law and the induced dynamics

noncomputable def InformationTheory.coarseLaw {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (π : MeasureTheory.Measure α) (q : α → β) : MeasureTheory.Measure β

The coarse-grained law: the distribution of the cell index.

Equations

• InformationTheory.coarseLaw π q = MeasureTheory.Measure.map q π

theorem InformationTheory.coarseLaw_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (π : MeasureTheory.Measure α) {q : α → β} (hq : Measurable q) {s : Set β} (hs : MeasurableSet s) : (coarseLaw π q) s = π (q ⁻¹' s)

theorem InformationTheory.isProbabilityMeasure_coarseLaw {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (π : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure π] {q : α → β} : MeasureTheory.IsProbabilityMeasure (coarseLaw π q)

noncomputable def InformationTheory.coarseStep {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (π : MeasureTheory.Measure α) (q : α → β) (F : α → α) (v : β) : MeasureTheory.Measure β

One step of the induced macro dynamics. From cell v: condition on that cell, evolve by F, read the cell. A null cell is sent to dirac v, which keeps the kernel Markov without affecting any statement about coarseLaw.

Equations

• InformationTheory.coarseStep π q F v = if π (q ⁻¹' {v}) = 0 then MeasureTheory.Measure.dirac v else MeasureTheory.Measure.map (fun (x : α) => q (F x)) π[|q ⁻¹' {v}]

noncomputable def InformationTheory.coarseKernel {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] (π : MeasureTheory.Measure α) (q : α → β) (F : α → α) : ProbabilityTheory.Kernel β β

The induced macro kernel. Measurability is free: the cell type is finite and discrete.

Equations

• InformationTheory.coarseKernel π q F = { toFun := InformationTheory.coarseStep π q F, measurable' := ⋯ }

@[simp]

theorem InformationTheory.coarseKernel_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] (π : MeasureTheory.Measure α) (q : α → β) (F : α → α) (v : β) : (coarseKernel π q F) v = coarseStep π q F v

theorem InformationTheory.isMarkovKernel_coarseKernel {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] (π : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure π] {q : α → β} {F : α → α} : ProbabilityTheory.IsMarkovKernel (coarseKernel π q F)

theorem InformationTheory.coarseStep_apply_mul {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] (π : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure π] {q : α → β} (hq : Measurable q) {F : α → α} (hF : Measurable F) (v : β) (s : Set β) : π (q ⁻¹' {v}) * (coarseStep π q F v) s = π (q ⁻¹' {v} ∩ (fun (x : α) => q (F x)) ⁻¹' s)

★★ The weighted step is the joint measure. Multiplying one macro step by the weight of the cell it starts from clears the conditioning, leaving the fine measure of "now in v, next in s".

theorem InformationTheory.comp_coarseLaw {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] [Fintype β] (π : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure π] {q : α → β} (hq : Measurable q) {F : α → α} (hF : Measurable F) : (coarseLaw π q).bind ⇑(coarseKernel π q F) = MeasureTheory.Measure.map (fun (x : α) => q (F x)) π

★★★ One step of the induced macro dynamics is the pushforward along q ∘ F. The macro law evolves by the macro kernel exactly as the fine measure evolves by F and is then read: the conditional step loses nothing and adds nothing.

Invariance forces the reference law, and the arrow follows

theorem InformationTheory.comp_coarseLaw_of_measurePreserving {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] [Fintype β] (π : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure π] {q : α → β} (hq : Measurable q) {F : α → α} (hF : MeasureTheory.MeasurePreserving F π π) : (coarseLaw π q).bind ⇑(coarseKernel π q F) = coarseLaw π q

★★★ Invariance of the fine measure makes the coarse law stationary. This is what makes the arrow a theorem rather than a posit: the reference law the divergence is measured from is not chosen, it is the coarse-grained law itself, fixed by the invariance.

theorem InformationTheory.antitone_klDiv_coarseLaw {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] [Fintype β] (π : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure π] {q : α → β} (hq : Measurable q) {F : α → α} (hF : MeasureTheory.MeasurePreserving F π π) (μ : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] : Antitone fun (n : ℕ) => klDiv (μ.compIterate (coarseKernel π q F) n) (coarseLaw π q)

★★★ The coarse-grained H-theorem. Along the macro dynamics induced by a measure-preserving fine dynamics, every macro law's relative entropy from the coarse-grained law is non-increasing, and monotonically so in the number of steps.

No detailed balance, symmetry, double stochasticity or mixing is assumed, and no property of the cells: the only input is that the fine dynamics preserves the fine measure.

theorem InformationTheory.monotone_measureEntropy_coarseLaw {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [DiscreteMeasurableSpace β] [Fintype β] [Nonempty β] (π : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure π] {q : α → β} (hq : Measurable q) {F : α → α} (hF : MeasureTheory.MeasurePreserving F π π) (huniform : coarseLaw π q = ProbabilityTheory.uniformOn Set.univ) (μ : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] : Monotone fun (n : ℕ) => measureEntropy (μ.compIterate (coarseKernel π q F) n)

★★ The entropy form. If the cells carry equal weight — the coarse law is uniform — the coarse-grained Shannon entropy is non-decreasing along the induced dynamics, by #110.