Gaussian smearing and density of entire analytic elements

For a point-norm continuous real action α on a possibly nonunital C⋆-algebra A, the Gaussian smearing of a : A with parameter c is the average of the orbit of a against the Gaussian density of width c⁻¹,

α.gaussianSmear c a = ∫ t, (c / √π) exp (-(c t)²) • α_t a.

The smeared element is entire analytic: its complex-time extension is obtained by translating the Gaussian kernel into the complex plane,

α_z (α.gaussianSmear c a) = ∫ t, (c / √π) exp (-(c (t - z))²) • α_t a,

which is entire by differentiation under the integral sign. Smearing commutes with the action and does not increase norms. As c → ∞ the Gaussian densities concentrate at 0, so α.gaussianSmear c a → a. Hence the entire analytic elements form a dense star subalgebra, invariant under the action. This is the density statement used to reduce identities such as the KMS condition to entire analytic elements.

Neither unitality of A nor any countability assumption is needed. For each c, smearing is complex linear and commutes with star.

Main definitions

• TauCeti.CStarAction.gaussianSmear: the Gaussian smearing of an element.
• TauCeti.CStarAction.gaussianSmearCLM: Gaussian smearing as a continuous linear map.

Main statements

• TauCeti.CStarAction.entireExtension_gaussianSmear: the complex-time extension of a Gaussian smearing.
• TauCeti.CStarAction.isEntireAnalytic_gaussianSmear: Gaussian smearings are entire analytic.
• TauCeti.CStarAction.gaussianSmear_add, TauCeti.CStarAction.gaussianSmear_smul: smearing is complex linear.
• TauCeti.CStarAction.gaussianSmear_star: smearing commutes with star.
• TauCeti.CStarAction.apply_gaussianSmear, TauCeti.CStarAction.norm_gaussianSmear_le: smearing commutes with the action and is contractive.
• TauCeti.CStarAction.tendsto_gaussianSmear: α.gaussianSmear c a → a as c → ∞.
• TauCeti.CStarAction.dense_entireAnalytic: the entire analytic elements are dense.

References

Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 1, second edition, Section 2.5.3, for the density of entire analytic elements by Gaussian smearing.

noncomputable def TauCeti.CStarAction.gaussianSmear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : A

The Gaussian smearing ∫ t, (c / √π) exp (-(c t)²) • α_t a of a. For c > 0 it is the average of the orbit of a against the Gaussian probability density of width c⁻¹.

theorem TauCeti.CStarAction.gaussianSmear_def {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : α.gaussianSmear c a = ∫ (t : ℝ), (↑c / ↑√Real.pi * Complex.exp (-(↑c * ↑t) ^ 2)) • (α (Multiplicative.ofAdd t)) a

The defining formula of the Gaussian smearing.

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_zero {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) : α.gaussianSmear c 0 = 0

The Gaussian smearing of 0 is 0.

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_zero_param {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : A) : α.gaussianSmear 0 a = 0

The Gaussian smearing with parameter 0 vanishes.

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_add {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a b : A) : α.gaussianSmear c (a + b) = α.gaussianSmear c a + α.gaussianSmear c b

The Gaussian smearing is additive.

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_smul {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (r : ℂ) (a : A) : α.gaussianSmear c (r • a) = r • α.gaussianSmear c a

The Gaussian smearing commutes with complex scalars.

The complex-time extension

theorem TauCeti.CStarAction.entireExtension_gaussianSmear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) (z : ℂ) : α.entireExtension (α.gaussianSmear c a) z = ∫ (t : ℝ), (↑c / ↑√Real.pi * Complex.exp (-(↑c * (↑t - z)) ^ 2)) • (α (Multiplicative.ofAdd t)) a

The complex-time extension of a Gaussian smearing is obtained by translating the Gaussian kernel: α_z (α.gaussianSmear c a) = ∫ t, (c / √π) exp (-(c (t - z))²) • α_t a.

theorem TauCeti.CStarAction.isEntireAnalytic_gaussianSmear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : α.IsEntireAnalytic (α.gaussianSmear c a)

Gaussian smearings are entire analytic.

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_neg {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : α.gaussianSmear (-c) a = -α.gaussianSmear c a

The Gaussian smearing is odd in the parameter c.

theorem TauCeti.CStarAction.apply_gaussianSmear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c s : ℝ) (a : A) : (α (Multiplicative.ofAdd s)) (α.gaussianSmear c a) = α.gaussianSmear c ((α (Multiplicative.ofAdd s)) a)

Gaussian smearing commutes with the action: α_s (α.gaussianSmear c a) = α.gaussianSmear c (α_s a).

Convergence as the width tends to zero

@[simp]

theorem TauCeti.CStarAction.gaussianSmear_star {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : α.gaussianSmear c (star a) = star (α.gaussianSmear c a)

The Gaussian smearing commutes with the star operation, since the Gaussian density is real and the action preserves star.

theorem TauCeti.CStarAction.norm_gaussianSmear_le {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : ‖α.gaussianSmear c a‖ ≤ ‖a‖

The Gaussian smearing is a contraction: ‖α.gaussianSmear c a‖ ≤ ‖a‖.

noncomputable def TauCeti.CStarAction.gaussianSmearCLM {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) : A →L[ℂ] A

Gaussian smearing as a continuous complex-linear map.

@[simp]

theorem TauCeti.CStarAction.gaussianSmearCLM_apply {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (a : A) : (α.gaussianSmearCLM c) a = α.gaussianSmear c a

Applying the continuous linear Gaussian smearing map gives the Gaussian smearing.

theorem TauCeti.CStarAction.toSemigroup_gaussianSmearCLM {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (c : ℝ) (t : NNReal) (a : A) : (α.toStronglyContinuousGroup.toSemigroup t) ((α.gaussianSmearCLM c) a) = (α.gaussianSmearCLM c) ((α.toStronglyContinuousGroup.toSemigroup t) a)

Gaussian smearing commutes with the associated strongly continuous semigroup.

theorem TauCeti.CStarAction.tendsto_gaussianSmear {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (a : A) : Filter.Tendsto (fun (c : ℝ) => α.gaussianSmear c a) Filter.atTop (nhds a)

Convergence of Gaussian smearings. As the width c⁻¹ of the Gaussian tends to zero, the Gaussian smearing of a tends to a.

Density

theorem TauCeti.CStarAction.dense_entireAnalytic {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) : Dense ↑α.entireAnalytic

Density of entire analytic elements. The entire analytic elements of a point-norm continuous real action are dense, since every element is a limit of its Gaussian smearings.