amp as a *-homomorphism

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

theorem CommutingRepetition.VN.Crossed.amp_sub {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_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) : IsSelfAdjoint (amp E)

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

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

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

amp as a *-algebra homomorphism B(K) → B(ℓ²(ℚ, K)).

Equations

• CommutingRepetition.VN.Crossed.ampHom = { toFun := CommutingRepetition.VN.Crossed.amp, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

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

theorem CommutingRepetition.VN.Crossed.continuous_ampHom {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] : Continuous ⇑ampHom

theorem CommutingRepetition.VN.Crossed.amp_cfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {f : ℝ → ℝ} (hf : Continuous f) : amp (cfc f E) = cfc f (amp E)

Amplification commutes with the continuous functional calculus.

Spectral measures of 1 ⊗ E

theorem CommutingRepetition.VN.Crossed.ν_apply_univ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (ξ : K) : (BorelCalc.ν E hE ξ) Set.univ = ENNReal.ofReal (‖ξ‖ ^ 2)

theorem CommutingRepetition.VN.Crossed.isFiniteMeasure_sum_ν {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (ζ : L2Q K) : MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.sum fun (s : ℚ) => BorelCalc.ν E hE (↑ζ s))

Σ_s ν_E(ζ s) is a finite measure (of mass ‖ζ‖²).

theorem CommutingRepetition.VN.Crossed.ν_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) (ζ : L2Q K) : BorelCalc.ν (amp E) ⋯ ζ = MeasureTheory.Measure.sum fun (s : ℚ) => BorelCalc.ν E hE (↑ζ s)

The spectral measure of 1 ⊗ E at ζ is Σ_s ν_E(ζ s).

theorem CommutingRepetition.VN.Crossed.amp_bfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : amp (BorelCalc.bfc E hE g) = BorelCalc.bfc (amp E) ⋯ g

Amplification commutes with the bounded Borel calculus.

theorem CommutingRepetition.VN.Crossed.amp_cbfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {E : K →L[ℂ] K} (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : BorelCalc.CBdd G) : amp (BorelCalc.cbfc E hE G) = BorelCalc.cbfc (amp E) ⋯ G

Amplification commutes with the complex bounded Borel calculus.