The Haar cell law of the fibre grid is uniform

Category: 7-SigmaLayer. BACKLOG #144, out of #130.

FibreCoarseArrow.lean cuts the T² fibre into (m+1)² cells of equal width, FibreFiniteHorizon.lean measures a cell's time-averaged occupation against its Haar weight, and FibreHorizonDivergence.lean compares the occupation law with the uniform cell law. All three say the weights are equal, because the construction makes them so, and none of them proved it. This file does.

• ★★★ volume_circCell_preimage — one circle cell has Haar measure 1/(m+1);
• ★★★ volume_torusCell_preimage — one fibre cell has 1/(m+1)², by the product measure;
• ★★★ coarseLaw_fibreCell_apply — so the Haar cell law of Σ gives every cell 1/(m+1)², and ★★ coarseLaw_fibreCell_toReal is the real-valued form the rate arguments consume.

How it goes, and why it is one argument rather than three

circCell m x is min m ⌊(m+1)·circRep x⌋₊, and circRep carries Haar measure on AddCircle 1 to Lebesgue measure on (0, 1], so a cell's weight is the Lebesgue measure of {t ∈ (0, 1] | min m ⌊(m+1)t⌋₊ = k}. The obvious plan is three cases — k = 0 loses its left endpoint to (0, 1], 0 < k < m is a clean half-open interval, and k = m absorbs t = 1 through the min clamp — and each case is a different interval, which is what made this look like M of endpoint bookkeeping.

It is one case instead. The set is sandwiched between Ioo (k/(m+1)) ((k+1)/(m+1)) and the corresponding Icc, uniformly in k, and those two have the same Lebesgue measure, so measure_mono in both directions pins the cell without ever naming which interval it is. The endpoints never have to be decided, only bounded. cellSet_inter_subset_Icc still splits on k < m against k = m, because the clamp genuinely behaves differently there, but each half is three lines and the k = 0 case has vanished entirely.

The general machinery this needs is ★★ RecordLayer.volume_rep_preimage — the rep-preimage of any measurable set weighs what the set weighs inside one turn — extracted here from the Ioc form that already existed, because a floor cell is half-open the other way round and the Ioc form cannot see it.

Honest scope

⚠️ This is the Haar cell law, not the occupation law. It says the reference measure spreads evenly over the cells. It says nothing about where a trajectory spends its time, which is #118's question and still carries #118(i)'s unproved decorrelation hypothesis.

⚠️ It unblocks a rate, and the rate is still time-averaged. With this, #130's divergence bound and #118(ii)'s L² bound are about the same reference and can be combined; the result is still a statement about time averages over [0, T), not about the law at step n, so R-019 is no closer than #118 left it.

⚠️ The grid only. circCell is the equal-width grid of FibreCoarseArrow.lean. Nothing here is stated for the Born cells of RecordLayer/CircleFibre.lean, whose widths are the Born weights and are deliberately not equal.

References: FibreCoarseArrow.lean (circRep, circIdx, circCell, torusCell, fibreCell), CircleFibre.lean (rep, volume_rep_preimage), FibreHorizonDivergence.lean (#130), FibreFiniteHorizon.lean (#118(ii)); specs/BACKLOG.md #144, #130, #118; specs/residues.tsv R-019.

The representatives of one cell, as a set of reals

def CSD.SigmaLayer.cellSet (m k : ℕ) : Set ℝ

The representatives that land in cell k: the grid condition, read on ℝ.

Equations

• CSD.SigmaLayer.cellSet m k = {t : ℝ | min m ⌊(↑m + 1) * t⌋₊ = k}

theorem CSD.SigmaLayer.measurableSet_cellSet (m k : ℕ) : MeasurableSet (cellSet m k)

theorem CSD.SigmaLayer.circRep_eq_rep : circRep = RecordLayer.rep

circRep is RecordLayer.rep: the two files took the measurable equivalence and the plain one, and the measurable one's toEquiv is the plain one.

theorem CSD.SigmaLayer.circCell_preimage (m : ℕ) (k : Fin (m + 1)) : circCell m ⁻¹' {k} = RecordLayer.rep ⁻¹' cellSet m ↑k

A cell of the circle is the rep-preimage of its grid condition.

The sandwich

theorem CSD.SigmaLayer.Ioo_subset_cellSet_inter (m : ℕ) (k : Fin (m + 1)) : Set.Ioo (↑↑k / (↑m + 1)) ((↑↑k + 1) / (↑m + 1)) ⊆ cellSet m ↑k ∩ Set.Ioc 0 1

The open interval of width 1/(m+1) sits inside the cell.

theorem CSD.SigmaLayer.cellSet_inter_subset_Icc (m : ℕ) (k : Fin (m + 1)) : cellSet m ↑k ∩ Set.Ioc 0 1 ⊆ Set.Icc (↑↑k / (↑m + 1)) ((↑↑k + 1) / (↑m + 1))

And the cell sits inside the closed interval of the same width. This is the half where the min clamp matters: at k = m the cell absorbs everything above m/(m+1), which is still inside the closed interval because the representatives stop at 1.

The weights

theorem CSD.SigmaLayer.volume_circCell_preimage (m : ℕ) (k : Fin (m + 1)) : MeasureTheory.volume (circCell m ⁻¹' {k}) = ENNReal.ofReal (↑m + 1)⁻¹

★★★ A circle cell has Haar measure 1/(m+1). Pinned by measure_mono between the open and closed intervals of that width, so no endpoint has to be decided.

theorem CSD.SigmaLayer.volume_torusCell_preimage (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : MeasureTheory.volume (torusCell m ⁻¹' {c}) = ENNReal.ofReal ((↑m + 1) ^ 2)⁻¹

★★★ A fibre cell has Haar measure 1/(m+1)²: the fibre is a product of two circles and so is its grid.

theorem CSD.SigmaLayer.coarseLaw_fibreCell_apply {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : (InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c} = ENNReal.ofReal ((↑m + 1) ^ 2)⁻¹

★★★ The Haar cell law of Σ is uniform: every one of the (m+1)² cells carries 1/(m+1)². This is the statement #130's bound and #118(ii)'s both assumed.

theorem CSD.SigmaLayer.coarseLaw_fibreCell_toReal {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : ((InformationTheory.coarseLaw (LF4.kMuL p₀) (fibreCell m)) {c}).toReal = ((↑m + 1) ^ 2)⁻¹

★★ The real-valued form, which is what the rate arguments consume.

The rate R-019's second clause asks for

With the reference identified, #130's pointwise divergence bound and #118(ii)'s L² bound are about the same quantity and compose. The two ingredients the composition needs beyond them are the measurability and boundedness of a cell's time-averaged occupation, which is what makes the integrand integrable.

theorem CSD.SigmaLayer.measurable_birkhoffAverage_fibreCellInd {N : ℕ} (m T : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : Measurable fun (p : LF4.KSigma N) => birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p

A cell's time-averaged occupation is measurable in the base point.

theorem CSD.SigmaLayer.birkhoffAverage_fibreCellInd_mem_Icc {N : ℕ} (m T : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (p : LF4.KSigma N) : birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p ∈ Set.Icc 0 1

And it lies in [0, 1], being an average of indicators.

theorem CSD.SigmaLayer.integrable_birkhoffAverage_sub_sq {N : ℕ} (p₀ : LF4.CPN N) (m T : ℕ) (c : Fin (m + 1) × Fin (m + 1)) {q : ℝ} (hq : q ∈ Set.Icc 0 1) : MeasureTheory.Integrable (fun (p : LF4.KSigma N) => (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - q) ^ 2) (LF4.kMuL p₀)

The squared deviation of an occupation from a weight in [0, 1] is integrable: it is measurable and bounded by 1.

theorem CSD.SigmaLayer.lintegral_klDiv_horizonLaw_le {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ε : ℕ → ℝ} {T : ℕ} (hdec : ∀ (c : Fin (m + 1) × Fin (m + 1)), MeasureTheory.HasCorrelationDecayUpTo (LF4.kMuL p₀) fibreStroke (fibreCellInd m c) ε T) (hT : 0 < T) : ∫⁻ (p : LF4.KSigma N), InformationTheory.klDiv (horizonLaw m T p) (ProbabilityTheory.uniformOn Set.univ) ∂LF4.kMuL p₀ ≤ ENNReal.ofReal ((↑m + 1) ^ 2 * ((↑m + 1) ^ 2 * (2 * (↑T)⁻¹ * ∑ u ∈ Finset.range T, ε u)))

★★★ R-019's second clause at a finite horizon, with its rate.

The divergence of the time-averaged occupation law from the cell law is, in expectation over the epistemic measure, at most (m+1)⁴·(2/T)·∑_{u<T} ε u. One factor (m+1)² is #118(ii)'s cell count and the other is the chi-squared conversion of #130, and the reference is the same on both sides because of coarseLaw_fibreCell_apply above — which is the whole reason this row existed.

⚠️ Still time-averaged: what equilibrates is a cell's occupation over [0, T), not the law at step n. And hdec is #118(i), unproved.