def ProbabilityTheory.IsPositiveDefinite (φ : ℝ → ℂ) : Prop

A complex-valued function φ : ℝ → ℂ is positive definite if for every finite collection of times t : Fin n → ℝ and complex coefficients z : Fin n → ℂ, the Hermitian form ∑_{i,j} φ(t_i - t_j) z_i \overline{z_j} has nonnegative real part. Equivalently, the matrix (φ(t_i - t_j))_{i,j} is positive semidefinite.

def ProbabilityTheory.IsPositiveDefiniteReal (φ : ℝ → ℝ) : Prop

A real-valued function φ : ℝ → ℝ is positive definite if its complex embedding (↑) ∘ φ : ℝ → ℂ is positive definite in the sense of IsPositiveDefinite.

def ProbabilityTheory.IsCharacteristicFun (φ : ℝ → ℂ) : Prop

A function φ : ℝ → ℂ is a characteristic function if it arises as the characteristic function t ↦ ∫ e^{itx} dμ(x) of some probability measure μ on ℝ.

def ProbabilityTheory.IsCharacteristicFunReal (φ : ℝ → ℝ) : Prop

A real-valued function φ : ℝ → ℝ is a characteristic function if its complex embedding (↑) ∘ φ is.

theorem ProbabilityTheory.bochner_theorem_complex (φ : ℝ → ℂ) : IsCharacteristicFun φ ↔ Continuous φ ∧ IsPositiveDefinite φ ∧ φ 0 = 1

Bochner's theorem (complex form). A function φ : ℝ → ℂ is the characteristic function of some probability measure on ℝ if and only if it is continuous, positive definite, and satisfies φ(0) = 1 (Durrett, Lecture 14/15).

theorem ProbabilityTheory.bochner_theorem (φ : ℝ → ℝ) : IsCharacteristicFunReal φ ↔ Continuous φ ∧ IsPositiveDefiniteReal φ ∧ φ 0 = 1

Bochner's theorem (real form). A continuous function φ : ℝ → ℝ with φ(1) = 1 — here packaged as φ(0) = 1 together with continuity and positive definiteness — is the characteristic function of some probability measure on ℝ if and only if it is positive definite (Durrett, Lecture 14/15).