Commutation with the Borel calculus

theorem CommutingRepetition.BorelCalc.commute_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {T : 𝓗 →L[ℂ] 𝓗} (hT : Commute E T) {g : ℝ → ℝ} (hg : Bdd g) : Commute (bfc E hE g) T

An operator commuting with E commutes with the Borel calculus of E.

theorem CommutingRepetition.BorelCalc.sa_mul_of_commute {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {A B : 𝓗 →L[ℂ] 𝓗} (hA : IsSelfAdjoint A) (hB : IsSelfAdjoint B) (h : Commute A B) : IsSelfAdjoint (A * B)

The spectral measure of a normal operator, pushed to the plane

noncomputable def CommutingRepetition.BorelCalc.ofRealCM {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (f : C(↑(spectrum ℂ Z), ℝ)) : C(↑(spectrum ℂ Z), ℂ)

Real continuous functions on the spectrum, as complex-valued ones.

Equations

• CommutingRepetition.BorelCalc.ofRealCM Z f = { toFun := fun (s : ↑(spectrum ℂ Z)) => ↑(f s), continuous_toFun := ⋯ }

theorem CommutingRepetition.BorelCalc.ofRealCM_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (f : C(↑(spectrum ℂ Z), ℝ)) (s : ↑(spectrum ℂ Z)) : (ofRealCM Z f) s = ↑(f s)

theorem CommutingRepetition.BorelCalc.ofRealCM_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (f g : C(↑(spectrum ℂ Z), ℝ)) : ofRealCM Z (f + g) = ofRealCM Z f + ofRealCM Z g

theorem CommutingRepetition.BorelCalc.ofRealCM_smul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (c : ℝ) (f : C(↑(spectrum ℂ Z), ℝ)) : ofRealCM Z (c • f) = ↑c • ofRealCM Z f

theorem CommutingRepetition.BorelCalc.ofRealCM_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (f g : C(↑(spectrum ℂ Z), ℝ)) : ofRealCM Z (f * g) = ofRealCM Z f * ofRealCM Z g

theorem CommutingRepetition.BorelCalc.star_ofRealCM {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (f : C(↑(spectrum ℂ Z), ℝ)) : star (ofRealCM Z f) = ofRealCM Z f

noncomputable def CommutingRepetition.BorelCalc.stateLinC {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : C(↑(spectrum ℂ Z), ℝ) →ₗ[ℝ] ℝ

The vector state f ↦ re ⟪ξ, f(Z) ξ⟫ on C(spectrum ℂ Z, ℝ).

Equations

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

theorem CommutingRepetition.BorelCalc.stateLinC_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) (f : C(↑(spectrum ℂ Z), ℝ)) : (stateLinC Z hZ ξ) f = (inner ℂ ξ (((cfcHom hZ) (ofRealCM Z f)) ξ)).re

theorem CommutingRepetition.BorelCalc.cfcHom_ofRealCM_sa {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (f : C(↑(spectrum ℂ Z), ℝ)) : IsSelfAdjoint ((cfcHom hZ) (ofRealCM Z f))

theorem CommutingRepetition.BorelCalc.stateLinC_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) {f : C(↑(spectrum ℂ Z), ℝ)} (hf : 0 ≤ f) : 0 ≤ (stateLinC Z hZ ξ) f

noncomputable def CommutingRepetition.BorelCalc.ΛC {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : CompactlySupportedContinuousMap ↑(spectrum ℂ Z) ℝ →ₚ[ℝ] ℝ

The vector state as a positive linear functional on C_c(spectrum ℂ Z, ℝ).

Equations

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

theorem CommutingRepetition.BorelCalc.ΛC_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) (f : CompactlySupportedContinuousMap ↑(spectrum ℂ Z) ℝ) : (ΛC Z hZ ξ) f = (inner ℂ ξ (((cfcHom hZ) (ofRealCM Z f.toContinuousMap)) ξ)).re

noncomputable def CommutingRepetition.BorelCalc.ρ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : MeasureTheory.Measure ↑(spectrum ℂ Z)

The Riesz measure of the vector state on the compact spectrum of Z.

Equations

• CommutingRepetition.BorelCalc.ρ Z hZ ξ = RealRMK.rieszMeasure (CommutingRepetition.BorelCalc.ΛC Z hZ ξ)

instance CommutingRepetition.BorelCalc.ρ_isFiniteMeasure {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : MeasureTheory.IsFiniteMeasure (ρ Z hZ ξ)

def CommutingRepetition.BorelCalc.toPlane {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) : ↑(spectrum ℂ Z) → ℝ × ℝ

z ↦ (re z, im z) on the spectrum.

Equations

• CommutingRepetition.BorelCalc.toPlane Z s = ((↑s).re, (↑s).im)

theorem CommutingRepetition.BorelCalc.measurable_toPlane {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) : Measurable (toPlane Z)

noncomputable def CommutingRepetition.BorelCalc.νJ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : MeasureTheory.Measure (ℝ × ℝ)

The spectral measure of the normal operator Z at ξ, on the plane.

Equations

• CommutingRepetition.BorelCalc.νJ Z hZ ξ = MeasureTheory.Measure.map (CommutingRepetition.BorelCalc.toPlane Z) (CommutingRepetition.BorelCalc.ρ Z hZ ξ)

instance CommutingRepetition.BorelCalc.νJ_isFiniteMeasure {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) : MeasureTheory.IsFiniteMeasure (νJ Z hZ ξ)

theorem CommutingRepetition.BorelCalc.integral_νJ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (Z : 𝓗 →L[ℂ] 𝓗) (hZ : IsStarNormal Z) (ξ : 𝓗) {F : ℝ × ℝ → ℝ} (hF : Continuous F) : ∫ (p : ℝ × ℝ), F p ∂νJ Z hZ ξ = (inner ℂ ξ ((cfc (fun (z : ℂ) => ↑(F (z.re, z.im))) Z) ξ)).re

The defining property: ∫ F dνJ = re ⟪ξ, F(re Z, im Z) ξ⟫ for continuous F.

The commuting pair E₁, E₂ and Z = E₁ + i E₂

noncomputable def CommutingRepetition.BorelCalc.Zp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) : 𝓗 →L[ℂ] 𝓗

Z = E₁ + i E₂.

Equations

• CommutingRepetition.BorelCalc.Zp E₁ E₂ = E₁ + Complex.I • E₂

theorem CommutingRepetition.BorelCalc.star_Zp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) : star (Zp E₁ E₂) = E₁ - Complex.I • E₂

theorem CommutingRepetition.BorelCalc.Zp_normal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) : IsStarNormal (Zp E₁ E₂)

theorem CommutingRepetition.BorelCalc.cfc_re {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) : cfc (fun (z : ℂ) => ↑z.re) (Zp E₁ E₂) = E₁

theorem CommutingRepetition.BorelCalc.cfc_im {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) : cfc (fun (z : ℂ) => ↑z.im) (Zp E₁ E₂) = E₂

theorem CommutingRepetition.BorelCalc.cfc_re_comp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Continuous g) : cfc (fun (z : ℂ) => ↑(g z.re)) (Zp E₁ E₂) = cfc g E₁

theorem CommutingRepetition.BorelCalc.cfc_im_comp {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g : ℝ → ℝ} (hg : Continuous g) : cfc (fun (z : ℂ) => ↑(g z.im)) (Zp E₁ E₂) = cfc g E₂

noncomputable def CommutingRepetition.BorelCalc.νP {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : MeasureTheory.Measure (ℝ × ℝ)

The joint spectral measure of the commuting pair (E₁, E₂) at ξ.

Equations

• CommutingRepetition.BorelCalc.νP E₁ E₂ h₁ h₂ hc ξ = CommutingRepetition.BorelCalc.νJ (CommutingRepetition.BorelCalc.Zp E₁ E₂) ⋯ ξ

instance CommutingRepetition.BorelCalc.νP_isFiniteMeasure {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : MeasureTheory.IsFiniteMeasure (νP E₁ E₂ h₁ h₂ hc ξ)

theorem CommutingRepetition.BorelCalc.commute_cfc_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (hc : Commute E₁ E₂) (g h : ℝ → ℝ) : Commute (cfc g E₁) (cfc h E₂)

theorem CommutingRepetition.BorelCalc.commute_bfc_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : Commute (bfc E₁ h₁ g) (bfc E₂ h₂ h)

theorem CommutingRepetition.BorelCalc.integral_νP_mul_cont {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hg : Continuous g) (hh : Continuous h) (ξ : 𝓗) : ∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νP E₁ E₂ h₁ h₂ hc ξ = (inner ℂ ξ ((cfc g E₁) ((cfc h E₂) ξ))).re

Products: for continuous g, h, ∫ g(s) h(t) dνP = re ⟪ξ, g(E₁) h(E₂) ξ⟫.

Transfer to bounded Borel functions

theorem CommutingRepetition.BorelCalc.integrable_of_bdd' {α : Type u_2} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {f : α → ℝ} (hf : Measurable f) {C : ℝ} (hC : ∀ (a : α), |f a| ≤ C) : MeasureTheory.Integrable f μ

Bounded measurable functions are integrable against finite measures.

theorem CommutingRepetition.BorelCalc.IsCombo.congr {Φ Ψ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) (h : ∀ (g : ℝ → ℝ), Bdd g → Φ g = Ψ g) : IsCombo Ψ

theorem CommutingRepetition.BorelCalc.isCombo_integral_mul {α : Type u_2} [MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] {u : α → ℝ} (hu : Measurable u) {w : α → ℝ} (hw : Measurable w) {C : ℝ} (hC : ∀ (a : α), |w a| ≤ C) : IsCombo fun (g : ℝ → ℝ) => ↑(∫ (a : α), g (u a) * w a ∂μ)

g ↦ ∫ g(u a) w(a) dμ(a) is a combination of finite measures on ℝ, for a finite measure μ, a measurable u and a bounded measurable weight w.

theorem CommutingRepetition.BorelCalc.inner_bfc_bfc_cont {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hgc : Continuous g) (hg : Bdd g) (hhc : Continuous h) (hh : Bdd h) (ξ : 𝓗) : ↑(∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νP E₁ E₂ h₁ h₂ hc ξ) = inner ℂ ξ ((bfc E₁ h₁ g) ((bfc E₂ h₂ h) ξ))

Step 0: bounded continuous g, h.

theorem CommutingRepetition.BorelCalc.inner_bfc_bfc_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hg : Bdd g) (hhc : Continuous h) (hh : Bdd h) (ξ : 𝓗) : ↑(∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νP E₁ E₂ h₁ h₂ hc ξ) = inner ℂ ξ ((bfc E₁ h₁ g) ((bfc E₂ h₂ h) ξ))

Step 1: bounded Borel g, bounded continuous h (transfer in g).

theorem CommutingRepetition.BorelCalc.inner_bfc_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ : 𝓗) : ↑(∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νP E₁ E₂ h₁ h₂ hc ξ) = inner ℂ ξ ((bfc E₁ h₁ g) ((bfc E₂ h₂ h) ξ))

The product formula for bounded Borel g, h: ∫ g(s) h(t) dνP_ξ(s, t) = ⟪ξ, g(E₁) h(E₂) ξ⟫ (transfer in h).

theorem CommutingRepetition.BorelCalc.integral_νP_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ : 𝓗) : ∫ (p : ℝ × ℝ), g p.1 * h p.2 ∂νP E₁ E₂ h₁ h₂ hc ξ = (inner ℂ ξ ((bfc E₁ h₁ g) ((bfc E₂ h₂ h) ξ))).re

Rectangles and marginals

theorem CommutingRepetition.BorelCalc.νP_prod {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) (ξ : 𝓗) : ↑((νP E₁ E₂ h₁ h₂ hc ξ) (I ×ˢ J)).toReal = inner ℂ ξ ((P E₁ h₁ I) ((P E₂ h₂ J) ξ))

Rectangle masses: νP_ξ(I × J) = ⟪ξ, 1_I(E₁) 1_J(E₂) ξ⟫.

theorem CommutingRepetition.BorelCalc.νP_prod_toReal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) {I J : Set ℝ} (hI : MeasurableSet I) (hJ : MeasurableSet J) (ξ : 𝓗) : ((νP E₁ E₂ h₁ h₂ hc ξ) (I ×ˢ J)).toReal = (inner ℂ ξ ((P E₁ h₁ I) ((P E₂ h₂ J) ξ))).re

theorem CommutingRepetition.BorelCalc.νP_map_fst {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : MeasureTheory.Measure.map Prod.fst (νP E₁ E₂ h₁ h₂ hc ξ) = ν E₁ h₁ ξ

First marginal: the spectral measure of E₁ at ξ.

theorem CommutingRepetition.BorelCalc.νP_map_snd {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : MeasureTheory.Measure.map Prod.snd (νP E₁ E₂ h₁ h₂ hc ξ) = ν E₂ h₂ ξ

Second marginal: the spectral measure of E₂ at ξ.

theorem CommutingRepetition.BorelCalc.νP_univ_toReal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E₁ E₂ : 𝓗 →L[ℂ] 𝓗) (h₁ : IsSelfAdjoint E₁) (h₂ : IsSelfAdjoint E₂) (hc : Commute E₁ E₂) (ξ : 𝓗) : ((νP E₁ E₂ h₁ h₂ hc ξ) Set.univ).toReal = ‖ξ‖ ^ 2

Total mass ‖ξ‖².