Affine transport between arcs of the record circle, and between rectangles of the fibre

Category: 7-SigmaLayer (the record layer — library-shaped, kept here because it is written in the record layer's own coordinate rep). BACKLOG #137; consumed by SkewReroute.lean.

An arc of the record circle is rep ⁻¹' Ioc x₀ (x₀ + w), and the affine map arcMap x₀ α λ : θ ↦ ⟨α + λ (rep θ − x₀)⟩ carries it onto the arc rep ⁻¹' Ioc α (α + λ w), stretching by λ. This file proves the transport law for Haar measure — ★ map_restrict_arcMap: the restriction of volume to the source arc pushes forward to λ⁻¹ times the restriction to the target arc — and its product on the fibre T² — ★★ map_restrict_rectMap: a map that stretches by λ₁ in θ₁ and by λ₂ in θ₂ with λ₁ λ₂ = 1 carries the restriction to a rectangle onto the restriction to the image rectangle exactly. With GluedMeasurePreserving.lean this is all a rectangle exchange needs.

Also here: existsUnique_mem_circleCell — for a probability vector the cells circleCell r i tile the circle exactly, every point in exactly one cell (the Born cells of CircleFibre.lean are a.e.-total there; the exact form is what a pointwise readout needs).

Honest scope

• The arcs are read in the representative rep ∈ (0, 1], so all arcs sit inside one turn; the wrap-around arc is not treated (none of the consumers' cells wrap).
• λ > 0 throughout: orientation-preserving transport only.

References: CircleFibre.lean (rep, circleCell, volume_rep_preimage), NullSeamGeneralN.lean (loSum_zero_val, loSum_succ_val, loSum_last_add), Mathlib AddCircle.measurePreserving_mk, Real.map_volume_mul_left; specs/BACKLOG.md #137.

Exact tiling by the cells of a probability vector

theorem CSD.RecordLayer.pos_of_mem_circleCell {k : ℕ} {r : Fin k → ℝ} {i : Fin k} {θ : CircleFibre} (hθ : θ ∈ circleCell r i) : 0 < r i

A point lies in a cell only if the cell has positive width.

theorem CSD.RecordLayer.existsUnique_mem_circleCell {k : ℕ} (r : Fin k → ℝ) (hr : ∀ (i : Fin k), 0 ≤ r i) (hsum : ∑ i : Fin k, r i = 1) (θ : CircleFibre) : ∃! i : Fin k, θ ∈ circleCell r i

★ The cells of a probability vector tile the circle exactly: every point lies in exactly one cell.

The affine map of an arc

noncomputable def CSD.RecordLayer.arcMap (x₀ α lam : ℝ) (θ : CircleFibre) : CircleFibre

The affine map of the record circle θ ↦ ⟨α + λ (rep θ − x₀)⟩: it carries the arc starting at x₀ to the arc starting at α, stretched by λ.

Equations

• CSD.RecordLayer.arcMap x₀ α lam θ = ↑(α + lam * (CSD.RecordLayer.rep θ - x₀))

theorem CSD.RecordLayer.measurable_coe_circleFibre : Measurable fun (x : ℝ) => ↑x

The quotient map ℝ → CircleFibre is measurable.

theorem CSD.RecordLayer.measurable_arcMap (x₀ α lam : ℝ) : Measurable (arcMap x₀ α lam)

theorem CSD.RecordLayer.arcMap_mem {x₀ α lam w : ℝ} (hlam : 0 < lam) (hα : 0 ≤ α) (hαw : α + lam * w ≤ 1) {θ : CircleFibre} (hθ : rep θ ∈ Set.Ioc x₀ (x₀ + w)) : rep (arcMap x₀ α lam θ) = α + lam * (rep θ - x₀) ∧ rep (arcMap x₀ α lam θ) ∈ Set.Ioc α (α + lam * w)

Pointwise transport: a point of the source arc lands in the target arc, at the affine image of its representative.

The transport law for Haar measure

theorem CSD.RecordLayer.map_rep_volume : MeasureTheory.Measure.map rep MeasureTheory.volume = MeasureTheory.volume.restrict (Set.Ioc 0 1)

Haar measure on the circle, read through rep, is Lebesgue measure on one turn.

theorem CSD.RecordLayer.map_coe_restrict_volume : MeasureTheory.Measure.map (fun (x : ℝ) => ↑x) (MeasureTheory.volume.restrict (Set.Ioc 0 1)) = MeasureTheory.volume

Lebesgue measure on one turn, pushed to the circle, is Haar measure.

theorem CSD.RecordLayer.map_rep_restrict_arc {a b : ℝ} (ha : 0 ≤ a) (hb : b ≤ 1) : MeasureTheory.Measure.map rep (MeasureTheory.volume.restrict (rep ⁻¹' Set.Ioc a b)) = MeasureTheory.volume.restrict (Set.Ioc a b)

The restriction of Haar measure to an arc, pushed to ℝ by rep, is Lebesgue measure on the corresponding interval.

theorem CSD.RecordLayer.map_coe_restrict_interval {a b : ℝ} (ha : 0 ≤ a) (hb : b ≤ 1) : MeasureTheory.Measure.map (fun (x : ℝ) => ↑x) (MeasureTheory.volume.restrict (Set.Ioc a b)) = MeasureTheory.volume.restrict (rep ⁻¹' Set.Ioc a b)

Lebesgue measure on an interval inside one turn, pushed to the circle, is Haar measure on the corresponding arc.

theorem CSD.RecordLayer.map_volume_affine {lam : ℝ} (hlam : 0 < lam) (c x₀ : ℝ) : MeasureTheory.Measure.map (fun (x : ℝ) => c + lam * (x - x₀)) MeasureTheory.volume = ENNReal.ofReal lam⁻¹ • MeasureTheory.volume

The affine map of the line scales Lebesgue measure by λ⁻¹.

theorem CSD.RecordLayer.preimage_affine_Ioc {lam : ℝ} (hlam : 0 < lam) (α x₀ w : ℝ) : (fun (x : ℝ) => α + lam * (x - x₀)) ⁻¹' Set.Ioc α (α + lam * w) = Set.Ioc x₀ (x₀ + w)

The affine map's preimage of the target interval is the source interval.

theorem CSD.RecordLayer.map_restrict_arcMap {x₀ α lam w : ℝ} (hx₀ : 0 ≤ x₀) (hxw : x₀ + w ≤ 1) (hlam : 0 < lam) (hα : 0 ≤ α) (hαw : α + lam * w ≤ 1) : MeasureTheory.Measure.map (arcMap x₀ α lam) (MeasureTheory.volume.restrict (rep ⁻¹' Set.Ioc x₀ (x₀ + w))) = ENNReal.ofReal lam⁻¹ • MeasureTheory.volume.restrict (rep ⁻¹' Set.Ioc α (α + lam * w))

★ The transport law for an arc. The restriction of Haar measure to the source arc pushes forward under arcMap to λ⁻¹ times the restriction to the target arc.

Rectangles of the fibre

noncomputable def CSD.RecordLayer.rectMap (x₀ α lam₁ y₀ β lam₂ : ℝ) : LF4.KTorus → LF4.KTorus

The affine map of a rectangle of the fibre: arcMap in each coordinate.

Equations

• CSD.RecordLayer.rectMap x₀ α lam₁ y₀ β lam₂ = Prod.map (CSD.RecordLayer.arcMap x₀ α lam₁) (CSD.RecordLayer.arcMap y₀ β lam₂)

theorem CSD.RecordLayer.measurable_rectMap (x₀ α lam₁ y₀ β lam₂ : ℝ) : Measurable (rectMap x₀ α lam₁ y₀ β lam₂)

theorem CSD.RecordLayer.map_restrict_rectMap {x₀ α lam₁ w y₀ β lam₂ h : ℝ} (hx₀ : 0 ≤ x₀) (hxw : x₀ + w ≤ 1) (hlam₁ : 0 < lam₁) (hα : 0 ≤ α) (hαw : α + lam₁ * w ≤ 1) (hy₀ : 0 ≤ y₀) (hyh : y₀ + h ≤ 1) (hlam₂ : 0 < lam₂) (hβ : 0 ≤ β) (hβh : β + lam₂ * h ≤ 1) (hjac : lam₁ * lam₂ = 1) : MeasureTheory.Measure.map (rectMap x₀ α lam₁ y₀ β lam₂) (MeasureTheory.volume.restrict ((rep ⁻¹' Set.Ioc x₀ (x₀ + w)) ×ˢ (rep ⁻¹' Set.Ioc y₀ (y₀ + h)))) = MeasureTheory.volume.restrict ((rep ⁻¹' Set.Ioc α (α + lam₁ * w)) ×ˢ (rep ⁻¹' Set.Ioc β (β + lam₂ * h)))

★★ The transport law for a rectangle, Jacobian one. Stretching by λ₁ in θ₁ and λ₂ in θ₂ with λ₁ λ₂ = 1 carries the restriction of volume to the source rectangle exactly onto the restriction to the target rectangle.