The inverse of θ on (0,2)

noncomputable def CommutingRepetition.VN.Modular.θinv (u : ℝ) : ℝ

θinv u = 2 / (1 + e^u), the inverse of θ on (0,2).

Equations

• CommutingRepetition.VN.Modular.θinv u = 2 / (1 + Real.exp u)

theorem CommutingRepetition.VN.Modular.continuous_θinv : Continuous θinv

theorem CommutingRepetition.VN.Modular.measurable_θinv : Measurable θinv

theorem CommutingRepetition.VN.Modular.θinv_θ {l : ℝ} (hl : l ∈ Set.Ioo 0 2) : θinv (θ l) = l

Measures on (0,2) are determined by their θ-Fourier transforms

theorem CommutingRepetition.VN.Modular.ae_mem_Ioo_of_compl_eq_zero {μ : MeasureTheory.Measure ℝ} (hμ : μ (Set.Ioo 0 2)ᶜ = 0) : ∀ᵐ (l : ℝ) ∂μ, l ∈ Set.Ioo 0 2

theorem CommutingRepetition.VN.Modular.integral_eq_integral_map_θ {μ : MeasureTheory.Measure ℝ} (hμ : μ (Set.Ioo 0 2)ᶜ = 0) {g : ℝ → ℝ} (hg : Measurable g) : ∫ (l : ℝ), g l ∂μ = ∫ (u : ℝ), g (θinv u) ∂MeasureTheory.Measure.map θ μ

theorem CommutingRepetition.VN.Modular.bdd_cos_θ (t : ℝ) : BorelCalc.Bdd fun (l : ℝ) => Real.cos (t * θ l)

theorem CommutingRepetition.VN.Modular.bdd_sin_θ (t : ℝ) : BorelCalc.Bdd fun (l : ℝ) => Real.sin (t * θ l)

theorem CommutingRepetition.VN.Modular.integral_eq_of_cos_sin {μ μ' : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure μ'] (hμ : μ (Set.Ioo 0 2)ᶜ = 0) (hμ' : μ' (Set.Ioo 0 2)ᶜ = 0) (hcos : ∀ (t : ℝ), ∫ (l : ℝ), Real.cos (t * θ l) ∂μ = ∫ (l : ℝ), Real.cos (t * θ l) ∂μ') (hsin : ∀ (t : ℝ), ∫ (l : ℝ), Real.sin (t * θ l) ∂μ = ∫ (l : ℝ), Real.sin (t * θ l) ∂μ') {g : ℝ → ℝ} (hg : Measurable g) : ∫ (l : ℝ), g l ∂μ = ∫ (l : ℝ), g l ∂μ'

Two finite measures concentrated on (0,2) with the same integrals of cos(tθ) and sin(tθ) for all t have the same integrals of every bounded Borel function.

Transfer to combinations of finite measures

theorem CommutingRepetition.VN.Modular.isFiniteMeasure_restrict_Ioo (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (μ.restrict (Set.Ioo 0 2))

theorem CommutingRepetition.VN.Modular.restrict_Ioo_compl (μ : MeasureTheory.Measure ℝ) : (μ.restrict (Set.Ioo 0 2)) (Set.Ioo 0 2)ᶜ = 0

theorem CommutingRepetition.VN.Modular.Bdd.indicator_of_bdd {s : Set ℝ} (hs : MeasurableSet s) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : BorelCalc.Bdd (s.indicator g)

theorem CommutingRepetition.VN.Modular.IsCombo.eq_zero_of_cos_sin {Φ : (ℝ → ℝ) → ℂ} (hΦ : BorelCalc.IsCombo Φ) (h0 : ∀ (g : ℝ → ℝ), BorelCalc.Bdd g → Φ ((Set.Ioo 0 2)ᶜ.indicator g) = 0) (hcos : ∀ (t : ℝ), (Φ fun (l : ℝ) => Real.cos (t * θ l)) = 0) (hsin : ∀ (t : ℝ), (Φ fun (l : ℝ) => Real.sin (t * θ l)) = 0) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : Φ g = 0

A combination of finite measures that vanishes on everything supported off (0,2) and on cos(tθ), sin(tθ) for all t vanishes on every bounded Borel function.

Operators: spectral projections at the endpoints

noncomputable def CommutingRepetition.VN.Modular.trunc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (l : ℝ) : ℝ

The truncation of the identity to [-‖E‖, ‖E‖]; equal to id on the spectrum.

Equations

• CommutingRepetition.VN.Modular.trunc E l = max (-‖E‖) (min l ‖E‖)

theorem CommutingRepetition.VN.Modular.continuous_trunc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) : Continuous (trunc E)

theorem CommutingRepetition.VN.Modular.bdd_trunc {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) : BorelCalc.Bdd (trunc E)

theorem CommutingRepetition.VN.Modular.trunc_of_mem {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) {l : ℝ} (hl : l ∈ Set.Icc (-‖E‖) ‖E‖) : trunc E l = l

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

theorem CommutingRepetition.VN.Modular.E_mul_P_singleton {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (c : ℝ) : E * BorelCalc.P E hE {c} = ↑c • BorelCalc.P E hE {c}

E P{c} = c P{c}: the spectral projection at a point is the eigenprojection.

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

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

theorem CommutingRepetition.VN.Modular.ν_compl_Ioo_eq_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (hspec : spectrum ℝ E ⊆ Set.Icc 0 2) (h0 : ∀ (ξ : 𝓗), E ξ = ↑0 • ξ → ξ = 0) (h2 : ∀ (ξ : 𝓗), E ξ = ↑2 • ξ → ξ = 0) (ξ : 𝓗) : (BorelCalc.ν E hE ξ) (Set.Ioo 0 2)ᶜ = 0

If the spectrum lies in [0,2] and 0, 2 are not eigenvalues, the spectral measures give no mass to (0,2)ᶜ.

theorem CommutingRepetition.VN.Modular.P_compl_Ioo_eq_zero {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (hspec : spectrum ℝ E ⊆ Set.Icc 0 2) (h0 : ∀ (ξ : 𝓗), E ξ = ↑0 • ξ → ξ = 0) (h2 : ∀ (ξ : 𝓗), E ξ = ↑2 • ξ → ξ = 0) : BorelCalc.P E hE (Set.Ioo 0 2)ᶜ = 0

If the spectrum lies in [0,2] and 0, 2 are not eigenvalues, the spectral projection of (0,2)ᶜ vanishes.

The Fourier converse for a self-adjoint operator with spectral measures on (0,2)

theorem CommutingRepetition.VN.Modular.re_gDel (t l : ℝ) : (gDel t l).re = Real.cos (t * θ l)

theorem CommutingRepetition.VN.Modular.im_gDel (t l : ℝ) : (gDel t l).im = Real.sin (t * θ l)

theorem CommutingRepetition.VN.Modular.cbfc_gDel_eq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (t : ℝ) : BorelCalc.cbfc E hE (gDel t) = (BorelCalc.bfc E hE fun (l : ℝ) => Real.cos (t * θ l)) + Complex.I • BorelCalc.bfc E hE fun (l : ℝ) => Real.sin (t * θ l)

cbfc (gDel t) = bfc (cos(tθ)) + i bfc (sin(tθ)).

theorem CommutingRepetition.VN.Modular.cbfc_gDel_neg_eq {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (t : ℝ) : BorelCalc.cbfc E hE (gDel (-t)) = (BorelCalc.bfc E hE fun (l : ℝ) => Real.cos (t * θ l)) - Complex.I • BorelCalc.bfc E hE fun (l : ℝ) => Real.sin (t * θ l)

theorem CommutingRepetition.VN.Modular.commute_bfc_cos_sin {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) {x : 𝓗 →L[ℂ] 𝓗} (hx : ∀ (t : ℝ), Commute x (BorelCalc.cbfc E hE (gDel t))) (t : ℝ) : Commute x (BorelCalc.bfc E hE fun (l : ℝ) => Real.cos (t * θ l)) ∧ Commute x (BorelCalc.bfc E hE fun (l : ℝ) => Real.sin (t * θ l))

Commuting with e^{itθ(E)} for t and −t gives commutation with cos(tθ(E)), sin(tθ(E)).

theorem CommutingRepetition.VN.Modular.commute_bfc_of_commute_cbfc_gDel {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (hP : BorelCalc.P E hE (Set.Ioo 0 2)ᶜ = 0) {x : 𝓗 →L[ℂ] 𝓗} (hx : ∀ (t : ℝ), Commute x (BorelCalc.cbfc E hE (gDel t))) {g : ℝ → ℝ} (hg : BorelCalc.Bdd g) : Commute x (BorelCalc.bfc E hE g)

The Fourier converse: an operator commuting with every e^{itθ(E)} commutes with every bounded Borel function of E, when the spectral measures of E live on (0,2).

theorem CommutingRepetition.VN.Modular.commute_of_commute_cbfc_gDel {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace ℂ 𝓗] [CompleteSpace 𝓗] (E : 𝓗 →L[ℂ] 𝓗) (hE : IsSelfAdjoint E) (hP : BorelCalc.P E hE (Set.Ioo 0 2)ᶜ = 0) {x : 𝓗 →L[ℂ] 𝓗} (hx : ∀ (t : ℝ), Commute x (BorelCalc.cbfc E hE (gDel t))) : Commute x E

The modular group

theorem CommutingRepetition.VN.Modular.P_R_compl_Ioo {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : BorelCalc.P (R M Ω) ⋯ (Set.Ioo 0 2)ᶜ = 0

theorem CommutingRepetition.VN.Modular.ν_R_compl_Ioo {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ζ : K) : (BorelCalc.ν (R M Ω) ⋯ ζ) (Set.Ioo 0 2)ᶜ = 0

The spectral measures of R give no mass to (0,2)ᶜ.

theorem CommutingRepetition.VN.Modular.commute_R_of_commute_Δit {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : K →L[ℂ] K} (h : ∀ (t : ℝ), Commute x (Δit M Ω t)) : Commute x (R M Ω)

Fourier converse for the modular group: commuting with every Δ^{it} means commuting with R (the converse of σ_eq_self_of_commute_R).

theorem CommutingRepetition.VN.Modular.isCentral_of_σ_eq_self {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {x : K →L[ℂ] K} (hx : x ∈ M) (h : ∀ (t : ℝ), σ M Ω t x = x) : IsCentral M Ω x

A fixed point of the modular group in M is central.