Assembly: joint measurability, the integral identity, and the

majorant integral (proof layer)

theorem CommutingRepetition.measurable_binIdx_pair (r : ℝ) {β : Type u_1} [MeasurableSpace β] {f g : β → ℝ} (hf : Measurable f) (hg : Measurable g) : Measurable fun (q : β) => binIdx r (f q) (g q)

Joint measurability of the bin index in the (shift, value) pair.

theorem CommutingRepetition.measurable_gridF_pair {r : ℝ} (hr : 1 < r) (L H : ℝ) : Measurable fun (q : ℝ × ℝ × ℝ) => gridF r q.1 L H q.2.1 q.2.2

Joint measurability of the disagreement integrand in the (shift, pair) variable.

theorem CommutingRepetition.gridGamma_eq_integral {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (hL : 0 < L) (θ : ℝ) (h1 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.1 ^ 2) ν) (h2 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.2 ^ 2) ν) : gridGamma ν r θ L H = ∫ (p : ℝ × ℝ), gridF r θ L H p.1 p.2 ∂ν

theorem CommutingRepetition.measurable_gridF_slice {r L H : ℝ} (hr : 1 < r) (θ : ℝ) : Measurable fun (p : ℝ × ℝ) => gridF r θ L H p.1 p.2

theorem CommutingRepetition.integral_gridF_eq_toReal {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (θ : ℝ) : ∫ (p : ℝ × ℝ), gridF r θ L H p.1 p.2 ∂ν = (∫⁻ (p : ℝ × ℝ), ENNReal.ofReal (gridF r θ L H p.1 p.2) ∂ν).toReal

theorem CommutingRepetition.integrable_gridF_slice {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (hL : 0 < L) (θ : ℝ) (h1 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.1 ^ 2) ν) (h2 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.2 ^ 2) ν) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => gridF r θ L H p.1 p.2) ν

Integrability of the fixed-shift disagreement integrand.

theorem CommutingRepetition.integrable_gridG {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {α L H : ℝ} (h1 : ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1) (h2 : ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => gridG α L H p.1 p.2) ν

Integrability of the scalar majorant.

theorem CommutingRepetition.integral_gridG_le {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {α L H ρ : ℝ} (hα0 : 0 < α) (hL : 0 < L) (hρ : 0 ≤ ρ) (hnn : ∀ᵐ (p : ℝ × ℝ) ∂ν, 0 ≤ p.1 ∧ 0 ≤ p.2) (h1 : ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1) (h2 : ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1) (ht1 : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.1}, p.1 ^ 2 ∂ν ≤ ρ) (ht2 : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.2}, p.2 ^ 2 ∂ν ≤ ρ) : ∫ (p : ℝ × ℝ), gridG α L H p.1 p.2 ∂ν ≤ 100 * (∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν + √(∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν) / α + ρ + L ^ 2)

The majorant integrates to the manuscript bound with C = 100.

theorem CommutingRepetition.setIntegral_gridGamma_le {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {α L H ρ : ℝ} (hα0 : 0 < α) (hα2 : α ≤ 1 / 2) (hL : 0 < L) (hρ : 0 ≤ ρ) (hnn : ∀ᵐ (p : ℝ × ℝ) ∂ν, 0 ≤ p.1 ∧ 0 ≤ p.2) (h1 : ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1) (h2 : ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1) (ht1 : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.1}, p.1 ^ 2 ∂ν ≤ ρ) (ht2 : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.2}, p.2 ^ 2 ∂ν ≤ ρ) : ∫ (θ : ℝ) in Set.Ico 0 1, gridGamma ν (1 + α) θ L H ≤ 100 * (∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν + √(∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν) / α + ρ + L ^ 2)

The θ-averaged disagreement bound (eq grid-disagreement, C = 100): swap the θ- and coupling-integrals by Tonelli, apply the pointwise θ-average master bound, and integrate the majorant.

theorem CommutingRepetition.measurable_gridGamma {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (hL : 0 < L) (h1 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.1 ^ 2) ν) (h2 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.2 ^ 2) ν) : Measurable fun (θ : ℝ) => gridGamma ν r θ L H

Shift-measurability of the disagreement functional.

theorem CommutingRepetition.gridGamma_nonneg {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (hL : 0 < L) (θ : ℝ) (h1 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.1 ^ 2) ν) (h2 : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => p.2 ^ 2) ν) : 0 ≤ gridGamma ν r θ L H

The disagreement functional is nonnegative.

theorem CommutingRepetition.gridGamma_le_two_sq {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r L H : ℝ} (hr : 1 < r) (hL : 0 < L) (θ : ℝ) (h1 : ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1) (h2 : ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1) : gridGamma ν r θ L H ≤ 2 * r ^ 2

Crude uniform bound: Γ_θ ≤ 2 r².

theorem CommutingRepetition.grid_disagreement : ∃ (C : ℝ), 0 < C ∧ ∀ (ν : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsProbabilityMeasure ν] (α L H ρ : ℝ), 0 < α → α ≤ 1 / 2 → 0 < L → L < H → 0 ≤ ρ → (∀ᵐ (p : ℝ × ℝ) ∂ν, 0 ≤ p.1 ∧ 0 ≤ p.2) → ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1 → ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1 → ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.1}, p.1 ^ 2 ∂ν ≤ ρ → ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.2}, p.2 ^ 2 ∂ν ≤ ρ → (∀ θ ∈ Set.Ico 0 1, 1 - ρ - L ^ 2 ≤ gridA ν (1 + α) θ L H ∧ gridA ν (1 + α) θ L H ≤ (1 + α) ^ 2 ∧ 1 - ρ - L ^ 2 ≤ gridB ν (1 + α) θ L H ∧ gridB ν (1 + α) θ L H ≤ (1 + α) ^ 2) ∧ ∫ (θ : ℝ) in Set.Ico 0 1, gridGamma ν (1 + α) θ L H ≤ C * (∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν + √(∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν) / α + ρ + L ^ 2)

Shifted-bin disagreement with cutoffs (node 1.3.3; 06_otqcs.tex, lem otqcs-grid, eqs ab-mass + grid-disagreement). Over an abstract coupling ν — probability measure on ℝ × ℝ, almost surely nonnegative coordinates, unit coordinate second moments (eq joint-moments), both high squared tails beyond H at most ρ — with ratio r = 1 + α, 0 < α ≤ 1/2, window 0 < L < H, and D = ∫ (a − b)² dν (= ‖h−k‖₂² at consumption, eq joint-moments): (i) for every shift θ ∈ [0,1) the retained rounded masses satisfy 1 − ρ − L² ≤ a_θ, b_θ ≤ r² (eq ab-mass); (ii) the average over θ ∼ Unif [0,1) of Γ_θ is at most C (D + √D / α + ρ + L²) for a universal numerical constant C (eq grid-disagreement).

theorem CommutingRepetition.exists_common_shift : ∃ (C : ℝ), 0 < C ∧ ∀ (ι : Type) [inst : Fintype ι] (π : ι → ℝ) (ν : ι → MeasureTheory.Measure (ℝ × ℝ)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (ν i)] (α L H ρ : ℝ), 0 < α → α ≤ 1 / 2 → 0 < L → L < H → 0 ≤ ρ → (∀ (i : ι), 0 ≤ π i) → ∑ i : ι, π i = 1 → (∀ (i : ι), ∀ᵐ (p : ℝ × ℝ) ∂ν i, 0 ≤ p.1 ∧ 0 ≤ p.2) → (∀ (i : ι), ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν i = 1) → (∀ (i : ι), ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν i = 1) → (∀ (i : ι), ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.1}, p.1 ^ 2 ∂ν i ≤ ρ) → (∀ (i : ι), ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.2}, p.2 ^ 2 ∂ν i ≤ ρ) → ∃ θ₀ ∈ Set.Ico 0 1, ∑ i : ι, π i * gridGamma (ν i) (1 + α) θ₀ L H ≤ C * (∑ i : ι, π i * ∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν i + √(∑ i : ι, π i * ∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂ν i) / α + ρ + L ^ 2)

Common shift selection (node 1.3.4; 06_otqcs.tex, eq common-shift): for a finite family of couplings satisfying the grid_disagreement hypotheses uniformly — one α, L, H and one tail bound ρ for every member — and a probability weight π on the family, there is one deterministic shift θ₀ ∈ [0,1) for which the π-average of Γ_{θ₀} is at most C (D̄ + √D̄ / α + ρ + L²), where D̄ is the π-average of the cross second moments (= E_π D_{st} at consumption). Average selection: no union bound, no division by π. Instantiated at the pair family ι = S × T.