noncomputable def CommutingRepetition.binIdx (r θ a : ℝ) : ℤ

Bin index of a on the shifted logarithmic grid with ratio r and shift θ: for 1 < r and 0 < a, binIdx r θ a = j exactly when a ∈ I_j^θ = [r^(j+θ), r^(j+1+θ)). Junk value at a ≤ 0 (the log is junk there), harmless: every consumer guards by the retained window [L, H] with 0 < L. [06_otqcs.tex, eq shifted-bins]

Equations

• CommutingRepetition.binIdx r θ a = ⌊Real.log a / Real.log r - θ⌋

noncomputable def CommutingRepetition.roundVal (r θ a : ℝ) : ℝ

The upper endpoint t_j^θ = r^(j+1+θ) of the shifted bin containing a — the upward-rounded value of a (real exponent, Real.rpow). [06_otqcs.tex, eq shifted-bins]

Equations

• CommutingRepetition.roundVal r θ a = r ^ (↑(CommutingRepetition.binIdx r θ a) + 1 + θ)

noncomputable def CommutingRepetition.roundSq (r θ L H a : ℝ) : ℝ

Retained rounded square: the integrand realizing a_θ(h) (and b_θ(k)) against the spectral distribution — (t_j^θ)² on the bin of a when a lies in the retained window [L, H], zero otherwise, so that ∑_j (t_j^θ)² τ(1_{I_j^θ ∩ [L,H]}(h)) = ∫ roundSq r θ L H a dμ(a). [06_otqcs.tex, eq abcGamma, first two lines]

Equations

• CommutingRepetition.roundSq r θ L H a = if a ∈ Set.Icc L H then CommutingRepetition.roundVal r θ a ^ 2 else 0

noncomputable def CommutingRepetition.jointRoundSq (r θ L H a b : ℝ) : ℝ

Same-bin retained joint rounded square: the integrand realizing c_θ(h,k) against the joint spectral measure — (t_j^θ)² when both coordinates land in the same shifted bin and both are retained, zero otherwise. [06_otqcs.tex, eq abcGamma, third line]

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CommutingRepetition.gridA (ν : MeasureTheory.Measure (ℝ × ℝ)) (r θ L H : ℝ) : ℝ

a_θ of eq abcGamma, read through the coupling: the retained rounded squared mass of the first coordinate.

Equations

• CommutingRepetition.gridA ν r θ L H = ∫ (p : ℝ × ℝ), CommutingRepetition.roundSq r θ L H p.1 ∂ν

noncomputable def CommutingRepetition.gridB (ν : MeasureTheory.Measure (ℝ × ℝ)) (r θ L H : ℝ) : ℝ

b_θ of eq abcGamma: the retained rounded squared mass of the second coordinate.

Equations

• CommutingRepetition.gridB ν r θ L H = ∫ (p : ℝ × ℝ), CommutingRepetition.roundSq r θ L H p.2 ∂ν

noncomputable def CommutingRepetition.gridC (ν : MeasureTheory.Measure (ℝ × ℝ)) (r θ L H : ℝ) : ℝ

c_θ of eq abcGamma: the same-bin retained joint rounded mass.

Equations

• CommutingRepetition.gridC ν r θ L H = ∫ (p : ℝ × ℝ), CommutingRepetition.jointRoundSq r θ L H p.1 p.2 ∂ν

noncomputable def CommutingRepetition.gridGamma (ν : MeasureTheory.Measure (ℝ × ℝ)) (r θ L H : ℝ) : ℝ

Γ_θ = a_θ + b_θ − 2 c_θ of eq abcGamma: the grid disagreement functional.

Equations

• CommutingRepetition.gridGamma ν r θ L H = CommutingRepetition.gridA ν r θ L H + CommutingRepetition.gridB ν r θ L H - 2 * CommutingRepetition.gridC ν r θ L H

Bin geometry (proof layer)

theorem CommutingRepetition.binIdx_eq_iff {r θ a : ℝ} (hr : 1 < r) (ha : 0 < a) {j : ℤ} : binIdx r θ a = j ↔ r ^ (↑j + θ) ≤ a ∧ a < r ^ (↑j + 1 + θ)

Characterization of the bin index for positive arguments.

theorem CommutingRepetition.le_roundVal {r θ a : ℝ} (hr : 1 < r) (ha : 0 < a) : a ≤ roundVal r θ a

theorem CommutingRepetition.roundVal_le {r θ a : ℝ} (hr : 1 < r) (ha : 0 < a) : roundVal r θ a ≤ r * a

theorem CommutingRepetition.roundVal_pos {r θ a : ℝ} (hr : 1 < r) : 0 < roundVal r θ a

theorem CommutingRepetition.roundSq_nonneg {r θ a L H : ℝ} : 0 ≤ roundSq r θ L H a

theorem CommutingRepetition.jointRoundSq_nonneg {r θ a L H b : ℝ} : 0 ≤ jointRoundSq r θ L H a b

theorem CommutingRepetition.roundSq_bounds {r θ a : ℝ} (hr : 1 < r) {L H : ℝ} (hL : 0 < L) (hmem : a ∈ Set.Icc L H) : a ^ 2 ≤ roundSq r θ L H a ∧ roundSq r θ L H a ≤ r ^ 2 * a ^ 2

On the retained window, the rounded square is between a² and r² a².

theorem CommutingRepetition.roundSq_of_notMem {r θ a L H : ℝ} (hmem : a ∉ Set.Icc L H) : roundSq r θ L H a = 0

theorem CommutingRepetition.jointRoundSq_le_left {r θ a L H b : ℝ} : jointRoundSq r θ L H a b ≤ roundSq r θ L H a

The joint rounded square is dominated by each slot's rounded square (roundVal factors through binIdx).

theorem CommutingRepetition.jointRoundSq_le_right {r θ a L H b : ℝ} : jointRoundSq r θ L H a b ≤ roundSq r θ L H b

Measurability (proof layer)

theorem CommutingRepetition.measurableSet_binIdx_fiber (r θ : ℝ) (j : ℤ) : MeasurableSet (binIdx r θ ⁻¹' {j})

theorem CommutingRepetition.measurable_binIdx (r θ : ℝ) : Measurable (binIdx r θ)

theorem CommutingRepetition.measurable_comp_binIdx (r θ : ℝ) (g : ℤ → ℝ) : Measurable fun (a : ℝ) => g (binIdx r θ a)

Any function out of the (discrete) bin index is measurable, so any real function factoring through it is.

theorem CommutingRepetition.measurable_roundVal (r θ : ℝ) : Measurable (roundVal r θ)

theorem CommutingRepetition.roundSq_eq_mul_indicator {r θ L H : ℝ} (a : ℝ) : roundSq r θ L H a = roundVal r θ a ^ 2 * (Set.Icc L H).indicator 1 a

theorem CommutingRepetition.measurable_roundSq (r θ L H : ℝ) : Measurable (roundSq r θ L H)

theorem CommutingRepetition.measurableSet_sameBin (r θ : ℝ) : MeasurableSet {p : ℝ × ℝ | binIdx r θ p.1 = binIdx r θ p.2}

theorem CommutingRepetition.jointRoundSq_eq_mul_indicator {r θ L H : ℝ} (p : ℝ × ℝ) : jointRoundSq r θ L H p.1 p.2 = roundSq r θ L H p.1 * {q : ℝ × ℝ | binIdx r θ q.1 = binIdx r θ q.2}.indicator 1 p * (Set.Icc L H).indicator 1 p.2

theorem CommutingRepetition.measurable_jointRoundSq (r θ L H : ℝ) : Measurable fun (p : ℝ × ℝ) => jointRoundSq r θ L H p.1 p.2

Integrability and the fixed-shift mass bounds (proof layer)

theorem CommutingRepetition.roundSq_le_sq {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (a : ℝ) : roundSq r θ L H a ≤ r ^ 2 * a ^ 2

theorem CommutingRepetition.integrable_of_integral_eq_one {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {f : ℝ × ℝ → ℝ} (h : ∫ (p : ℝ × ℝ), f p ∂ν = 1) : MeasureTheory.Integrable f ν

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

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

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

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

Upper half of eq ab-mass for the first coordinate.

theorem CommutingRepetition.gridA_ge {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r θ L H ρ : ℝ} (hr : 1 < r) (hL : 0 < L) (hLH : L < H) (hnn : ∀ᵐ (p : ℝ × ℝ) ∂ν, 0 ≤ p.1 ∧ 0 ≤ p.2) (h1 : ∫ (p : ℝ × ℝ), p.1 ^ 2 ∂ν = 1) (htail : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.1}, p.1 ^ 2 ∂ν ≤ ρ) : 1 - ρ - L ^ 2 ≤ gridA ν r θ L H

Lower half of eq ab-mass for the first coordinate.

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

Upper half of eq ab-mass for the second coordinate.

theorem CommutingRepetition.gridB_ge {ν : MeasureTheory.Measure (ℝ × ℝ)} [MeasureTheory.IsProbabilityMeasure ν] {r θ L H ρ : ℝ} (hr : 1 < r) (hL : 0 < L) (hLH : L < H) (hnn : ∀ᵐ (p : ℝ × ℝ) ∂ν, 0 ≤ p.1 ∧ 0 ≤ p.2) (h2 : ∫ (p : ℝ × ℝ), p.2 ^ 2 ∂ν = 1) (htail : ∫ (p : ℝ × ℝ) in {q : ℝ × ℝ | H < q.2}, p.2 ^ 2 ∂ν ≤ ρ) : 1 - ρ - L ^ 2 ≤ gridB ν r θ L H

Lower half of eq ab-mass for the second coordinate.

The separation probability (proof layer; eq

separation-probability via a two-interval cover)

theorem CommutingRepetition.volume_sep_le {u v : ℝ} (huv : u ≤ v) : MeasureTheory.volume {θ : ℝ | θ ∈ Set.Ico 0 1 ∧ ⌊u - θ⌋ ≠ ⌊v - θ⌋} ≤ ENNReal.ofReal (2 * (v - u))

A uniformly shifted unit grid separates two reals with probability at most twice their distance (eq separation-probability, weakened by a factor of 2 — absorbed by the universal constant): every separating shift lies in one of two translates of Ioc u v.

The pointwise θ-averaged disagreement bound (proof layer)

noncomputable def CommutingRepetition.gridF (r θ L H a b : ℝ) : ℝ

The disagreement integrand.

Equations

• CommutingRepetition.gridF r θ L H a b = CommutingRepetition.roundSq r θ L H a + CommutingRepetition.roundSq r θ L H b - 2 * CommutingRepetition.jointRoundSq r θ L H a b

theorem CommutingRepetition.gridF_nonneg {r L H a b : ℝ} (θ : ℝ) : 0 ≤ gridF r θ L H a b

theorem CommutingRepetition.gridF_of_notMem_notMem {r L H a b : ℝ} (θ : ℝ) (haw : a ∉ Set.Icc L H) (hbw : b ∉ Set.Icc L H) : gridF r θ L H a b = 0

Both coordinates off the window: the integrand vanishes.

theorem CommutingRepetition.gridF_of_mem_notMem {r L H a b : ℝ} (θ : ℝ) (hbw : b ∉ Set.Icc L H) : gridF r θ L H a b = roundSq r θ L H a

One coordinate off the window: the integrand is the other slot's rounded square.

theorem CommutingRepetition.gridF_of_notMem_mem {r L H a b : ℝ} (θ : ℝ) (haw : a ∉ Set.Icc L H) : gridF r θ L H a b = roundSq r θ L H b

theorem CommutingRepetition.gridF_of_mem_mem {r L H a b : ℝ} (hr1 : 1 < r) (hr2 : r ≤ 2) (hL : 0 < L) (θ : ℝ) (haw : a ∈ Set.Icc L H) (hbw : b ∈ Set.Icc L H) : gridF r θ L H a b ≤ {θ' : ℝ | binIdx r θ' a ≠ binIdx r θ' b}.indicator (fun (x : ℝ) => 4 * (a ^ 2 + b ^ 2)) θ

Both on the window: the integrand is bounded by 4(a² + b²) and vanishes off the separation event.

The scalar majorant and the θ-averaged bound (proof layer)

noncomputable def CommutingRepetition.gridG (α L H a b : ℝ) : ℝ

The scalar majorant of the θ-averaged disagreement integrand.

Equations

• CommutingRepetition.gridG α L H a b = 32 * (a - b) ^ 2 + 48 / α * (max a b * |a - b|) + 8 * ((if H < a then a ^ 2 else 0) + if H < b then b ^ 2 else 0) + 16 * L ^ 2

theorem CommutingRepetition.gridG_nonneg {α L H a b : ℝ} (hα0 : 0 < α) (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ gridG α L H a b

theorem CommutingRepetition.gridF_comm {r L H a b : ℝ} (θ : ℝ) : gridF r θ L H a b = gridF r θ L H b a

theorem CommutingRepetition.gridG_comm {α L H a b : ℝ} : gridG α L H a b = gridG α L H b a

theorem CommutingRepetition.measurableSet_sepTheta (r a b : ℝ) : MeasurableSet {θ : ℝ | binIdx r θ a ≠ binIdx r θ b}

The θ-averaged master bound (proof layer)

theorem CommutingRepetition.shift_dist_le {α L a b : ℝ} (hα0 : 0 < α) (hα2 : α ≤ 1 / 2) (hL : 0 < L) (haL : L ≤ a) (hab : a ≤ b) (hnear : b < 2 * a) : Real.log b / Real.log (1 + α) - Real.log a / Real.log (1 + α) ≤ 3 * (b - a) / (α * b)

Grid-coordinate distance against the scaled value distance in the comparable case.

theorem CommutingRepetition.lintegral_gridF_le_core {α L H a b : ℝ} (hα0 : 0 < α) (hα2 : α ≤ 1 / 2) (hL : 0 < L) (ha : 0 ≤ a) (hab : a ≤ b) : ∫⁻ (θ : ℝ) in Set.Ico 0 1, ENNReal.ofReal (gridF (1 + α) θ L H a b) ≤ ENNReal.ofReal (gridG α L H a b)

The θ-averaged pointwise bound, oriented a ≤ b.

theorem CommutingRepetition.lintegral_gridF_le {α L H a b : ℝ} (hα0 : 0 < α) (hα2 : α ≤ 1 / 2) (hL : 0 < L) (ha : 0 ≤ a) (hb : 0 ≤ b) : ∫⁻ (θ : ℝ) in Set.Ico 0 1, ENNReal.ofReal (gridF (1 + α) θ L H a b) ≤ ENNReal.ofReal (gridG α L H a b)

The θ-averaged pointwise bound, symmetric form.