Relaxation of a general L² fibre density

Category: 7-SigmaLayer. BACKLOG #147 (out of #118); R-019.

FibreCellDecay.lean proved R-019's convergence clause — the cell law after n strokes approaches the uniform cell law in relative entropy — for initial densities constant on the fibre cells, with a rate. This file removes the restriction on the density: for every L² density on the fibre, nonnegative and normalised, the cell law after n strokes converges to uniform, in relative entropy, ★★★ tendsto_klDiv_fibreStepLaw. No rate: the rate of a general density depends on the density, and the rate for coarse-grained densities is the earlier file's business.

The argument

Nothing is new on Σ: the stroke acts on the fibre with the base fixed (fibreStroke_iterate), the base carries mass 1 (integral_snd_kMuL), and a fibre cell is a set on T² (fibreCellInd_eq_torusCellInd_snd, definitional). So the weight a cell carries after n strokes is the correlation ∫ 1_{c'}(cat^n y) ϱ(y) dy on the torus (fibreStepWeight_eq), and Mathlib/Dynamics/CatMapStrongMixing.lean — the cat map is strongly mixing on L²(T²) — sends it to |c'| ∫ ϱ = (m+1)⁻² (★★★ tendsto_fibreStepWeight). Finitely many cells, so the chi-squared bound of ChiSquare.lean sends the relative entropy to zero.

The results

• ★★★ tendsto_integral_fibreStroke_iterate_mul_snd: the hyperbolic stroke is mixing on Σ for fibre observables: for f, g ∈ L²(T²), ∫ f((fibreStroke^n p).2) g(p.2) dμL → (∫ f)(∫ g).
• ★★★ tendsto_fibreStepWeight: for every ϱ ∈ L²(T²), the weight of every cell after n strokes tends to (m+1)⁻² ∫ ϱ.
• ★★★ tendsto_klDiv_fibreStepLaw: the relaxation H-theorem for a general L² fibre density: for ϱ ≥ 0 with ∫ ϱ = 1, the cell law after n strokes (fibreStepLaw, a probability measure on the cells, isProbabilityMeasure_fibreStepLaw) satisfies klDiv (fibreStepLaw n) (uniform) → 0. This is R-019's convergence clause with no condition on the initial density, for the hyperbolic fibre map.

Honest scope

• The map is the available hyperbolic witness, not a derived de-isolation dynamics, exactly as in FibreCellDecay.lean: catStroke is MovingFibreWitness.lean's cat map. That the physical de-isolation flow acts on the fibre by a hyperbolic map is Posit 1 (BACKLOG #19), and it is now the only thing R-019 is open on. The relaxation H-theorem for the fibre stays on the map identification. RESIDUE(R-019)
• Densities on the fibre coordinate. ϱ is a function of p.2. A density on Σ depending on the base coordinate too reduces to this by integrating out the base (its fibre marginal is in L² by Jensen, the base measure being a probability measure); that reduction is not written.
• No rate, by design. The rate for a general density depends on the decay of its Fourier coefficients; klDiv_stepLaw_le is the rate for the coarse-grained class.
• Unchanged: nothing here is about the translation kFlow, which relaxation_requires_hyperbolic_fibre shows cannot decorrelate; the typicality posits are untouched.

References: specs/BACKLOG.md #147, #118, #18, #19; specs/residues.tsv R-019; Mathlib/Dynamics/CatMapStrongMixing.lean; Mathlib/InformationTheory/ChiSquare.lean; SigmaLayer/FibreCellDecay.lean; SigmaLayer/FibreCellUniform.lean; SigmaLayer/MovingFibreWitness.lean.

The cell indicator, read on the fibre

noncomputable def CSD.SigmaLayer.torusCellInd (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (y : LF4.KTorus) : ℝ

The indicator of the cell c of the (m+1) × (m+1) grid, as a function on the fibre T².

Equations

• CSD.SigmaLayer.torusCellInd m c y = (CSD.SigmaLayer.torusCell m ⁻¹' {c}).indicator (fun (x : CSD.LF4.KTorus) => 1) y

theorem CSD.SigmaLayer.fibreCellInd_eq_torusCellInd_snd {N : ℕ} (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (p : LF4.KSigma N) : fibreCellInd m c p = torusCellInd m c p.2

The fibre cell indicator is the torus cell indicator of the fibre coordinate (definitional).

theorem CSD.SigmaLayer.measurable_torusCellInd (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : Measurable (torusCellInd m c)

theorem CSD.SigmaLayer.torusCellInd_nonneg (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (y : LF4.KTorus) : 0 ≤ torusCellInd m c y

theorem CSD.SigmaLayer.norm_torusCellInd_le (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (y : LF4.KTorus) : ‖torusCellInd m c y‖ ≤ 1

theorem CSD.SigmaLayer.memLp_two_torusCellInd (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : MeasureTheory.MemLp (torusCellInd m c) 2 MeasureTheory.volume

theorem CSD.SigmaLayer.torusCellInd_eq_ite (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) (y : LF4.KTorus) : torusCellInd m c y = if torusCell m y = c then 1 else 0

theorem CSD.SigmaLayer.sum_torusCellInd (m : ℕ) (y : LF4.KTorus) : ∑ c : Fin (m + 1) × Fin (m + 1), torusCellInd m c y = 1

Exactly one cell contains any point of the fibre.

theorem CSD.SigmaLayer.integral_torusCellInd {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (c : Fin (m + 1) × Fin (m + 1)) : ∫ (y : LF4.KTorus), torusCellInd m c y = ((↑m + 1) ^ 2)⁻¹

A cell has volume (m+1)⁻² on the fibre: #144's uniform coarse law, read on T² through the base (which is why a base point p₀ appears in a statement about the torus).

The hyperbolic stroke is mixing on Σ for fibre observables

theorem CSD.SigmaLayer.tendsto_integral_fibreStroke_iterate_mul_snd {N : ℕ} (p₀ : LF4.CPN N) {f g : LF4.KTorus → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (p : LF4.KSigma N), f (fibreStroke^[n] p).2 * g p.2 ∂LF4.kMuL p₀) Filter.atTop (nhds ((∫ (p : LF4.KSigma N), f p.2 ∂LF4.kMuL p₀) * ∫ (p : LF4.KSigma N), g p.2 ∂LF4.kMuL p₀))

★★★ Mixing of the hyperbolic stroke for fibre observables: for f, g ∈ L²(T²), the correlation ∫ f((fibreStroke^n p).2) g(p.2) dμL tends to the product of the means.

The step-n cell law of a general fibre density

noncomputable def CSD.SigmaLayer.fibreStepWeight {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (ϱ : LF4.KTorus → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : ℝ

The weight the cell c' carries after n strokes, for an initial density ϱ on the fibre: ∫ 1_{c'}(fibreStroke^n p) ϱ(p.2) dμL.

Equations

• CSD.SigmaLayer.fibreStepWeight p₀ m ϱ n c' = ∫ (p : CSD.LF4.KSigma N), CSD.SigmaLayer.fibreCellInd m c' (CSD.SigmaLayer.fibreStroke^[n] p) * ϱ p.2 ∂CSD.LF4.kMuL p₀

theorem CSD.SigmaLayer.fibreStepWeight_eq {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (ϱ : LF4.KTorus → ℝ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : fibreStepWeight p₀ m ϱ n c' = ∫ (y : LF4.KTorus), torusCellInd m c' (MeasureTheory.cat^[n] y) * ϱ y

The weight is a correlation on the fibre alone.

theorem CSD.SigmaLayer.tendsto_fibreStepWeight {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (hϱ : MeasureTheory.MemLp ϱ 2 MeasureTheory.volume) (c' : Fin (m + 1) × Fin (m + 1)) : Filter.Tendsto (fun (n : ℕ) => fibreStepWeight p₀ m ϱ n c') Filter.atTop (nhds (((↑m + 1) ^ 2)⁻¹ * ∫ (y : LF4.KTorus), ϱ y))

★★★ Relaxation of a general L² fibre density, cell by cell: the weight of every cell after n strokes tends to the uniform value (m+1)⁻² ∫ ϱ.

theorem CSD.SigmaLayer.integrable_torusCellInd_iterate_mul (m : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) (n : ℕ) {ϱ : LF4.KTorus → ℝ} (hϱ : MeasureTheory.MemLp ϱ 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : MeasureTheory.Torus2) => torusCellInd m c' (MeasureTheory.cat^[n] y) * ϱ y) MeasureTheory.volume

theorem CSD.SigmaLayer.fibreStepWeight_nonneg {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (h0 : 0 ≤ᵐ[MeasureTheory.volume] ϱ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : 0 ≤ fibreStepWeight p₀ m ϱ n c'

theorem CSD.SigmaLayer.sum_fibreStepWeight {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (hϱ : MeasureTheory.MemLp ϱ 2 MeasureTheory.volume) (n : ℕ) : ∑ c' : Fin (m + 1) × Fin (m + 1), fibreStepWeight p₀ m ϱ n c' = ∫ (y : LF4.KTorus), ϱ y

The step weights sum to the mass of the density.

noncomputable def CSD.SigmaLayer.fibreStepLaw {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) (ϱ : LF4.KTorus → ℝ) (n : ℕ) : MeasureTheory.Measure (Fin (m + 1) × Fin (m + 1))

The law at step n of the fibre density ϱ, as a measure on the cells.

Equations

• CSD.SigmaLayer.fibreStepLaw p₀ m ϱ n = ∑ c' : Fin (m + 1) × Fin (m + 1), ENNReal.ofReal (CSD.SigmaLayer.fibreStepWeight p₀ m ϱ n c') • MeasureTheory.Measure.dirac c'

theorem CSD.SigmaLayer.fibreStepLaw_real_apply {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (h0 : 0 ≤ᵐ[MeasureTheory.volume] ϱ) (n : ℕ) (c' : Fin (m + 1) × Fin (m + 1)) : (fibreStepLaw p₀ m ϱ n).real {c'} = fibreStepWeight p₀ m ϱ n c'

theorem CSD.SigmaLayer.isProbabilityMeasure_fibreStepLaw {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (hϱ : MeasureTheory.MemLp ϱ 2 MeasureTheory.volume) (h0 : 0 ≤ᵐ[MeasureTheory.volume] ϱ) (hnorm : ∫ (y : LF4.KTorus), ϱ y = 1) (n : ℕ) : MeasureTheory.IsProbabilityMeasure (fibreStepLaw p₀ m ϱ n)

The step law of a nonnegative density of mass 1 is a probability measure.

theorem CSD.SigmaLayer.tendsto_klDiv_fibreStepLaw {N : ℕ} (p₀ : LF4.CPN N) (m : ℕ) {ϱ : LF4.KTorus → ℝ} (hϱ : MeasureTheory.MemLp ϱ 2 MeasureTheory.volume) (h0 : 0 ≤ᵐ[MeasureTheory.volume] ϱ) (hnorm : ∫ (y : LF4.KTorus), ϱ y = 1) : Filter.Tendsto (fun (n : ℕ) => InformationTheory.klDiv (fibreStepLaw p₀ m ϱ n) (ProbabilityTheory.uniformOn Set.univ)) Filter.atTop (nhds 0)

★★★ The relaxation H-theorem for a general L² fibre density (R-019's convergence clause, with no condition on the initial density): for ϱ ∈ L²(T²) nonnegative with ∫ ϱ = 1, the relative entropy of the step-n cell law with respect to the uniform cell law tends to zero.