theorem CommutingRepetition.GraphMod.Eop_comm_conjJ (M : StdTracialAlgebra) (x y : M.H) : Commute (Eop M x) (M.conjJ (Eop M y))

Eₓ ∈ R(M)′ commutes with J E_y J.

theorem CommutingRepetition.GraphMod.conjJ_Eop_sa (M : StdTracialAlgebra) (y : M.H) : IsSelfAdjoint (M.conjJ (Eop M y))

noncomputable def CommutingRepetition.GraphMod.νxy (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure (ℝ × ℝ)

The joint spectral measure of (Eₓ, J E_y J) at the trace vector.

Equations

• CommutingRepetition.GraphMod.νxy M x y = CommutingRepetition.BorelCalc.νP (CommutingRepetition.GraphMod.Eop M x) (M.conjJ (CommutingRepetition.GraphMod.Eop M y)) ⋯ ⋯ ⋯ M.traceVector

instance CommutingRepetition.GraphMod.νxy_isFiniteMeasure (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.IsFiniteMeasure (νxy M x y)

theorem CommutingRepetition.GraphMod.νxy_map_fst (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure.map Prod.fst (νxy M x y) = BorelCalc.ν (Eop M x) ⋯ M.traceVector

theorem CommutingRepetition.GraphMod.νxy_map_snd (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure.map Prod.snd (νxy M x y) = BorelCalc.ν (Eop M y) ⋯ M.traceVector

theorem CommutingRepetition.GraphMod.νxy_univ (M : StdTracialAlgebra) (x y : M.H) : (νxy M x y) Set.univ = 1

instance CommutingRepetition.GraphMod.νxy_isProbabilityMeasure (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.IsProbabilityMeasure (νxy M x y)

theorem CommutingRepetition.GraphMod.νxy_prod (M : StdTracialAlgebra) (x y : M.H) {K K' : Set ℝ} (hK : MeasurableSet K) (hK' : MeasurableSet K') : ↑((νxy M x y) (K ×ˢ K')).toReal = inner ℂ M.traceVector ((BorelCalc.P (Eop M x) ⋯ K) ((BorelCalc.P (Eop M y) ⋯ K') M.traceVector))

Rectangle masses: ν_{x,y}(K × K') = ⟪Ω, 1_K(Eₓ) 1_{K'}(E_y) Ω⟫.

theorem CommutingRepetition.GraphMod.integral_νxy_mul (M : StdTracialAlgebra) (x y : M.H) {g h : ℝ → ℝ} (hg : BorelCalc.Bdd g) (hh : BorelCalc.Bdd h) : ∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νxy M x y = (inner ℂ ((BorelCalc.bfc (Eop M x) ⋯ g) M.traceVector) ((BorelCalc.bfc (Eop M y) ⋯ h) M.traceVector)).re

The product formula at the trace vector, for bounded Borel g, h: ∫ g(s) h(t) dν_{x,y} = re ⟪g(Eₓ) Ω, h(E_y) Ω⟫.

The coupling of the modulus distributions

theorem CommutingRepetition.GraphMod.measurable_ψψ : Measurable (Prod.map ψ ψ)

noncomputable def CommutingRepetition.GraphMod.νψ (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure (ℝ × ℝ)

The joint coupling ν_{x,y} = (ψ × ψ)_* ν_{Eₓ, JE_yJ; Ω} of μₓ and μ_y.

Equations

• CommutingRepetition.GraphMod.νψ M x y = MeasureTheory.Measure.map (Prod.map CommutingRepetition.GraphMod.ψ CommutingRepetition.GraphMod.ψ) (CommutingRepetition.GraphMod.νxy M x y)

theorem CommutingRepetition.GraphMod.νψ_prob (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.IsProbabilityMeasure (νψ M x y)

theorem CommutingRepetition.GraphMod.νψ_map_fst (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure.map Prod.fst (νψ M x y) = μx M x

theorem CommutingRepetition.GraphMod.νψ_map_snd (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Measure.map Prod.snd (νψ M x y) = μx M y

theorem CommutingRepetition.GraphMod.cross (M : StdTracialAlgebra) (x y : M.H) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) : M.vnModel.τ (projx M x I * projx M y J) = ↑((νψ M x y) (I ×ˢ J)).toReal

The rectangle identity in the form consumed by JointSpectralData.cross.

The cross moment

theorem CommutingRepetition.GraphMod.integrable_ψ_sq_fst (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => ψ p.1 ^ 2) (νxy M x y)

theorem CommutingRepetition.GraphMod.integrable_ψ_sq_snd (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => ψ p.2 ^ 2) (νxy M x y)

theorem CommutingRepetition.GraphMod.integrable_ψ_mul (M : StdTracialAlgebra) (x y : M.H) : MeasureTheory.Integrable (fun (p : ℝ × ℝ) => ψ p.1 * ψ p.2) (νxy M x y)

theorem CommutingRepetition.GraphMod.integral_ψ_sq_fst (M : StdTracialAlgebra) (x y : M.H) : ∫ (p : ℝ × ℝ), ψ p.1 ^ 2 ∂νxy M x y = ‖x‖ ^ 2

theorem CommutingRepetition.GraphMod.integral_ψ_sq_snd (M : StdTracialAlgebra) (x y : M.H) : ∫ (p : ℝ × ℝ), ψ p.2 ^ 2 ∂νxy M x y = ‖y‖ ^ 2

theorem CommutingRepetition.GraphMod.ψn_mul_mono (p : ℝ × ℝ) : Monotone fun (n : ℕ) => ψn n p.1 * ψn n p.2

theorem CommutingRepetition.GraphMod.ψn_mul_tendsto (p : ℝ × ℝ) : Filter.Tendsto (fun (n : ℕ) => ψn n p.1 * ψn n p.2) Filter.atTop (nhds (ψ p.1 * ψ p.2))

theorem CommutingRepetition.GraphMod.integral_ψ_mul (M : StdTracialAlgebra) (x y : M.H) : ∫ (p : ℝ × ℝ), ψ p.1 * ψ p.2 ∂νxy M x y = (inner ℂ (hvec M x) (hvec M y)).re

The cross term: ∫ ψ(s) ψ(t) dν_{x,y} = re ⟪hvec x, hvec y⟫.

theorem CommutingRepetition.GraphMod.crossMoment (M : StdTracialAlgebra) (x y : M.H) : ∫ (p : ℝ × ℝ), (p.1 - p.2) ^ 2 ∂νψ M x y = ‖hvec M x - hvec M y‖ ^ 2

The cross moment: ∫ (s − t)² dν_{x,y}(s, t) = ‖hvec x − hvec y‖².