Bounded Borel functions

def CommutingRepetition.BorelCalc.Bdd (g : ℝ → ℝ) : Prop

Bounded Borel functions on ℝ: the domain of the Borel functional calculus.

Equations

• CommutingRepetition.BorelCalc.Bdd g = (Measurable g ∧ ∃ (C : ℝ), ∀ (t : ℝ), |g t| ≤ C)

theorem CommutingRepetition.BorelCalc.Bdd.measurable {g : ℝ → ℝ} (hg : Bdd g) : Measurable g

theorem CommutingRepetition.BorelCalc.Bdd.integrable {g : ℝ → ℝ} (hg : Bdd g) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable g μ

theorem CommutingRepetition.BorelCalc.Bdd.const (c : ℝ) : Bdd fun (x : ℝ) => c

theorem CommutingRepetition.BorelCalc.Bdd.one : Bdd 1

theorem CommutingRepetition.BorelCalc.Bdd.zero : Bdd 0

theorem CommutingRepetition.BorelCalc.Bdd.add {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : Bdd (g + h)

theorem CommutingRepetition.BorelCalc.Bdd.neg {g : ℝ → ℝ} (hg : Bdd g) : Bdd (-g)

theorem CommutingRepetition.BorelCalc.Bdd.sub {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : Bdd (g - h)

theorem CommutingRepetition.BorelCalc.Bdd.mul {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : Bdd (g * h)

theorem CommutingRepetition.BorelCalc.Bdd.const_mul (c : ℝ) {g : ℝ → ℝ} (hg : Bdd g) : Bdd fun (t : ℝ) => c * g t

theorem CommutingRepetition.BorelCalc.Bdd.indicator {I : Set ℝ} (hI : MeasurableSet I) : Bdd (I.indicator 1)

theorem CommutingRepetition.BorelCalc.Bdd.of_continuous {g : ℝ → ℝ} (hg : Continuous g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) : Bdd g

theorem CommutingRepetition.BorelCalc.Bdd.measurableSet_of_indicator {I : Set ℝ} (h : Bdd (I.indicator 1)) : MeasurableSet I

theorem CommutingRepetition.BorelCalc.Bdd.of_compactlySupported (f : CompactlySupportedContinuousMap ℝ ℝ) : Bdd ⇑f

Combinations of finite measures and the transfer principle

def CommutingRepetition.BorelCalc.IsCombo (Φ : (ℝ → ℝ) → ℂ) : Prop

Φ is a combination: Φ g = (∫ g dμ₁ − ∫ g dμ₂) + i (∫ g dμ₃ − ∫ g dμ₄) for bounded Borel g, with μ₁, …, μ₄ finite measures on ℝ.

Equations

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

theorem CommutingRepetition.BorelCalc.IsCombo.integral (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : IsCombo fun (g : ℝ → ℝ) => ↑(∫ (t : ℝ), g t ∂μ)

theorem CommutingRepetition.BorelCalc.IsCombo.add {Φ Ψ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) (hΨ : IsCombo Ψ) : IsCombo fun (g : ℝ → ℝ) => Φ g + Ψ g

theorem CommutingRepetition.BorelCalc.IsCombo.smul_real (r : ℝ) {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) : IsCombo fun (g : ℝ → ℝ) => ↑r * Φ g

theorem CommutingRepetition.BorelCalc.IsCombo.smul_I {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) : IsCombo fun (g : ℝ → ℝ) => Complex.I * Φ g

theorem CommutingRepetition.BorelCalc.IsCombo.smul (c : ℂ) {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) : IsCombo fun (g : ℝ → ℝ) => c * Φ g

theorem CommutingRepetition.BorelCalc.IsCombo.neg {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) : IsCombo fun (g : ℝ → ℝ) => -Φ g

theorem CommutingRepetition.BorelCalc.IsCombo.sub {Φ Ψ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) (hΨ : IsCombo Ψ) : IsCombo fun (g : ℝ → ℝ) => Φ g - Ψ g

theorem CommutingRepetition.BorelCalc.IsCombo.conjugate {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) : IsCombo fun (g : ℝ → ℝ) => (starRingEnd ℂ) (Φ g)

theorem CommutingRepetition.BorelCalc.IsCombo.transfer {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) (h : ∀ (g : ℝ → ℝ), Continuous g → Bdd g → Φ g = 0) {g : ℝ → ℝ} (hg : Bdd g) : Φ g = 0

Transfer principle: a combination vanishing on all bounded continuous functions vanishes on all bounded Borel functions.

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

Two combinations agreeing on bounded continuous functions agree on bounded Borel functions.

Multiplying the test function by a fixed bounded Borel function

noncomputable def CommutingRepetition.BorelCalc.IsCombo.wd (μ : MeasureTheory.Measure ℝ) (h : ℝ → ℝ) : MeasureTheory.Measure ℝ

The measure h⁺ dμ.

Equations

• CommutingRepetition.BorelCalc.IsCombo.wd μ h = μ.withDensity fun (t : ℝ) => ↑(h t).toNNReal

theorem CommutingRepetition.BorelCalc.IsCombo.wd_isFiniteMeasure (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {h : ℝ → ℝ} (hh : Bdd h) : MeasureTheory.IsFiniteMeasure (wd μ h)

theorem CommutingRepetition.BorelCalc.IsCombo.integral_wd (μ : MeasureTheory.Measure ℝ) {h : ℝ → ℝ} (hh : Bdd h) (g : ℝ → ℝ) : ∫ (t : ℝ), g t ∂wd μ h = ∫ (t : ℝ), max (h t) 0 * g t ∂μ

theorem CommutingRepetition.BorelCalc.Bdd.max_zero {h : ℝ → ℝ} (hh : Bdd h) : Bdd fun (t : ℝ) => max (h t) 0

theorem CommutingRepetition.BorelCalc.IsCombo.integral_mul_eq_wd (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : ∫ (t : ℝ), (g * h) t ∂μ = ∫ (t : ℝ), g t ∂wd μ h - ∫ (t : ℝ), g t ∂wd μ (-h)

theorem CommutingRepetition.BorelCalc.IsCombo.mul_right {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) {h : ℝ → ℝ} (hh : Bdd h) : IsCombo fun (g : ℝ → ℝ) => Φ (g * h)

theorem CommutingRepetition.BorelCalc.IsCombo.mul_left {Φ : (ℝ → ℝ) → ℂ} (hΦ : IsCombo Φ) {h : ℝ → ℝ} (hh : Bdd h) : IsCombo fun (g : ℝ → ℝ) => Φ (h * g)

The polarized form

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

The quadratic form Q g ξ = ∫ g dν_ξ (as a complex number).

Equations

• CommutingRepetition.BorelCalc.Q E hE g ξ = ↑(∫ (t : ℝ), g t ∂CommutingRepetition.BorelCalc.ν E hE ξ)

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

The polarized form: pol g ξ η = ⟪ξ, g(E) η⟫ for continuous g.

Equations

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

theorem CommutingRepetition.BorelCalc.isCombo_Q {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : IsCombo fun (g : ℝ → ℝ) => Q E hE g ξ

theorem CommutingRepetition.BorelCalc.isCombo_pol {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ η : 𝓗) : IsCombo fun (g : ℝ → ℝ) => pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.pol_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Continuous g) (ξ η : 𝓗) : pol E hE g ξ η = inner ℂ ξ ((cfc g E) η)

theorem CommutingRepetition.BorelCalc.pol_add_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ ξ' η : 𝓗) : pol E hE g (ξ + ξ') η = pol E hE g ξ η + pol E hE g ξ' η

theorem CommutingRepetition.BorelCalc.pol_smul_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (c : ℂ) (ξ η : 𝓗) : pol E hE g (c • ξ) η = (starRingEnd ℂ) c * pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.pol_add_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ η η' : 𝓗) : pol E hE g ξ (η + η') = pol E hE g ξ η + pol E hE g ξ η'

theorem CommutingRepetition.BorelCalc.pol_smul_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (c : ℂ) (ξ η : 𝓗) : pol E hE g ξ (c • η) = c * pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.pol_conj {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : (starRingEnd ℂ) (pol E hE g η ξ) = pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.pol_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : pol E hE g ξ ξ = Q E hE g ξ

theorem CommutingRepetition.BorelCalc.pol_zero_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (η : 𝓗) : pol E hE g 0 η = 0

theorem CommutingRepetition.BorelCalc.pol_zero_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : pol E hE g ξ 0 = 0

Boundedness

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

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

theorem CommutingRepetition.BorelCalc.norm_pol_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) {C : ℝ} (hC : ∀ (t : ℝ), |g t| ≤ C) (ξ η : 𝓗) : ‖pol E hE g ξ η‖ ≤ 2 * C * ‖ξ‖ * ‖η‖

noncomputable def CommutingRepetition.BorelCalc.polForm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) : 𝓗 →L⋆[ℂ] 𝓗 →L[ℂ] ℂ

The polarized form as a bounded sesquilinear map.

Equations

• CommutingRepetition.BorelCalc.polForm E hE hg = (LinearMap.mk₂'ₛₗ (starRingEnd ℂ) (RingHom.id ℂ) (CommutingRepetition.BorelCalc.pol E hE g) ⋯ ⋯ ⋯ ⋯).mkContinuous₂ (2 * ⋯.choose) ⋯

theorem CommutingRepetition.BorelCalc.polForm_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : ((polForm E hE hg) ξ) η = pol E hE g ξ η

The Borel functional calculus

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

The Borel functional calculus g(E) for a bounded Borel function g (junk value 0 otherwise): the operator of the polarized form of the spectral measures.

Equations

• CommutingRepetition.BorelCalc.bfc E hE g = if hg : CommutingRepetition.BorelCalc.Bdd g then InnerProductSpace.continuousLinearMapOfBilin (CommutingRepetition.BorelCalc.polForm E hE hg) else 0

theorem CommutingRepetition.BorelCalc.bfc_of_not {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : ¬Bdd g) : bfc E hE g = 0

theorem CommutingRepetition.BorelCalc.inner_bfc_left {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : inner ℂ ((bfc E hE g) ξ) η = pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.inner_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ η : 𝓗) : inner ℂ ξ ((bfc E hE g) η) = pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.inner_bfc_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (ξ : 𝓗) : inner ℂ ξ ((bfc E hE g) ξ) = Q E hE g ξ

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

theorem CommutingRepetition.BorelCalc.ext_of_inner {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S T : 𝓗 →L[ℂ] 𝓗} (h : ∀ (ξ η : 𝓗), inner ℂ ξ (S η) = inner ℂ ξ (T η)) : S = T

theorem CommutingRepetition.BorelCalc.ext_of_inner_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {S T : 𝓗 →L[ℂ] 𝓗} (h : ∀ (ξ : 𝓗), inner ℂ ξ (S ξ) = inner ℂ ξ (T ξ)) : S = T

An operator is determined by its quadratic form.

theorem CommutingRepetition.BorelCalc.bfc_unique {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) {T : 𝓗 →L[ℂ] 𝓗} (h : ∀ (ξ η : 𝓗), inner ℂ ξ (T η) = pol E hE g ξ η) : T = bfc E hE g

theorem CommutingRepetition.BorelCalc.bfc_cfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (hc : Continuous g) : bfc E hE g = cfc g E

On bounded continuous functions the Borel calculus is the continuous one.

theorem CommutingRepetition.BorelCalc.bfc_congr_op {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] {E E' : 𝓗 →L[ℂ] 𝓗} (h : E = E') (hE : IsSelfAdjoint E) (hE' : IsSelfAdjoint E') (g : ℝ → ℝ) : bfc E hE g = bfc E' hE' g

Rewriting the operator inside bfc (the self-adjointness proof is transported).

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

Linearity

theorem CommutingRepetition.BorelCalc.Q_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ : 𝓗) : Q E hE (g + h) ξ = Q E hE g ξ + Q E hE h ξ

theorem CommutingRepetition.BorelCalc.Q_sub {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ : 𝓗) : Q E hE (g - h) ξ = Q E hE g ξ - Q E hE h ξ

theorem CommutingRepetition.BorelCalc.Q_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℝ) (g : ℝ → ℝ) (ξ : 𝓗) : Q E hE (fun (t : ℝ) => c * g t) ξ = ↑c * Q E hE g ξ

theorem CommutingRepetition.BorelCalc.pol_add_fun {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ η : 𝓗) : pol E hE (g + h) ξ η = pol E hE g ξ η + pol E hE h ξ η

theorem CommutingRepetition.BorelCalc.pol_sub_fun {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ η : 𝓗) : pol E hE (g - h) ξ η = pol E hE g ξ η - pol E hE h ξ η

theorem CommutingRepetition.BorelCalc.pol_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℝ) (g : ℝ → ℝ) (ξ η : 𝓗) : pol E hE (fun (t : ℝ) => c * g t) ξ η = ↑c * pol E hE g ξ η

theorem CommutingRepetition.BorelCalc.bfc_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : bfc E hE (g + h) = bfc E hE g + bfc E hE h

theorem CommutingRepetition.BorelCalc.bfc_sub {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : bfc E hE (g - h) = bfc E hE g - bfc E hE h

theorem CommutingRepetition.BorelCalc.bfc_const_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℝ) {g : ℝ → ℝ} (hg : Bdd g) : (bfc E hE fun (t : ℝ) => c * g t) = ↑c • bfc E hE g

theorem CommutingRepetition.BorelCalc.bfc_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : bfc E hE 1 = 1

theorem CommutingRepetition.BorelCalc.bfc_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) : bfc E hE 0 = 0

theorem CommutingRepetition.BorelCalc.bfc_const {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℝ) : (bfc E hE fun (x : ℝ) => c) = ↑c • 1

Multiplicativity

theorem CommutingRepetition.BorelCalc.cfc_mul_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) {g h : ℝ → ℝ} (hg : Continuous g) (hh : Continuous h) : cfc (g * h) E = cfc g E * cfc h E

theorem CommutingRepetition.BorelCalc.pol_bfc_right_cont {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hgc : Continuous g) (hg : Bdd g) (hh : Bdd h) (ξ η : 𝓗) : pol E hE g ξ ((bfc E hE h) η) = pol E hE (g * h) ξ η

Step 1: for continuous g and Borel h, by transfer in h.

theorem CommutingRepetition.BorelCalc.pol_bfc_right {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ η : 𝓗) : pol E hE g ξ ((bfc E hE h) η) = pol E hE (g * h) ξ η

Step 2: for Borel g and h, by transfer in g.

theorem CommutingRepetition.BorelCalc.bfc_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : bfc E hE (g * h) = bfc E hE g * bfc E hE h

Multiplicativity of the Borel functional calculus.

theorem CommutingRepetition.BorelCalc.bfc_comm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) : bfc E hE g * bfc E hE h = bfc E hE h * bfc E hE g

theorem CommutingRepetition.BorelCalc.integral_ν_bfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (ξ : 𝓗) : ∫ (t : ℝ), g t ∂ν E hE ((bfc E hE h) ξ) = ∫ (t : ℝ), (h * g * h) t ∂ν E hE ξ

The spectral measure of h(E) ξ: ∫ g dν_{h(E)ξ} = ∫ g h² dν_ξ.

Order

theorem CommutingRepetition.BorelCalc.bfc_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (h0 : ∀ (t : ℝ), 0 ≤ g t) : 0 ≤ bfc E hE g

theorem CommutingRepetition.BorelCalc.bfc_mono {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g h : ℝ → ℝ} (hg : Bdd g) (hh : Bdd h) (hle : ∀ (t : ℝ), g t ≤ h t) : bfc E hE g ≤ bfc E hE h

theorem CommutingRepetition.BorelCalc.bfc_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (h1 : ∀ (t : ℝ), g t ≤ 1) : bfc E hE g ≤ 1

theorem CommutingRepetition.BorelCalc.bfc_norm_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {g : ℝ → ℝ} (hg : Bdd g) (h0 : ∀ (t : ℝ), 0 ≤ g t) (h1 : ∀ (t : ℝ), g t ≤ 1) : ‖bfc E hE g‖ ≤ 1