No atoms at non-eigenvalues; Borel functions equal a.e. give the same operator

theorem CommutingRepetition.BorelCalc.P_singleton_eq_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {c : ℝ} (hinj : ∀ (x : 𝓗), E x = ↑c • x → x = 0) : P E hE {c} = 0

If E − c is injective, the spectral projection of {c} vanishes.

theorem CommutingRepetition.BorelCalc.ν_singleton_eq_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {c : ℝ} (hinj : ∀ (x : 𝓗), E x = ↑c • x → x = 0) (ξ : 𝓗) : (ν E hE ξ) {c} = 0

No atom of the spectral measures at a non-eigenvalue.

theorem CommutingRepetition.BorelCalc.cbfc_congr_ae {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {G G' : ℝ → ℂ} (hG : CBdd G) (hG' : CBdd G') (h : ∀ (ξ : 𝓗), G =ᵐ[ν E hE ξ] G') : cbfc E hE G = cbfc E hE G'

Borel functions which agree a.e. for every spectral measure give the same operator.

The scalar functions gE z = e^{zθ} gT

noncomputable def CommutingRepetition.VN.Modular.gE (z : ℂ) (l : ℝ) : ℂ

gE z l = e^{z θ(l)} gT(l).

Equations

• CommutingRepetition.VN.Modular.gE z l = Complex.exp (z * ↑(CommutingRepetition.VN.Modular.θ l)) * ↑(CommutingRepetition.VN.Modular.gT l)

theorem CommutingRepetition.VN.Modular.measurable_gE (z : ℂ) : Measurable (gE z)

theorem CommutingRepetition.VN.Modular.norm_gE (z : ℂ) (l : ℝ) : ‖gE z l‖ = Real.exp (z.re * θ l) * gT l

theorem CommutingRepetition.VN.Modular.gT_eq_zero_of_notMem {l : ℝ} (hl : l ∉ Set.Ioo 0 2) : gT l = 0

theorem CommutingRepetition.VN.Modular.θ_of_mem {l : ℝ} (hl : l ∈ Set.Ioo 0 2) : θ l = Real.log ((2 - l) / l)

theorem CommutingRepetition.VN.Modular.θ_of_notMem {l : ℝ} (hl : l ∉ Set.Ioo 0 2) : θ l = 0

theorem CommutingRepetition.VN.Modular.exp_half_θ_mul_gT {l : ℝ} (hl : l ∈ Set.Ioo 0 2) : Real.exp (θ l / 2) * gT l = 2 - l

e^{θ/2} gT = 2 − l on (0, 2).

theorem CommutingRepetition.VN.Modular.exp_neg_half_θ_mul_gT {l : ℝ} (hl : l ∈ Set.Ioo 0 2) : Real.exp (-(θ l / 2)) * gT l = l

e^{-θ/2} gT = l on (0, 2).

theorem CommutingRepetition.VN.Modular.exp_abs_half_θ_mul_gT_le (l : ℝ) : Real.exp (|θ l| / 2) * gT l ≤ 2

e^{|θ|/2} gT ≤ 2.

theorem CommutingRepetition.VN.Modular.norm_gE_le {z : ℂ} (hz : |z.re| ≤ 1 / 2) (l : ℝ) : ‖gE z l‖ ≤ 2

‖gE z l‖ ≤ 2 on the closed strip.

theorem CommutingRepetition.VN.Modular.mul_exp_neg_le {a s : ℝ} (ha : 0 < a) (hs : 0 ≤ s) : s * Real.exp (-(a * s)) ≤ 1 / a

s e^{-a s} ≤ 1/a for a > 0, s ≥ 0.

theorem CommutingRepetition.VN.Modular.norm_θ_mul_gE_le {z : ℂ} {δ : ℝ} (hδ : 0 < δ) (hz : |z.re| ≤ 1 / 2 - δ) (l : ℝ) : ‖↑(θ l) * gE z l‖ ≤ 2 / δ

‖θ gE z‖ ≤ 2/δ for |Re z| ≤ 1/2 − δ.

theorem CommutingRepetition.VN.Modular.norm_exp_sub_one_div_le {h : ℂ} (hh : h ≠ 0) (θ₀ : ℝ) : ‖(Complex.exp (h * ↑θ₀) - 1) / h‖ ≤ |θ₀| * (Real.exp (‖h‖ * |θ₀|) + 2)

‖(e^{w} − 1)/h‖ ≤ |θ|(e^{|h||θ|} + 2) for w = h θ, h ≠ 0.

theorem CommutingRepetition.VN.Modular.norm_gE_quotient_le {z₀ h : ℂ} {δ : ℝ} (hδ : 0 < δ) (hz : |z₀.re| ≤ 1 / 2 - δ) (hh : ‖h‖ ≤ δ / 2) (hh0 : h ≠ 0) (l : ℝ) : ‖(gE (z₀ + h) l - gE z₀ l) / h‖ ≤ 12 / δ

The difference quotient bound: for |Re z₀| = 1/2 − δ and ‖h‖ ≤ δ/2, ‖(gE (z₀ + h) l − gE z₀ l)/h‖ ≤ 12/δ.

The operator family E(z)

theorem CommutingRepetition.VN.Modular.cbdd_gE {z : ℂ} (hz : |z.re| ≤ 1 / 2) : BorelCalc.CBdd (gE z)

theorem CommutingRepetition.BorelCalc.cbfc_const_mul' {𝓗 : Type u_2} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℂ) {H : ℝ → ℂ} (hH : CBdd H) : (cbfc E hE fun (t : ℝ) => c * H t) = c • cbfc E hE H

cbfc (c * H) = c • cbfc H.

noncomputable def CommutingRepetition.VN.Modular.Efam {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (z : ℂ) : K →L[ℂ] K

The analytic family E(z) = cbfc(R)(e^{zθ} gT).

Equations

• CommutingRepetition.VN.Modular.Efam M Ω z = CommutingRepetition.BorelCalc.cbfc (CommutingRepetition.VN.Modular.R M Ω) ⋯ (CommutingRepetition.VN.Modular.gE z)

noncomputable def CommutingRepetition.VN.Modular.Efam' {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (z : ℂ) : K →L[ℂ] K

Its derivative E'(z) = cbfc(R)(θ e^{zθ} gT).

Equations

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

theorem CommutingRepetition.VN.Modular.norm_Efam_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {z : ℂ} (hz : |z.re| ≤ 1 / 2) : ‖Efam M Ω z‖ ≤ 2

theorem CommutingRepetition.VN.Modular.norm_Efam_apply_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {z : ℂ} (hz : |z.re| ≤ 1 / 2) (ξ : K) : ‖(Efam M Ω z) ξ‖ ≤ 2 * ‖ξ‖

theorem CommutingRepetition.VN.Modular.Efam_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : Efam M Ω 0 = Tm M Ω

theorem CommutingRepetition.VN.Modular.star_Efam {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {z : ℂ} (hz : |z.re| ≤ 1 / 2) : star (Efam M Ω z) = Efam M Ω ((starRingEnd ℂ) z)

theorem CommutingRepetition.VN.Modular.Jm_Efam {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {z : ℂ} (hz : |z.re| ≤ 1 / 2) (ξ : K) : (Jm M Ω) ((Efam M Ω z) ξ) = (Efam M Ω (-(starRingEnd ℂ) z)) ((Jm M Ω) ξ)

J E(z) = E(-z̄) J.

The spectral measures of R live on (0, 2)

theorem CommutingRepetition.VN.Modular.ae_mem_Ioo {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ξ : K) : ∀ᵐ (l : ℝ) ∂BorelCalc.ν (R M Ω) ⋯ ξ, l ∈ Set.Ioo 0 2

Boundary values

noncomputable def CommutingRepetition.VN.Modular.g₁ (l : ℝ) : ℝ

g₁ l = l on [0, 2], bounded continuous.

Equations

• CommutingRepetition.VN.Modular.g₁ l = CommutingRepetition.VN.Modular.clamp 1 (l - 1) + 1

noncomputable def CommutingRepetition.VN.Modular.g₂ (l : ℝ) : ℝ

g₂ l = 2 − l on [0, 2], bounded continuous.

Equations

• CommutingRepetition.VN.Modular.g₂ l = 2 - CommutingRepetition.VN.Modular.g₁ l

theorem CommutingRepetition.VN.Modular.g₁_eq {l : ℝ} (hl : l ∈ Set.Icc 0 2) : g₁ l = l

theorem CommutingRepetition.VN.Modular.g₂_eq {l : ℝ} (hl : l ∈ Set.Icc 0 2) : g₂ l = 2 - l

theorem CommutingRepetition.VN.Modular.continuous_g₁ : Continuous g₁

theorem CommutingRepetition.VN.Modular.continuous_g₂ : Continuous g₂

theorem CommutingRepetition.VN.Modular.bdd_g₁ : BorelCalc.Bdd g₁

theorem CommutingRepetition.VN.Modular.bdd_g₂ : BorelCalc.Bdd g₂

theorem CommutingRepetition.VN.Modular.bfc_g₁ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : BorelCalc.bfc (R M Ω) ⋯ g₁ = R M Ω

theorem CommutingRepetition.VN.Modular.bfc_g₂ {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : BorelCalc.bfc (R M Ω) ⋯ g₂ = 2 - R M Ω

theorem CommutingRepetition.VN.Modular.re_half_add (t : ℝ) : |(1 / 2 + ↑t * Complex.I).re| ≤ 1 / 2

theorem CommutingRepetition.VN.Modular.re_neg_half_add (t : ℝ) : |(-1 / 2 + ↑t * Complex.I).re| ≤ 1 / 2

theorem CommutingRepetition.VN.Modular.Efam_half_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) : Efam M Ω (1 / 2 + ↑t * Complex.I) = (2 - R M Ω) * Δit M Ω t

E(1/2 + it) = (2 − R) Δ^{it}.

theorem CommutingRepetition.VN.Modular.Efam_neg_half_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) : Efam M Ω (-1 / 2 + ↑t * Complex.I) = R M Ω * Δit M Ω t

E(-1/2 + it) = R Δ^{it}.

Continuity on the closed strip and analyticity on the open strip

theorem CommutingRepetition.VN.Modular.continuous_gE_left (l : ℝ) : Continuous fun (z : ℂ) => gE z l

theorem CommutingRepetition.VN.Modular.continuousOn_Efam_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω ξ : K) : ContinuousOn (fun (z : ℂ) => (Efam M Ω z) ξ) StripCauchy.strip

z ↦ E(z) ξ is continuous on the closed strip.

theorem CommutingRepetition.VN.Modular.mem_strip_of_close {z₀ y : ℂ} {δ : ℝ} (hz : |z₀.re| ≤ 1 / 2 - δ) (hy : ‖y - z₀‖ ≤ δ / 2) (hδ : 0 < δ) : |y.re| ≤ 1 / 2

theorem CommutingRepetition.VN.Modular.hasDerivAt_Efam_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {z₀ : ℂ} (hz₀ : |z₀.re| < 1 / 2) (ξ : K) : HasDerivAt (fun (z : ℂ) => (Efam M Ω z) ξ) ((Efam' M Ω z₀) ξ) z₀

z ↦ E(z) ξ is complex differentiable on the open strip, with derivative E'(z) ξ.