Finite measures on ℝ and the transfer principle

theorem CommutingRepetition.BorelCalc.integrable_of_bdd {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : MeasureTheory.Integrable g μ

Bounded measurable real functions are integrable against finite measures.

theorem CommutingRepetition.BorelCalc.isFiniteMeasure_smul_of_ne_top {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {c : ENNReal} (hc : c ≠ ⊤) : MeasureTheory.IsFiniteMeasure (c • μ)

theorem CommutingRepetition.BorelCalc.isFiniteMeasure_finset_sum {ι : Type u_1} (s : Finset ι) (μ : ι → MeasureTheory.Measure ℝ) (h : ∀ (i : ι), MeasureTheory.IsFiniteMeasure (μ i)) : MeasureTheory.IsFiniteMeasure (∑ i ∈ s, μ i)

theorem CommutingRepetition.BorelCalc.integrable_finset_sum_measure {ι : Type u_1} (s : Finset ι) (μ : ι → MeasureTheory.Measure ℝ) {g : ℝ → ℝ} (hg : ∀ (i : ι), MeasureTheory.Integrable g (μ i)) : MeasureTheory.Integrable g (∑ i ∈ s, μ i)

theorem CommutingRepetition.BorelCalc.integral_finset_sum_measure' {ι : Type u_1} (s : Finset ι) (μ : ι → MeasureTheory.Measure ℝ) {g : ℝ → ℝ} (hg : ∀ (i : ι), MeasureTheory.Integrable g (μ i)) : ∫ (t : ℝ), g t ∂∑ i ∈ s, μ i = ∑ i ∈ s, ∫ (t : ℝ), g t ∂μ i

noncomputable def CommutingRepetition.BorelCalc.comb {n : ℕ} (m : Fin n → MeasureTheory.Measure ℝ) (a : Fin n → ℝ) : MeasureTheory.Measure ℝ

The positive part of a real combination of measures: ∑ (a k)⁺ • m k.

Equations

• CommutingRepetition.BorelCalc.comb m a = ∑ k : Fin n, ENNReal.ofReal (a k) • m k

instance CommutingRepetition.BorelCalc.comb_isFiniteMeasure {n : ℕ} (m : Fin n → MeasureTheory.Measure ℝ) [∀ (k : Fin n), MeasureTheory.IsFiniteMeasure (m k)] (a : Fin n → ℝ) : MeasureTheory.IsFiniteMeasure (comb m a)

theorem CommutingRepetition.BorelCalc.integral_comb {n : ℕ} (m : Fin n → MeasureTheory.Measure ℝ) (a : Fin n → ℝ) {g : ℝ → ℝ} (hg : ∀ (k : Fin n), MeasureTheory.Integrable g (m k)) : ∫ (t : ℝ), g t ∂comb m a = ∑ k : Fin n, max (a k) 0 * ∫ (t : ℝ), g t ∂m k

theorem CommutingRepetition.BorelCalc.transfer {n : ℕ} (m : Fin n → MeasureTheory.Measure ℝ) [∀ (k : Fin n), MeasureTheory.IsFiniteMeasure (m k)] (a : Fin n → ℝ) (h : ∀ (g : ℝ → ℝ), Continuous g → ∑ k : Fin n, a k * ∫ (t : ℝ), g t ∂m k = 0) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : ∑ k : Fin n, a k * ∫ (t : ℝ), g t ∂m k = 0

Transfer principle (real coefficients): a real-linear identity among the integrals of finitely many finite measures on ℝ valid for all continuous test functions is valid for all bounded Borel functions.

theorem CommutingRepetition.BorelCalc.transferC {n : ℕ} (m : Fin n → MeasureTheory.Measure ℝ) [∀ (k : Fin n), MeasureTheory.IsFiniteMeasure (m k)] (a : Fin n → ℂ) (h : ∀ (g : ℝ → ℝ), Continuous g → ∑ k : Fin n, a k * ↑(∫ (t : ℝ), g t ∂m k) = 0) {g : ℝ → ℝ} (hg : Measurable g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : ∑ k : Fin n, a k * ↑(∫ (t : ℝ), g t ∂m k) = 0

Transfer principle (complex coefficients).

Self-adjoint operators: elementary inner-product facts

theorem CommutingRepetition.BorelCalc.inner_sa {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 →L[ℂ] 𝓗} (hT : IsSelfAdjoint T) (x y : 𝓗) : inner ℂ x (T y) = inner ℂ (T x) y

theorem CommutingRepetition.BorelCalc.inner_self_real {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 →L[ℂ] 𝓗} (hT : IsSelfAdjoint T) (ξ : 𝓗) : ↑(inner ℂ ξ (T ξ)).re = inner ℂ ξ (T ξ)

The quadratic form of a self-adjoint operator is real.

theorem CommutingRepetition.BorelCalc.inner_self_im {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 →L[ℂ] 𝓗} (hT : IsSelfAdjoint T) (ξ : 𝓗) : (inner ℂ ξ (T ξ)).im = 0

The spectral measure of a vector state

noncomputable def CommutingRepetition.BorelCalc.stateLin {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : C(↑(spectrum ℝ E), ℝ) →ₗ[ℝ] ℝ

The vector state f ↦ re ⟪ξ, f(E) ξ⟫ on C(spectrum ℝ E, ℝ), real-linear.

Equations

• CommutingRepetition.BorelCalc.stateLin E hE ξ = { toFun := fun (f : C(↑(spectrum ℝ E), ℝ)) => (inner ℂ ξ (((cfcHom hE) f) ξ)).re, map_add' := ⋯, map_smul' := ⋯ }

theorem CommutingRepetition.BorelCalc.stateLin_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) (f : C(↑(spectrum ℝ E), ℝ)) : (stateLin E hE ξ) f = (inner ℂ ξ (((cfcHom hE) f) ξ)).re

theorem CommutingRepetition.BorelCalc.stateLin_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {f : C(↑(spectrum ℝ E), ℝ)} (hf : 0 ≤ f) : 0 ≤ (stateLin E hE ξ) f

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

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

Equations

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

theorem CommutingRepetition.BorelCalc.Λ_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) (f : CompactlySupportedContinuousMap ↑(spectrum ℝ E) ℝ) : (Λ E hE ξ) f = (inner ℂ ξ (((cfcHom hE) f.toContinuousMap) ξ)).re

noncomputable def CommutingRepetition.BorelCalc.ν₀ {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : MeasureTheory.Measure ↑(spectrum ℝ E)

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

Equations

• CommutingRepetition.BorelCalc.ν₀ E hE ξ = RealRMK.rieszMeasure (CommutingRepetition.BorelCalc.Λ E hE ξ)

instance CommutingRepetition.BorelCalc.ν₀_isFiniteMeasure {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : MeasureTheory.IsFiniteMeasure (ν₀ E hE ξ)

noncomputable def CommutingRepetition.BorelCalc.ν {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : MeasureTheory.Measure ℝ

The spectral measure of the vector state ξ for the self-adjoint operator E: the Riesz measure of f ↦ ⟪ξ, f(E) ξ⟫, pushed forward to ℝ.

Equations

• CommutingRepetition.BorelCalc.ν E hE ξ = MeasureTheory.Measure.map Subtype.val (CommutingRepetition.BorelCalc.ν₀ E hE ξ)

instance CommutingRepetition.BorelCalc.ν_isFiniteMeasure {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : MeasureTheory.IsFiniteMeasure (ν E hE ξ)

theorem CommutingRepetition.BorelCalc.integral_ν {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {g : ℝ → ℝ} (hg : Continuous g) : ∫ (t : ℝ), g t ∂ν E hE ξ = (inner ℂ ξ ((cfc g E) ξ)).re

The defining property: ∫ g dν_ξ = ⟪ξ, g(E) ξ⟫ for continuous g.

theorem CommutingRepetition.BorelCalc.integral_ν_complex {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {g : ℝ → ℝ} (hg : Continuous g) : ↑(∫ (t : ℝ), g t ∂ν E hE ξ) = inner ℂ ξ ((cfc g E) ξ)

theorem CommutingRepetition.BorelCalc.ν_compl_spectrum {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : (ν E hE ξ) (spectrum ℝ E)ᶜ = 0

The spectral measure is concentrated on the spectrum.

theorem CommutingRepetition.BorelCalc.ν_univ_toReal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : ((ν E hE ξ) Set.univ).toReal = ‖ξ‖ ^ 2

Total mass: ν_ξ(ℝ) = ‖ξ‖².

theorem CommutingRepetition.BorelCalc.ν_univ_real {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : (ν E hE ξ).real Set.univ = ‖ξ‖ ^ 2

theorem CommutingRepetition.BorelCalc.abs_integral_ν_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {g : ℝ → ℝ} {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : |∫ (t : ℝ), g t ∂ν E hE ξ| ≤ C * ‖ξ‖ ^ 2

Integrals against the spectral measure are bounded by C ‖ξ‖².

theorem CommutingRepetition.BorelCalc.integral_ν_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {g : ℝ → ℝ} (hg : ∀ (t : ℝ), 0 ≤ g t) : 0 ≤ ∫ (t : ℝ), g t ∂ν E hE ξ

theorem CommutingRepetition.BorelCalc.integral_ν_mono {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) {g h : ℝ → ℝ} (hg : Measurable g) (hh : Measurable h) {C : ℝ} (hgC : ∀ (t : ℝ), |g t| ≤ C) (hhC : ∀ (t : ℝ), |h t| ≤ C) (hgh : ∀ (t : ℝ), g t ≤ h t) : ∫ (t : ℝ), g t ∂ν E hE ξ ≤ ∫ (t : ℝ), h t ∂ν E hE ξ