The smearing operator ∫ a(t) U(t) dt

theorem CommutingRepetition.VN.Modular.integrable_smul_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) (ξ : K) : MeasureTheory.Integrable (fun (t : ℝ) => a t • (U t) ξ) MeasureTheory.volume

noncomputable def CommutingRepetition.VN.Modular.smear {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) : K →L[ℂ] K

The smearing operator ξ ↦ ∫ a(t) U(t) ξ dt of a uniformly bounded strongly continuous family U against an integrable weight a.

Equations

• CommutingRepetition.VN.Modular.smear a ha U hUc hUb = { toFun := fun (ξ : K) => ∫ (t : ℝ), a t • (U t) ξ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ((∫ (t : ℝ), ‖a t‖) * C) ⋯

theorem CommutingRepetition.VN.Modular.smear_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) (ξ : K) : (smear a ha U hUc hUb) ξ = ∫ (t : ℝ), a t • (U t) ξ

theorem CommutingRepetition.VN.Modular.norm_smear_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) : ‖smear a ha U hUc hUb‖ ≤ (∫ (t : ℝ), ‖a t‖) * C

theorem CommutingRepetition.VN.Modular.inner_smear {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) (η ξ : K) : inner ℂ η ((smear a ha U hUc hUb) ξ) = ∫ (t : ℝ), a t * inner ℂ η ((U t) ξ)

theorem CommutingRepetition.VN.Modular.clm_smear {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) (S : K →L[ℂ] K) (ξ : K) : S ((smear a ha U hUc hUb) ξ) = ∫ (t : ℝ), a t • S ((U t) ξ)

theorem CommutingRepetition.VN.Modular.smear_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (a : ℝ → ℂ) (ha : MeasureTheory.Integrable a MeasureTheory.volume) (U : ℝ → K →L[ℂ] K) {C : ℝ} (hUc : ∀ (v : K), Continuous fun (t : ℝ) => (U t) v) (hUb : ∀ (t : ℝ), ‖U t‖ ≤ C) (N : VonNeumannAlgebra K) (hU : ∀ (t : ℝ), U t ∈ N) : smear a ha U hUc hUb ∈ N

Smearing a family of elements of a von Neumann algebra stays in it.

Exchange: ∫ a(t) Δ^{it} ζ dt = â(θ)(R) ζ

theorem CommutingRepetition.VN.Modular.measurable_gDel_uncurry : Measurable fun (z : ℝ × ℝ) => gDel z.1 z.2

theorem CommutingRepetition.VN.Modular.integrable_mul_gDel {a : ℝ → ℂ} (ha : MeasureTheory.Integrable a MeasureTheory.volume) (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.Integrable (fun (z : ℝ × ℝ) => a z.1 * gDel z.1 z.2) (MeasureTheory.volume.prod μ)

theorem CommutingRepetition.VN.Modular.smear_Δit_eq_cbfc {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : ℝ → ℂ} (ha : MeasureTheory.Integrable a MeasureTheory.volume) {Ĝ : ℝ → ℂ} (hĜ : BorelCalc.CBdd Ĝ) (hint : ∀ (l : ℝ), ∫ (t : ℝ), a t * gDel t l = Ĝ l) : smear a ha (fun (t : ℝ) => Δit M Ω t) ⋯ ⋯ = BorelCalc.cbfc (R M Ω) ⋯ Ĝ

∫ a(t) Δ^{it} dt = Ĝ(R) where Ĝ(l) = ∫ a(t) e^{itθ(l)} dt.

theorem CommutingRepetition.VN.Modular.integral_smul_Δit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {a : ℝ → ℂ} (ha : MeasureTheory.Integrable a MeasureTheory.volume) {Ĝ : ℝ → ℂ} (hĜ : BorelCalc.CBdd Ĝ) (hint : ∀ (l : ℝ), ∫ (t : ℝ), a t * gDel t l = Ĝ l) (ζ : K) : ∫ (t : ℝ), a t • (Δit M Ω t) ζ = (BorelCalc.cbfc (R M Ω) ⋯ Ĝ) ζ

Gaussians and their Fourier transforms

noncomputable def CommutingRepetition.VN.Modular.gauss (k t : ℝ) : ℝ

The normalized Gaussian a_k(t) = √(k/π) e^{-kt²}.

Equations

• CommutingRepetition.VN.Modular.gauss k t = √(k / Real.pi) * Real.exp (-k * t ^ 2)

theorem CommutingRepetition.VN.Modular.gauss_nonneg (k t : ℝ) : 0 ≤ gauss k t

theorem CommutingRepetition.VN.Modular.continuous_gauss (k : ℝ) : Continuous (gauss k)

theorem CommutingRepetition.VN.Modular.integrable_gauss {k : ℝ} (hk : 0 < k) : MeasureTheory.Integrable (gauss k) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.integral_gauss {k : ℝ} (hk : 0 < k) : ∫ (t : ℝ), gauss k t = 1

theorem CommutingRepetition.VN.Modular.integrable_gaussC {k : ℝ} (hk : 0 < k) : MeasureTheory.Integrable (fun (t : ℝ) => ↑(gauss k t)) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.integral_norm_gaussC {k : ℝ} (hk : 0 < k) : ∫ (t : ℝ), ‖↑(gauss k t)‖ = 1

theorem CommutingRepetition.VN.Modular.integral_gaussC_mul_exp {k : ℝ} (hk : 0 < k) (u : ℝ) : ∫ (t : ℝ), ↑(gauss k t) * Complex.exp (↑(t * u) * Complex.I) = ↑(Real.exp (-u ^ 2 / (4 * k)))

The Gaussian Fourier transform: ∫ a_k(t) e^{itu} dt = e^{-u²/(4k)}.

noncomputable def CommutingRepetition.VN.Modular.gaussFlat (k t : ℝ) : ℂ

The modulated Gaussian a_k^♭(t) = e^{k/4} a_k(t) e^{-ikt}.

Equations

• CommutingRepetition.VN.Modular.gaussFlat k t = ↑(Real.exp (k / 4)) * ↑(CommutingRepetition.VN.Modular.gauss k t) * Complex.exp (-(↑(k * t) * Complex.I))

theorem CommutingRepetition.VN.Modular.norm_gaussFlat (k t : ℝ) : ‖gaussFlat k t‖ = Real.exp (k / 4) * gauss k t

theorem CommutingRepetition.VN.Modular.integrable_gaussFlat {k : ℝ} (hk : 0 < k) : MeasureTheory.Integrable (gaussFlat k) MeasureTheory.volume

theorem CommutingRepetition.VN.Modular.integral_norm_gaussFlat {k : ℝ} (hk : 0 < k) : ∫ (t : ℝ), ‖gaussFlat k t‖ = Real.exp (k / 4)

theorem CommutingRepetition.VN.Modular.integral_gaussFlat_mul_exp {k : ℝ} (hk : 0 < k) (u : ℝ) : ∫ (t : ℝ), gaussFlat k t * Complex.exp (↑(t * u) * Complex.I) = ↑(Real.exp (-u ^ 2 / (4 * k))) * ↑(Real.exp (u / 2))

∫ a_k^♭(t) e^{itu} dt = e^{-u²/(4k)} e^{u/2}.

The spectral functions e^{-θ²/(4k)} and e^{-θ²/(4k)} e^{θ/2}

noncomputable def CommutingRepetition.VN.Modular.gk (k l : ℝ) : ℝ

gk k l = e^{-θ(l)²/(4k)}.

Equations

• CommutingRepetition.VN.Modular.gk k l = Real.exp (-CommutingRepetition.VN.Modular.θ l ^ 2 / (4 * k))

noncomputable def CommutingRepetition.VN.Modular.gkFlat (k l : ℝ) : ℝ

gkFlat k l = e^{-θ(l)²/(4k)} e^{θ(l)/2}.

Equations

• CommutingRepetition.VN.Modular.gkFlat k l = CommutingRepetition.VN.Modular.gk k l * Real.exp (CommutingRepetition.VN.Modular.θ l / 2)

theorem CommutingRepetition.VN.Modular.gk_pos (k l : ℝ) : 0 < gk k l

theorem CommutingRepetition.VN.Modular.gk_le_one {k : ℝ} (hk : 0 < k) (l : ℝ) : gk k l ≤ 1

theorem CommutingRepetition.VN.Modular.measurable_gk (k : ℝ) : Measurable (gk k)

theorem CommutingRepetition.VN.Modular.bdd_gk {k : ℝ} (hk : 0 < k) : BorelCalc.Bdd (gk k)

theorem CommutingRepetition.VN.Modular.gkFlat_le {k : ℝ} (hk : 0 < k) (l : ℝ) : gkFlat k l ≤ Real.exp (k / 4)

theorem CommutingRepetition.VN.Modular.gkFlat_pos (k l : ℝ) : 0 < gkFlat k l

theorem CommutingRepetition.VN.Modular.measurable_gkFlat (k : ℝ) : Measurable (gkFlat k)

theorem CommutingRepetition.VN.Modular.bdd_gkFlat {k : ℝ} (hk : 0 < k) : BorelCalc.Bdd (gkFlat k)

theorem CommutingRepetition.VN.Modular.integral_gaussC_mul_gDel {k : ℝ} (hk : 0 < k) (l : ℝ) : ∫ (t : ℝ), ↑(gauss k t) * gDel t l = ↑(gk k l)

theorem CommutingRepetition.VN.Modular.integral_gaussFlat_mul_gDel {k : ℝ} (hk : 0 < k) (l : ℝ) : ∫ (t : ℝ), gaussFlat k t * gDel t l = ↑(gkFlat k l)

The smeared elements x_k and x_k^♭

theorem CommutingRepetition.VN.Modular.norm_σ_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (x : K →L[ℂ] K) : ‖σ M Ω t x‖ ≤ ‖x‖

theorem CommutingRepetition.VN.Modular.continuous_σ_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) (v : K) : Continuous fun (t : ℝ) => (σ M Ω t x) v

noncomputable def CommutingRepetition.VN.Modular.xk {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (k : ℝ) (hk : 0 < k) (x : K →L[ℂ] K) : K →L[ℂ] K

The Gaussian smearing x_k = ∫ a_k(t) σ_t(x) dt.

Equations

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

noncomputable def CommutingRepetition.VN.Modular.xkFlat {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (k : ℝ) (hk : 0 < k) (x : K →L[ℂ] K) : K →L[ℂ] K

The companion x_k^♭ = e^{k/4} ∫ a_k(t) e^{-ikt} σ_t(x*) dt.

Equations

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

theorem CommutingRepetition.VN.Modular.xk_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : ℝ} (hk : 0 < k) {x : K →L[ℂ] K} (hx : x ∈ M) : xk M Ω k hk x ∈ M

theorem CommutingRepetition.VN.Modular.xkFlat_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : ℝ} (hk : 0 < k) {x : K →L[ℂ] K} (hx : x ∈ M) : xkFlat M Ω k hk x ∈ M

theorem CommutingRepetition.VN.Modular.norm_xk_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {k : ℝ} (hk : 0 < k) (x : K →L[ℂ] K) : ‖xk M Ω k hk x‖ ≤ ‖x‖

theorem CommutingRepetition.VN.Modular.norm_xkFlat_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {k : ℝ} (hk : 0 < k) (x : K →L[ℂ] K) : ‖xkFlat M Ω k hk x‖ ≤ Real.exp (k / 4) * ‖x‖

theorem CommutingRepetition.VN.Modular.xk_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {k : ℝ} (hk : 0 < k) (x : K →L[ℂ] K) : (xk M Ω k hk x) Ω = (BorelCalc.bfc (R M Ω) ⋯ (gk k)) (x Ω)

x_k Ω = e^{-θ²/(4k)}(R) xΩ.

theorem CommutingRepetition.VN.Modular.xkFlat_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {k : ℝ} (hk : 0 < k) (x : K →L[ℂ] K) : (xkFlat M Ω k hk x) Ω = (BorelCalc.bfc (R M Ω) ⋯ (gkFlat k)) ((star x) Ω)

x_k^♭ Ω = (e^{-θ²/(4k)} e^{θ/2})(R) x*Ω.

theorem CommutingRepetition.VN.Modular.gk_two_sub (k l : ℝ) : gk k (2 - l) = gk k l

theorem CommutingRepetition.VN.Modular.gkFlat_two_sub (k l : ℝ) : gkFlat k (2 - l) = gk k l * Real.exp (-(θ l / 2))

The reflected companion function gkFlat k (2 − l) = e^{-θ²/(4k)} e^{-θ/2}.

theorem CommutingRepetition.VN.Modular.Jm_xkFlat_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : ℝ} (hk : 0 < k) {x : K →L[ℂ] K} (hx : x ∈ M) : (Jm M Ω) ((xkFlat M Ω k hk x) Ω) = (xk M Ω k hk x) Ω

The key identity J x_k^♭ Ω = x_k Ω.

Left boundedness

theorem CommutingRepetition.VN.Modular.re_inner_commutant_apply_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {c y : K →L[ℂ] K} (hc' : c ∈ M.commutant) (hy : y ∈ M) (hy0 : 0 ≤ y) : (inner ℂ (c Ω) (y (c Ω))).re ≤ ‖c‖ ^ 2 * (inner ℂ Ω (y Ω)).re

For c ∈ M′ and 0 ≤ y ∈ M: ⟪cΩ, y cΩ⟫ ≤ ‖c‖² ⟪Ω, yΩ⟫.

theorem CommutingRepetition.VN.Modular.norm_conjJm_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (G : K →L[ℂ] K) : ‖conjJm M Ω G‖ ≤ ‖G‖

theorem CommutingRepetition.VN.Modular.inner_Ω_star_mul_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (a y : K →L[ℂ] K) : inner ℂ Ω ((star a * y * a) Ω) = inner ℂ (a Ω) (y (a Ω))

theorem CommutingRepetition.VN.Modular.re_inner_xk_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {k : ℝ} (hk : 0 < k) {x y : K →L[ℂ] K} (hx : x ∈ M) (hy : y ∈ M) (hy0 : 0 ≤ y) : (inner ℂ Ω ((star (xk M Ω k hk x) * y * xk M Ω k hk x) Ω)).re ≤ ‖xkFlat M Ω k hk x‖ ^ 2 * (inner ℂ Ω (y Ω)).re

HJX Lemma 2.5(i) for the smeared elements: ψ(x_k* y x_k) ≤ ‖x_k^♭‖² ψ(y) for 0 ≤ y ∈ M.

Convergence x_k Ω → xΩ

theorem CommutingRepetition.VN.Modular.tendsto_gk (l : ℝ) : Filter.Tendsto (fun (n : ℕ) => ↑(gk (↑n + 1) l)) Filter.atTop (nhds 1)

theorem CommutingRepetition.VN.Modular.tendsto_xk_apply_Ω {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (x : K →L[ℂ] K) : Filter.Tendsto (fun (n : ℕ) => (xk M Ω (↑n + 1) ⋯ x) Ω) Filter.atTop (nhds (x Ω))

x_k Ω → xΩ along k = n + 1 → ∞: the smeared elements are ‖·‖_ψ-dense.