The finite-horizon bound in relative-entropy form

Category: 7-SigmaLayer. BACKLOG #130, out of #118(ii).

FibreFiniteHorizon.lean (#118(ii)) proved the L² statement: at horizon T the mean-square deviation of a cell's time-averaged occupation from its Haar value is at most (2/T)·∑_{u<T} ε u, and summed over the (m+1)² cells it costs one factor (m+1)². R-019's second clause is phrased in relative entropy, and this file says the same thing in that vocabulary.

Two pieces, exactly as #130 priced them.

• The occupation law. horizonLaw m T p is the time-averaged occupation of the cells along the orbit of p out to T, as a Measure on the cells rather than a family of real numbers: the uniform average of the T Dirac masses at the cells visited. ★★ horizonLaw_real_apply identifies its mass at c with #118(ii)'s Birkhoff average, so the two files are talking about the same object; ★ isProbabilityMeasure_horizonLaw for T > 0, and ★ measurable_horizonLaw is the measurability in the base point #130 asked for.
• The divergence bound. ★★★ klDiv_horizonLaw_le_chiSq: the divergence of the occupation law from the uniform cell law is at most (m+1)² times the mean-square deviation of the occupations from 1/(m+1)², pointwise in the base point. With #118(ii) that is the relative-entropy reading of the finite-horizon bound, at the cost of one more factor (m+1)².

Honest scope

⚠️ The reference is the uniform cell law, and #118(ii)'s is the Haar cell law. The chi-squared inequality is proved against uniformOn univ (ChiSquare.lean), so the deviation below is measured from 1/(m+1)², while #118(ii) measures it from coarseLaw (kMuL p₀) (fibreCell m). These agree only if the Haar cell law is uniform, and nothing in this corpus proves that. It is true — the cells of circCell have equal width by construction — but the proof is a floor-and-endpoint computation on AddCircle 1 with the min m clamp and the (0, 1] representative to handle, and it is BACKLOG #144. Combining the bound below with #118(ii) therefore needs that identification, which is why no such combination is stated here: #130's own phrasing assumed it silently, and naming it is the honest form. What is proved below needs no such hypothesis.

⚠️ Still time-averaged, so still not R-019. Everything inherits #118(ii)'s scope: what equilibrates is a cell's time-averaged occupation, not the law at step n. The entropy vocabulary changes nothing about that, exactly as the row that wanted it recorded.

⚠️ (m+1)² on top of #118(ii)'s (m+1)². The chi-squared conversion costs one factor of the cell count, so in this vocabulary the bound degrades quartically in the fineness of the coarse-graining. R-019's "rate set by the cell size" is further away here than in the L² reading, not closer.

⚠️ The occupation law is not a limit object. horizonLaw m T p is a finite average over [0, T); nothing says it converges as T → ∞, and the T = 0 value is the zero measure.

References: FibreFiniteHorizon.lean (#118(ii), fibreCellInd, integral_sum_birkhoffAverage_fibreCellInd_sub_sq_le), FibreCoarseArrow.lean (fibreCell, fibreStroke, circCell), ChiSquare.lean (klDiv_uniformOn_univ_le_chiSq); specs/BACKLOG.md #130, #118, #144; specs/residues.tsv R-019.

The cell indicator as a test for one cell

theorem CSD.SigmaLayer.fibreCellInd_eq_ite {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (q : LF4.KSigma N) : fibreCellInd m c q = if fibreCell m q = c then 1 else 0

The cell indicator, as the test fibreCell p = c.

theorem CSD.SigmaLayer.fibreCellInd_nonneg {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (q : LF4.KSigma N) : 0 ≤ fibreCellInd m c q

The time-averaged occupation law of the cells

noncomputable def CSD.SigmaLayer.horizonLaw {N : ℕ} (m T : ℕ) (p : LF4.KSigma N) : MeasureTheory.Measure (Fin (m + 1) × Fin (m + 1))

The occupation law at horizon T: the uniform average of the Dirac masses at the cells the orbit of p visits over [0, T). This is #118(ii)'s family of Birkhoff averages assembled into a single measure on the cells, which is the form a divergence takes its argument in.

Equations

• CSD.SigmaLayer.horizonLaw m T p = (↑T)⁻¹ • ∑ u ∈ Finset.range T, MeasureTheory.Measure.dirac (CSD.SigmaLayer.fibreCell m (CSD.SigmaLayer.fibreStroke^[u] p))

theorem CSD.SigmaLayer.horizonLaw_real_apply {N : ℕ} (m T : ℕ) (p : LF4.KSigma N) (c : Fin (m + 1) × Fin (m + 1)) : (horizonLaw m T p).real {c} = birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p

★★ Its mass at a cell is #118(ii)'s Birkhoff average, so the two files are about one object.

theorem CSD.SigmaLayer.isProbabilityMeasure_horizonLaw {N : ℕ} (m T : ℕ) (p : LF4.KSigma N) (hT : 0 < T) : MeasureTheory.IsProbabilityMeasure (horizonLaw m T p)

★ It is a probability measure at a positive horizon.

theorem CSD.SigmaLayer.measurable_horizonLaw {N : ℕ} (m T : ℕ) : Measurable fun (p : LF4.KSigma N) => horizonLaw m T p

★ Measurable in the base point, which is what makes the divergence below a function of p that can be integrated.

The divergence bound

theorem CSD.SigmaLayer.klDiv_horizonLaw_le_chiSq {N : ℕ} (m T : ℕ) (p : LF4.KSigma N) (hT : 0 < T) : InformationTheory.klDiv (horizonLaw m T p) (ProbabilityTheory.uniformOn Set.univ) ≤ ENNReal.ofReal ((↑m + 1) ^ 2 * ∑ c : Fin (m + 1) × Fin (m + 1), (birkhoffAverage ℝ fibreStroke (fibreCellInd m c) T p - ((↑m + 1) ^ 2)⁻¹) ^ 2)

★★★ The finite-horizon bound in relative-entropy form.

The divergence of the time-averaged occupation law from the uniform cell law is at most (m+1)² times the mean-square deviation of the occupations from 1/(m+1)². This is the chi-squared inequality of ChiSquare.lean at the occupation law, and it is the conversion R-019's second clause asks for: an L² estimate on the occupations becomes an estimate on the divergence, at the cost of one factor of the cell count.