Bounded measurable complex functions

def CommutingRepetition.BorelCalc.CBdd (G : ℝ → ℂ) : Prop

Bounded measurable complex-valued functions on ℝ.

Equations

• CommutingRepetition.BorelCalc.CBdd G = (Measurable G ∧ ∃ (C : ℝ), ∀ (t : ℝ), ‖G t‖ ≤ C)

theorem CommutingRepetition.BorelCalc.CBdd.measurable {G : ℝ → ℂ} (hG : CBdd G) : Measurable G

theorem CommutingRepetition.BorelCalc.CBdd.re {G : ℝ → ℂ} (hG : CBdd G) : Bdd fun (t : ℝ) => (G t).re

theorem CommutingRepetition.BorelCalc.CBdd.im {G : ℝ → ℂ} (hG : CBdd G) : Bdd fun (t : ℝ) => (G t).im

theorem CommutingRepetition.BorelCalc.CBdd.const (z : ℂ) : CBdd fun (x : ℝ) => z

theorem CommutingRepetition.BorelCalc.CBdd.one : CBdd fun (x : ℝ) => 1

theorem CommutingRepetition.BorelCalc.CBdd.ofReal {g : ℝ → ℝ} (hg : Bdd g) : CBdd fun (t : ℝ) => ↑(g t)

theorem CommutingRepetition.BorelCalc.CBdd.add {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : CBdd (G + H)

theorem CommutingRepetition.BorelCalc.CBdd.sub {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : CBdd (G - H)

theorem CommutingRepetition.BorelCalc.CBdd.mul {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : CBdd (G * H)

theorem CommutingRepetition.BorelCalc.CBdd.conjugate {G : ℝ → ℂ} (hG : CBdd G) : CBdd fun (t : ℝ) => (starRingEnd ℂ) (G t)

theorem CommutingRepetition.BorelCalc.CBdd.smul {G : ℝ → ℂ} (c : ℂ) (hG : CBdd G) : CBdd fun (t : ℝ) => c * G t

theorem CommutingRepetition.BorelCalc.CBdd.norm_sq {G : ℝ → ℂ} (hG : CBdd G) : Bdd fun (t : ℝ) => ‖G t‖ ^ 2

theorem CommutingRepetition.BorelCalc.CBdd.integrable {G : ℝ → ℂ} (hG : CBdd G) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable G μ

The complex Borel calculus

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

G(E) := (Re G)(E) + i (Im G)(E).

Equations

• CommutingRepetition.BorelCalc.cbfc E hE G = (CommutingRepetition.BorelCalc.bfc E hE fun (t : ℝ) => (G t).re) + Complex.I • CommutingRepetition.BorelCalc.bfc E hE fun (t : ℝ) => (G t).im

theorem CommutingRepetition.BorelCalc.cbfc_ofReal {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (g : ℝ → ℝ) : (cbfc E hE fun (t : ℝ) => ↑(g t)) = bfc E hE g

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

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

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

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

theorem CommutingRepetition.BorelCalc.cbfc_add {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : cbfc E hE (G + H) = cbfc E hE G + cbfc E hE H

theorem CommutingRepetition.BorelCalc.cbfc_sub {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : cbfc E hE (G - H) = cbfc E hE G - cbfc E hE H

theorem CommutingRepetition.BorelCalc.cbfc_mul {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : cbfc E hE (G * H) = cbfc E hE G * cbfc E hE H

theorem CommutingRepetition.BorelCalc.cbfc_star {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : CBdd G) : star (cbfc E hE G) = cbfc E hE fun (t : ℝ) => (starRingEnd ℂ) (G t)

theorem CommutingRepetition.BorelCalc.cbfc_comm {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G H : ℝ → ℂ} (hG : CBdd G) (hH : CBdd H) : cbfc E hE G * cbfc E hE H = cbfc E hE H * cbfc E hE G

theorem CommutingRepetition.BorelCalc.inner_cbfc_self {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : CBdd G) (ξ : 𝓗) : inner ℂ ξ ((cbfc E hE G) ξ) = ∫ (t : ℝ), G t ∂ν E hE ξ

⟪ξ, G(E) ξ⟫ = ∫ G dν_ξ.

theorem CommutingRepetition.BorelCalc.norm_sq_cbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : CBdd G) (ξ : 𝓗) : ‖(cbfc E hE G) ξ‖ ^ 2 = ∫ (t : ℝ), ‖G t‖ ^ 2 ∂ν E hE ξ

‖G(E) ξ‖² = ∫ |G|² dν_ξ.

theorem CommutingRepetition.BorelCalc.norm_cbfc_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : CBdd G) {C : ℝ} (hC0 : 0 ≤ C) (hC : ∀ (t : ℝ), ‖G t‖ ≤ C) : ‖cbfc E hE G‖ ≤ C

Norm bound: ‖G(E)‖ ≤ sup |G|.

Eigenvectors

theorem CommutingRepetition.BorelCalc.ae_norm_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (ξ : 𝓗) : ∀ᵐ (t : ℝ) ∂ν E hE ξ, |t| ≤ ‖E‖

The spectral measure is concentrated on [-‖E‖, ‖E‖].

theorem CommutingRepetition.BorelCalc.ae_eq_of_eigen {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {ξ : 𝓗} {c : ℝ} (hξ : E ξ = ↑c • ξ) : ∀ᵐ (t : ℝ) ∂ν E hE ξ, t = c

The spectral measure of an eigenvector is concentrated at the eigenvalue.

theorem CommutingRepetition.BorelCalc.cbfc_eigen {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G : ℝ → ℂ} (hG : CBdd G) {ξ : 𝓗} {c : ℝ} (hξ : E ξ = ↑c • ξ) : (cbfc E hE G) ξ = G c • ξ

E ξ = c ξ implies G(E) ξ = G(c) ξ.

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

Commutation, membership, dominated convergence

theorem CommutingRepetition.BorelCalc.commute_cbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {T : 𝓗 →L[ℂ] 𝓗} (hT : Commute E T) {G : ℝ → ℂ} (hG : CBdd G) : Commute (cbfc E hE G) T

theorem CommutingRepetition.BorelCalc.cbfc_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (N : VonNeumannAlgebra 𝓗) (hEN : E ∈ N) {G : ℝ → ℂ} (hG : CBdd G) : cbfc E hE G ∈ N

theorem CommutingRepetition.BorelCalc.tendsto_cbfc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {ι : Type u_2} {l : Filter ι} [l.IsCountablyGenerated] {G : ι → ℝ → ℂ} {Ginf : ℝ → ℂ} (hG : ∀ (i : ι), CBdd (G i)) (hGinf : CBdd Ginf) {C : ℝ} (hC : ∀ (i : ι) (t : ℝ), ‖G i t‖ ≤ C) (hCinf : ∀ (t : ℝ), ‖Ginf t‖ ≤ C) (hlim : ∀ (t : ℝ), Filter.Tendsto (fun (i : ι) => G i t) l (nhds (Ginf t))) (ξ : 𝓗) : Filter.Tendsto (fun (i : ι) => (cbfc E hE (G i)) ξ) l (nhds ((cbfc E hE Ginf) ξ))

Dominated convergence: uniformly bounded G i → Ginf pointwise gives G i (E) ξ → Ginf(E) ξ.