Physicslib4.GNS.CauchySchwarz

Cauchy-Schwarz inequality for positive linear functionals on a *-algebra

This file states the Cauchy-Schwarz inequality for positive linear functionals on an arbitrary (not necessarily unital, not necessarily normed) *-algebra over ℂ, following the AQFT-in-Lean blueprint section 10.1, label lmm:cauchy-schwarz-inequality.

The hypothesis is weaker than Physicslib4.GNS.State: we only require a ℂ-linear functional ω : A →ₗ[ℂ] ℂ together with positivity 0 ≤ ω (star a * a) for all a. Continuity and normalisation are not assumed.

Main statements

• Physicslib4.GNS.omega_star_swap_conj: for a positive linear functional ω on a *-algebra A, ω (star a * b) = star (ω (star b * a)) for all a, b : A.
• Physicslib4.GNS.cauchy_schwarz_inequality: under the same hypotheses, Complex.normSq (ω (star a * b)) ≤ (ω (star a * a)).re * (ω (star b * b)).re for all a, b : A.

Both conclusions of the blueprint lemma are recorded; the primary entry-point is cauchy_schwarz_inequality.

Typeclass setup

The blueprint says "*-algebra"; the minimal Mathlib shape needed to state the lemma is a complex *-ring, i.e. [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A]. Continuity of ω and normalisation are not required.

theorem Physicslib4.GNS.omega_star_swap_conj {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (ω : A →ₗ[ℂ] ℂ) (hω : ∀ (a : A), 0 ≤ ω (star a * a)) (a b : A) : ω (star a * b) = star (ω (star b * a))

Hermitian symmetry of a positive functional: ω(a* b) is the complex conjugate of ω(b* a).

A linear functional ω on a complex -algebra is positive when ω(a a) ≥ 0 for every a. The form ⟨a, b⟩ = ω(a* b) is then Hermitian, as an inner product is. The proof applies positivity to a + b and ia + b.

Implementation note: ω is only linear (A →ₗ[ℂ] ℂ); continuity, normalisation and a unit are not needed, and A is any complex *-ring with compatible scalar action.

Blueprint: the Hermitian symmetry used in lmm:cauchy-schwarz-inequality

theorem Physicslib4.GNS.cauchy_schwarz_inequality {A : Type u_1} [NonUnitalNonAssocRing A] [StarRing A] [Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A] (ω : A →ₗ[ℂ] ℂ) (hω : ∀ (a : A), 0 ≤ ω (star a * a)) (a b : A) : Complex.normSq (ω (star a * b)) ≤ (ω (star a * a)).re * (ω (star b * b)).re

The Cauchy–Schwarz inequality |ω(a* b)|² ≤ ω(a* a) ω(b* b) for a positive linear functional ω.

The form ⟨a, b⟩ = ω(a* b) is a positive semi-definite Hermitian form on A, and this is the Cauchy–Schwarz inequality for it; it holds although the form may be degenerate. It is the key step in the GNS construction: if ω(n* n) = 0 then ω(b* n) = 0 for every b (lmm1). Every state is a positive functional, so the inequality applies to states.

Implementation note: ω is only linear (A →ₗ[ℂ] ℂ), not assumed continuous or normalised, and A is any complex -ring with compatible scalar action. Since ω(a a) and ω(b* b) are non-negative reals, the right-hand side is written with real parts, and the left-hand side is Complex.normSq.

Blueprint: lmm:cauchy-schwarz-inequality