@[reducible, inline]

abbrev CommutingRepetition.VN.Crossed.L2Q (K : Type u_2) [NormedAddCommGroup K] [InnerProductSpace ℂ K] : Type u_2

ℓ²(ℚ, K).

Equations

• CommutingRepetition.VN.Crossed.L2Q K = ↥(lp (fun (x : ℚ) => K) 2)

instance CommutingRepetition.VN.Crossed.instCFC_L2Q {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : ContinuousFunctionalCalculus ℝ (L2Q K →L[ℂ] L2Q K) IsSelfAdjoint

Shortcut instance: the self-adjoint continuous functional calculus on B(ℓ²(ℚ, K)) (instance search otherwise gives up on this type).

ℓ² bookkeeping

theorem CommutingRepetition.VN.Crossed.two_toReal : ENNReal.toReal 2 = 2

theorem CommutingRepetition.VN.Crossed.summable_norm_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (f : L2Q K) : Summable fun (s : ℚ) => ‖↑f s‖ ^ 2

theorem CommutingRepetition.VN.Crossed.norm_sq_eq_tsum {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (f : L2Q K) : ‖f‖ ^ 2 = ∑' (s : ℚ), ‖↑f s‖ ^ 2

theorem CommutingRepetition.VN.Crossed.memℓp_of_summable_sq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {g : ℚ → K} (hg : Summable fun (s : ℚ) => ‖g s‖ ^ 2) : Memℓp g 2

noncomputable def CommutingRepetition.VN.Crossed.mkVec {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ → K) (hg : Summable fun (s : ℚ) => ‖g s‖ ^ 2) : L2Q K

The element of ℓ²(ℚ, K) with coordinates g.

Equations

• CommutingRepetition.VN.Crossed.mkVec g hg = ⟨g, ⋯⟩

theorem CommutingRepetition.VN.Crossed.mkVec_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ → K) (hg : Summable fun (s : ℚ) => ‖g s‖ ^ 2) (s : ℚ) : ↑(mkVec g hg) s = g s

theorem CommutingRepetition.VN.Crossed.norm_le_of_tsum_sq_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {f : L2Q K} {C : ℝ} (hC : 0 ≤ C) (h : ∑' (s : ℚ), ‖↑f s‖ ^ 2 ≤ C ^ 2) : ‖f‖ ≤ C

theorem CommutingRepetition.VN.Crossed.norm_apply_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (f : L2Q K) (s : ℚ) : ‖↑f s‖ ≤ ‖f‖

Coordinate embeddings and evaluations

noncomputable def CommutingRepetition.VN.Crossed.sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (g : ℚ) : K →L[ℂ] L2Q K

The g-th coordinate embedding K → ℓ²(ℚ, K).

Equations

• CommutingRepetition.VN.Crossed.sgl g = lp.singleContinuousLinearMap ℂ (fun (x : ℚ) => K) 2 g

noncomputable def CommutingRepetition.VN.Crossed.ev {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (g : ℚ) : L2Q K →L[ℂ] K

The g-th coordinate evaluation ℓ²(ℚ, K) → K.

Equations

• CommutingRepetition.VN.Crossed.ev g = lp.evalCLM ℂ (fun (x : ℚ) => K) 2 g

theorem CommutingRepetition.VN.Crossed.ev_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) : (ev g) f = ↑f g

theorem CommutingRepetition.VN.Crossed.sgl_apply_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) : ↑((sgl g) v) g = v

theorem CommutingRepetition.VN.Crossed.sgl_apply_ne {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) {s : ℚ} (h : s ≠ g) : ↑((sgl g) v) s = 0

theorem CommutingRepetition.VN.Crossed.sgl_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) (s : ℚ) : ↑((sgl g) v) s = if s = g then v else 0

theorem CommutingRepetition.VN.Crossed.ev_sgl_self {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) : (ev g) ((sgl g) v) = v

theorem CommutingRepetition.VN.Crossed.ev_sgl_ne {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {s g : ℚ} (h : s ≠ g) (v : K) : (ev s) ((sgl g) v) = 0

theorem CommutingRepetition.VN.Crossed.norm_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) : ‖(sgl g) v‖ = ‖v‖

theorem CommutingRepetition.VN.Crossed.inner_sgl_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g h : ℚ) (v w : K) : inner ℂ ((sgl g) v) ((sgl h) w) = if g = h then inner ℂ v w else 0

theorem CommutingRepetition.VN.Crossed.hasSum_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (f : L2Q K) : HasSum (fun (s : ℚ) => (sgl s) (↑f s)) f

theorem CommutingRepetition.VN.Crossed.eq_top_of_sgl_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {V : Submodule ℂ (L2Q K)} (hV : IsClosed ↑V) (h : ∀ (s : ℚ) (v : K), (sgl s) v ∈ V) : V = ⊤

A closed submodule containing all sgl s v is everything.

noncomputable def CommutingRepetition.VN.Crossed.unit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (g h : ℚ) : L2Q K →L[ℂ] L2Q K

The matrix unit e_g e_h*.

Equations

• CommutingRepetition.VN.Crossed.unit g h = CommutingRepetition.VN.Crossed.sgl g ∘SL CommutingRepetition.VN.Crossed.ev h

theorem CommutingRepetition.VN.Crossed.unit_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g h : ℚ) (f : L2Q K) : (unit g h) f = (sgl g) (↑f h)

Diagonal operators

def CommutingRepetition.VN.Crossed.IsBddFam {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (x : ℚ → K →L[ℂ] K) : Prop

A uniformly bounded family of operators.

Equations

• CommutingRepetition.VN.Crossed.IsBddFam x = ∃ (C : ℝ), ∀ (s : ℚ), ‖x s‖ ≤ C

theorem CommutingRepetition.VN.Crossed.IsBddFam.const {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : IsBddFam fun (x : ℚ) => y

theorem CommutingRepetition.VN.Crossed.IsBddFam.mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x y : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (hy : IsBddFam y) : IsBddFam fun (s : ℚ) => x s * y s

theorem CommutingRepetition.VN.Crossed.IsBddFam.add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x y : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (hy : IsBddFam y) : IsBddFam fun (s : ℚ) => x s + y s

theorem CommutingRepetition.VN.Crossed.IsBddFam.smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (c : ℂ) {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) : IsBddFam fun (s : ℚ) => c • x s

theorem CommutingRepetition.VN.Crossed.IsBddFam.star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) : IsBddFam fun (s : ℚ) => Star.star (x s)

theorem CommutingRepetition.VN.Crossed.IsBddFam.comp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (φ : ℚ → ℚ) : IsBddFam fun (s : ℚ) => x (φ s)

theorem CommutingRepetition.VN.Crossed.IsBddFam.of_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} {C : ℝ} (h : ∀ (s : ℚ), ‖x s‖ ≤ C) : IsBddFam x

theorem CommutingRepetition.VN.Crossed.summable_norm_sq_diag {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) {C : ℝ} (hx : ∀ (s : ℚ), ‖x s‖ ≤ C) (f : L2Q K) : Summable fun (s : ℚ) => ‖(x s) (↑f s)‖ ^ 2

noncomputable def CommutingRepetition.VN.Crossed.diagPre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) {C : ℝ} (hx : ∀ (s : ℚ), ‖x s‖ ≤ C) : L2Q K →ₗ[ℂ] L2Q K

The diagonal operator of a uniformly bounded family, as a linear map.

Equations

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

theorem CommutingRepetition.VN.Crossed.diagPre_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) {C : ℝ} (hx : ∀ (s : ℚ), ‖x s‖ ≤ C) (f : L2Q K) (s : ℚ) : ↑((diagPre x hx) f) s = (x s) (↑f s)

theorem CommutingRepetition.VN.Crossed.norm_diagPre_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) {C : ℝ} (hx : ∀ (s : ℚ), ‖x s‖ ≤ C) (f : L2Q K) : ‖(diagPre x hx) f‖ ≤ max C 0 * ‖f‖

noncomputable def CommutingRepetition.VN.Crossed.diag {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) : L2Q K →L[ℂ] L2Q K

The diagonal operator ⊕_s x s of a uniformly bounded family (junk 0 otherwise).

Equations

• CommutingRepetition.VN.Crossed.diag x = if hx : CommutingRepetition.VN.Crossed.IsBddFam x then (CommutingRepetition.VN.Crossed.diagPre x ⋯).mkContinuous (max (Exists.choose hx) 0) ⋯ else 0

theorem CommutingRepetition.VN.Crossed.diag_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) (hx : IsBddFam x) (f : L2Q K) (s : ℚ) : ↑((diag x) f) s = (x s) (↑f s)

theorem CommutingRepetition.VN.Crossed.diag_ext {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) (hx : IsBddFam x) {T : L2Q K →L[ℂ] L2Q K} (h : ∀ (f : L2Q K) (s : ℚ), ↑(T f) s = (x s) (↑f s)) : T = diag x

theorem CommutingRepetition.VN.Crossed.norm_diag_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) {C : ℝ} (hC : 0 ≤ C) (hx : ∀ (s : ℚ), ‖x s‖ ≤ C) : ‖diag x‖ ≤ C

theorem CommutingRepetition.VN.Crossed.ev_diag {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) (hx : IsBddFam x) (s : ℚ) (f : L2Q K) : (ev s) ((diag x) f) = (x s) ((ev s) f)

theorem CommutingRepetition.VN.Crossed.diag_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (x : ℚ → K →L[ℂ] K) (hx : IsBddFam x) (g : ℚ) (v : K) : (diag x) ((sgl g) v) = (sgl g) ((x g) v)

theorem CommutingRepetition.VN.Crossed.diag_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x y : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (hy : IsBddFam y) : (diag fun (s : ℚ) => x s + y s) = diag x + diag y

theorem CommutingRepetition.VN.Crossed.diag_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (c : ℂ) (hx : IsBddFam x) : (diag fun (s : ℚ) => c • x s) = c • diag x

theorem CommutingRepetition.VN.Crossed.diag_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x y : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (hy : IsBddFam y) : (diag fun (s : ℚ) => x s * y s) = diag x * diag y

theorem CommutingRepetition.VN.Crossed.diag_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : (diag fun (x : ℚ) => 1) = 1

theorem CommutingRepetition.VN.Crossed.diag_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : (diag fun (x : ℚ) => 0) = 0

theorem CommutingRepetition.VN.Crossed.inner_diag_right {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (f g : L2Q K) : inner ℂ f ((diag x) g) = ∑' (s : ℚ), inner ℂ (↑f s) ((x s) (↑g s))

theorem CommutingRepetition.VN.Crossed.diag_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) : (diag fun (s : ℚ) => star (x s)) = star (diag x)

theorem CommutingRepetition.VN.Crossed.diag_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (h : ∀ (s : ℚ), IsSelfAdjoint (x s)) : IsSelfAdjoint (diag x)

noncomputable def CommutingRepetition.VN.Crossed.amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : L2Q K →L[ℂ] L2Q K

1 ⊗ y.

Equations

• CommutingRepetition.VN.Crossed.amp y = CommutingRepetition.VN.Crossed.diag fun (x : ℚ) => y

theorem CommutingRepetition.VN.Crossed.amp_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) (f : L2Q K) (s : ℚ) : ↑((amp y) f) s = y (↑f s)

theorem CommutingRepetition.VN.Crossed.amp_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : amp 1 = 1

theorem CommutingRepetition.VN.Crossed.amp_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y z : K →L[ℂ] K) : amp (y * z) = amp y * amp z

theorem CommutingRepetition.VN.Crossed.amp_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : amp (star y) = star (amp y)

theorem CommutingRepetition.VN.Crossed.amp_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y z : K →L[ℂ] K) : amp (y + z) = amp y + amp z

theorem CommutingRepetition.VN.Crossed.amp_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (c : ℂ) (y : K →L[ℂ] K) : amp (c • y) = c • amp y

theorem CommutingRepetition.VN.Crossed.amp_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) (g : ℚ) (v : K) : (amp y) ((sgl g) v) = (sgl g) (y v)

theorem CommutingRepetition.VN.Crossed.norm_amp_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (y : K →L[ℂ] K) : ‖amp y‖ ≤ ‖y‖

theorem CommutingRepetition.VN.Crossed.amp_diag_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) {y : K →L[ℂ] K} (h : ∀ (s : ℚ), Commute (x s) y) : Commute (diag x) (amp y)

Shifts

theorem CommutingRepetition.VN.Crossed.summable_norm_sq_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) : Summable fun (s : ℚ) => ‖↑f (s - g)‖ ^ 2

noncomputable def CommutingRepetition.VN.Crossed.shiftPre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) : L2Q K →ₗ[ℂ] L2Q K

The shift (shift g f)(h) = f(h − g) as a linear map.

Equations

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

theorem CommutingRepetition.VN.Crossed.shiftPre_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) (s : ℚ) : ↑((shiftPre g) f) s = ↑f (s - g)

theorem CommutingRepetition.VN.Crossed.norm_shiftPre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) : ‖(shiftPre g) f‖ = ‖f‖

noncomputable def CommutingRepetition.VN.Crossed.shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) : L2Q K →L[ℂ] L2Q K

The unitary shift λ(g): (λ(g) f)(h) = f(h − g).

Equations

• CommutingRepetition.VN.Crossed.shift g = (CommutingRepetition.VN.Crossed.shiftPre g).mkContinuous 1 ⋯

theorem CommutingRepetition.VN.Crossed.shift_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) (s : ℚ) : ↑((shift g) f) s = ↑f (s - g)

theorem CommutingRepetition.VN.Crossed.norm_shift_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f : L2Q K) : ‖(shift g) f‖ = ‖f‖

theorem CommutingRepetition.VN.Crossed.shift_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : shift 0 = 1

theorem CommutingRepetition.VN.Crossed.shift_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g h : ℚ) : shift (g + h) = shift g * shift h

theorem CommutingRepetition.VN.Crossed.shift_neg_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) : shift (-g) * shift g = 1

theorem CommutingRepetition.VN.Crossed.shift_mul_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) : shift g * shift (-g) = 1

theorem CommutingRepetition.VN.Crossed.shift_comm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g h : ℚ) : shift g * shift h = shift h * shift g

theorem CommutingRepetition.VN.Crossed.inner_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (f k : L2Q K) : inner ℂ ((shift g) f) ((shift g) k) = inner ℂ f k

theorem CommutingRepetition.VN.Crossed.shift_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) : star (shift g) = shift (-g)

theorem CommutingRepetition.VN.Crossed.shift_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g s : ℚ) (v : K) : (shift g) ((sgl s) v) = (sgl (s + g)) v

theorem CommutingRepetition.VN.Crossed.shift_diag {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (g : ℚ) (hx : IsBddFam x) : shift g * diag x = (diag fun (s : ℚ) => x (s - g)) * shift g

Covariance of shifts and diagonal operators: λ(g) ⊕ x_s = (⊕ x_{s−g}) λ(g).

theorem CommutingRepetition.VN.Crossed.shift_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (y : K →L[ℂ] K) : shift g * amp y = amp y * shift g

theorem CommutingRepetition.VN.Crossed.shift_mul_diag_mul_shift_neg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (g : ℚ) (hx : IsBddFam x) : shift g * diag x * shift (-g) = diag fun (s : ℚ) => x (s - g)