Retained bins as a band family

noncomputable def CommutingRepetition.binLo (r θ L : ℝ) : ℤ

Lowest retained bin index: the bin containing L.

Equations

• CommutingRepetition.binLo r θ L = CommutingRepetition.binIdx r θ L

noncomputable def CommutingRepetition.binHi (r θ H : ℝ) : ℤ

Highest retained bin index: the bin containing H.

Equations

• CommutingRepetition.binHi r θ H = CommutingRepetition.binIdx r θ H

noncomputable def CommutingRepetition.binCount (r θ L H : ℝ) : ℕ

Number of retained bins (those meeting the window [L, H]).

Equations

• CommutingRepetition.binCount r θ L H = (CommutingRepetition.binHi r θ H - CommutingRepetition.binLo r θ L + 1).toNat

noncomputable def CommutingRepetition.retainedBin (r θ L H : ℝ) (k : Fin (binCount r θ L H)) : Set ℝ

The k-th retained bin I_j^θ ∩ [L, H], j = binLo + k (06_otqcs.tex, eq N1-Z "the finite retained bin set").

Equations

• CommutingRepetition.retainedBin r θ L H k = CommutingRepetition.binIdx r θ ⁻¹' {CommutingRepetition.binLo r θ L + ↑↑k} ∩ Set.Icc L H

noncomputable def CommutingRepetition.retainedVal (r θ L H : ℝ) (k : Fin (binCount r θ L H)) : ℝ

Its band value: the upper endpoint t_j^θ = r^(j+1+θ) (eq shifted-bins).

Equations

• CommutingRepetition.retainedVal r θ L H k = r ^ (↑(CommutingRepetition.binLo r θ L + ↑↑k) + 1 + θ)

theorem CommutingRepetition.binIdx_mono {r θ : ℝ} (hr : 1 < r) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : binIdx r θ a ≤ binIdx r θ b

theorem CommutingRepetition.binIdx_mem_range {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) {a : ℝ} (ha : a ∈ Set.Icc L H) : binLo r θ L ≤ binIdx r θ a ∧ binIdx r θ a ≤ binHi r θ H

noncomputable def CommutingRepetition.retainedIdx {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) {a : ℝ} (ha : a ∈ Set.Icc L H) : Fin (binCount r θ L H)

The retained index of a point of the window.

Equations

• CommutingRepetition.retainedIdx hr hL ha = ⟨(CommutingRepetition.binIdx r θ a - CommutingRepetition.binLo r θ L).toNat, ⋯⟩

theorem CommutingRepetition.retainedIdx_spec {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) {a : ℝ} (ha : a ∈ Set.Icc L H) : binLo r θ L + ↑↑(retainedIdx hr hL ha) = binIdx r θ a

theorem CommutingRepetition.roundSq_eq_sum_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (a : ℝ) : roundSq r θ L H a = ∑ k : Fin (binCount r θ L H), retainedVal r θ L H k ^ 2 * (retainedBin r θ L H k).indicator 1 a

The retained rounded square regroups over the retained bins: roundSq a = ∑_k t_k² 1_{B_k}(a) (eq abcGamma, finite retained-bin form).

theorem CommutingRepetition.jointRoundSq_eq_sum_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (a b : ℝ) : jointRoundSq r θ L H a b = ∑ k : Fin (binCount r θ L H), retainedVal r θ L H k ^ 2 * (retainedBin r θ L H k ×ˢ retainedBin r θ L H k).indicator 1 (a, b)

The same-bin joint rounded square regroups over the retained bins: jointRoundSq a b = ∑_k t_k² 1_{B_k × B_k}(a, b).

theorem CommutingRepetition.isBandFamily_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) : IsBandFamily (retainedBin r θ L H) (retainedVal r θ L H)

The retained bins form a band family.

theorem CommutingRepetition.retainedBin_subset {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (k : Fin (binCount r θ L H)) : retainedBin r θ L H k ⊆ Set.Icc (retainedVal r θ L H k / r) (retainedVal r θ L H k)

Each retained bin sits inside [t_k / r, t_k] (the shifted-bin geometry, as consumed by selSharp_round).

theorem CommutingRepetition.iUnion_retainedBin {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) : ⋃ (k : Fin (binCount r θ L H)), retainedBin r θ L H k = Set.Icc L H

The retained bins cover exactly the window [L, H].

theorem CommutingRepetition.binCount_pos {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (hLH : L ≤ H) : 0 < binCount r θ L H

A nondegenerate window retains at least one bin.

The grid functionals as band sums

theorem CommutingRepetition.gridA_eq_sum_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (ν : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsProbabilityMeasure ν] : gridA ν r θ L H = ∑ k : Fin (binCount r θ L H), retainedVal r θ L H k ^ 2 * ((MeasureTheory.Measure.map Prod.fst ν) (retainedBin r θ L H k)).toReal

theorem CommutingRepetition.gridB_eq_sum_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (ν : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsProbabilityMeasure ν] : gridB ν r θ L H = ∑ k : Fin (binCount r θ L H), retainedVal r θ L H k ^ 2 * ((MeasureTheory.Measure.map Prod.snd ν) (retainedBin r θ L H k)).toReal

theorem CommutingRepetition.gridC_eq_sum_retained {r θ L H : ℝ} (hr : 1 < r) (hL : 0 < L) (ν : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsProbabilityMeasure ν] : gridC ν r θ L H = ∑ k : Fin (binCount r θ L H), retainedVal r θ L H k ^ 2 * (ν (retainedBin r θ L H k ×ˢ retainedBin r θ L H k)).toReal

Band-mass inequalities (eq c-min and a + b − c ≤ Z)

theorem CommutingRepetition.marg_add_marg_sub_prod_le_one (ν : MeasureTheory.Measure (ℝ × ℝ)) [MeasureTheory.IsProbabilityMeasure ν] {B : Set ℝ} (hB : MeasurableSet B) : ((MeasureTheory.Measure.map Prod.fst ν) B).toReal + ((MeasureTheory.Measure.map Prod.snd ν) B).toReal - (ν (B ×ˢ B)).toReal ≤ 1

Per bin: μ_A(B) + μ_B(B) − ν(B×B) = ν((B×ℝ) ∪ (ℝ×B)) ≤ 1.

theorem CommutingRepetition.bandCross_nonneg {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (s : S) (t' : T) : 0 ≤ bandCross F B t s t'

theorem CommutingRepetition.bandCross_le_bandMassA {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (s : S) (t' : T) : bandCross F B t s t' ≤ bandMassA F B t s

theorem CommutingRepetition.bandCross_le_bandMassB {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (s : S) (t' : T) : bandCross F B t s t' ≤ bandMassB F B t t'

theorem CommutingRepetition.bandMassA_le_bandZ {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (s : S) : bandMassA F B t s ≤ bandZ t

theorem CommutingRepetition.bandMassB_le_bandZ {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (t' : T) : bandMassB F B t t' ≤ bandZ t

theorem CommutingRepetition.bandMass_add_sub_cross_le_bandZ {N : StdTracialAlgebra} {S : Type v} {T : Type w} {x : S → N.H} {y : T → N.H} (F : ModulusFamily N x y) {m : ℕ} (B : Fin m → Set ℝ) (t : Fin m → ℝ) (hB : IsBandFamily B t) (s : S) (t' : T) : bandMassA F B t s + bandMassB F B t t' - bandCross F B t s t' ≤ bandZ t

a_s + b_t − c_{st} ≤ Z (the per-trial progress is a probability).

theorem CommutingRepetition.bandZ_pos_of_pos {m : ℕ} (hm : 0 < m) {t : Fin m → ℝ} (ht : ∀ (j : Fin m), 0 < t j) : 0 < bandZ t

Z = ∑ t_j² > 0 for a nonempty band family with positive values.

Second-moment facts for the spectral distributions

theorem CommutingRepetition.integrable_sq_of_integral_eq_one {μ : MeasureTheory.Measure ℝ} (h : ∫ (b : ℝ), b ^ 2 ∂μ = 1) : MeasureTheory.Integrable (fun (b : ℝ) => b ^ 2) μ

theorem CommutingRepetition.setIntegral_sq_Icc_ge (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (hnn : μ (Set.Iio 0) = 0) (h1 : ∫ (b : ℝ), b ^ 2 ∂μ = 1) {L H ρ : ℝ} (hL : 0 < L) (hLH : L < H) (htail : ∫ (b : ℝ) in Set.Ioi H, b ^ 2 ∂μ ≤ ρ) : 1 - ρ - L ^ 2 ≤ ∫ (b : ℝ) in Set.Icc L H, b ^ 2 ∂μ

The retained-window second moment of a spectral distribution supported on [0, ∞) with unit second moment and high tail at most ρ is at least 1 − ρ − L² (06_otqcs.tex, eq rounding-tails: the omitted region is the low window [0, L) of mass at most L² and the high tail).

theorem CommutingRepetition.exists_tail_cutoff {ι : Type u_1} [Fintype ι] (μ : ι → MeasureTheory.Measure ℝ) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (hint : ∀ (i : ι), MeasureTheory.Integrable (fun (b : ℝ) => b ^ 2) (μ i)) {ρ : ℝ} (hρ : 0 < ρ) (L : ℝ) : ∃ (H : ℝ), L < H ∧ ∀ (i : ι), ∫ (b : ℝ) in Set.Ioi H, b ^ 2 ∂μ i ≤ ρ

One finite cutoff H > L makes every high squared tail of a finite family of probability measures with finite second moment at most ρ (06_otqcs.tex, "for each ρ > 0 one finite H makes the two high-tail bounds hold for every member").