Bochner's theorem

TheoremBochner's theorem#✓fully proved

Let \(f : \mathbb{R} \to \mathbb{C}\). Then \(f\) is continuous, satisfies \(f(0) = 1\), and is positive definite, meaning that for every \(n \in \mathbb{N}\), all points \(x_1, \dots, x_n \in \mathbb{R}\) and all coefficients \(c_1, \dots, c_n \in \mathbb{C}\) the sum \(S = \sum_{i=1}^{n} \sum_{j=1}^{n} \overline{c_i}\, c_j\, f(x_i - x_j)\) is a nonnegative real number, if and only if there is a Borel probability measure \(\mu\) on \(\mathbb{R}\) such that \(f(t) = \int_{\mathbb{R}} e^{itx} \, d\mu(x)\) for every \(t \in \mathbb{R}\), that is, \(f\) is the characteristic function of \(\mu\).

theorem bochner
    {f : ℝ → ℂ} :
    (Continuous f ∧ f 0 = 1 ∧
      ∀ (n : ℕ) (x : Fin n → ℝ) (c : Fin n → ℂ),
        let S := ∑ i : Fin n, ∑ j : Fin n, star (c i) * c j * f (x i - x j)
        S.im = 0 ∧ 0 ≤ S.re)
    ↔
    (∃ (μ : Measure ℝ), IsProbabilityMeasure μ ∧ ∀ (t : ℝ), f t = charFun μ t)

Sources

• Bochner's theorem on positive-definite functions, S. Bochner, Vorlesungen über Fouriersche Integrale 1932 and Math. Ann. 108 (1933); see Folland, Abstract Harmonic Analysis, Fourier Analysis on Groups; Lean is ℝ→ℂ iff version continuous f 0=1 positive- definite via double sum iff ∃ Borel probability μ with f = charFun μ, fixed +I sign via charFun.

Used by 1

Used byForward direction of Bochner's theorem

DefinitionPositive definite functions#✓fully proved

A function \(\varphi : \mathbb{R} \to \mathbb{C}\) is positive definite when for every \(n \in \mathbb{N}\), all \(t_1, \dots, t_n \in \mathbb{R}\) and all \(z_1, \dots, z_n \in \mathbb{C}\), the sum \(S = \sum_{i=1}^{n} \sum_{j=1}^{n} \varphi(t_i - t_j) \, z_i \, \overline{z_j}\) is real and nonnegative, that is, \(\operatorname{Im} S = 0\) and \(\operatorname{Re} S \ge 0\).

def IsPositiveDefinite (φ : ℝ → ℂ) : Prop :=
  ∀ (n : ℕ) (t : Fin n → ℝ) (z : Fin n → ℂ),
    let S := ∑ i, ∑ j, φ (t i - t j) * z i * starRingEnd ℂ (z j)
    S.im = 0 ∧ 0 ≤ S.re

Used by 4

Used byForward direction of Bochner's theorem · Real-valued characteristic functions are continuous and positive definite · Characteristic functions are positive definite · Positive definite real-valued functions

DefinitionPositive definite real-valued functions#✓fully proved

A function \(\varphi : \mathbb{R} \to \mathbb{R}\) is positive definite when its composition with the inclusion \(\mathbb{R} \to \mathbb{C}\) is positive definite, that is, when for every \(n \in \mathbb{N}\), all \(t_1, \dots, t_n \in \mathbb{R}\) and all \(z_1, \dots, z_n \in \mathbb{C}\), the sum \(\sum_{i=1}^{n} \sum_{j=1}^{n} \varphi(t_i - t_j) \, z_i \, \overline{z_j}\) is a nonnegative real number.

def IsPositiveDefiniteReal (φ : ℝ → ℝ) : Prop :=
  IsPositiveDefinite ((↑) ∘ φ)

Uses 1 · Used by 1

Statement usesPositive definite functions

Used byReal-valued characteristic functions are continuous and positive definite

DefinitionCharacteristic functions#✓fully proved

A function \(\varphi : \mathbb{R} \to \mathbb{C}\) is a characteristic function when there is a probability measure \(\mu\) on \(\mathbb{R}\) whose characteristic function equals \(\varphi\), that is, \(\int_{\mathbb{R}} e^{itx} \, d\mu(x) = \varphi(t)\) for every \(t \in \mathbb{R}\).

def IsCharacteristicFun (φ : ℝ → ℂ) : Prop :=
  ∃ μ : Measure ℝ, IsProbabilityMeasure μ ∧ ∀ t, charFun μ t = φ t

Used by 3

Used byForward direction of Bochner's theorem · Real-valued characteristic functions are continuous and positive definite · Real-valued characteristic functions

DefinitionReal-valued characteristic functions#✓fully proved

A function \(\varphi : \mathbb{R} \to \mathbb{R}\) is a real-valued characteristic function when its composition with the inclusion \(\mathbb{R} \to \mathbb{C}\) is a characteristic function, that is, when there is a probability measure \(\mu\) on \(\mathbb{R}\) with \(\int_{\mathbb{R}} e^{itx} \, d\mu(x) = \varphi(t)\) for every \(t \in \mathbb{R}\).

def IsCharacteristicFunReal (φ : ℝ → ℝ) : Prop :=
  IsCharacteristicFun ((↑) ∘ φ)

Uses 1 · Used by 1

Statement usesCharacteristic functions

Used byReal-valued characteristic functions are continuous and positive definite

TheoremForward direction of Bochner's theorem#✓fully proved

Let \(\varphi : \mathbb{R} \to \mathbb{C}\) be the characteristic function of a probability measure on \(\mathbb{R}\). Then \(\varphi\) is continuous, positive definite, and satisfies \(\varphi(0) = 1\).

theorem bochner_forward (φ : ℝ → ℂ) (hφ : IsCharacteristicFun φ) :
    Continuous φ ∧ IsPositiveDefinite φ ∧ φ 0 = 1

Uses 3 · Used by 2

Statement usesCharacteristic functions · Positive definite functions

Proof usesBochner's theorem

Used byReal-valued characteristic functions are continuous and positive definite · Characteristic functions are positive definite

TheoremCharacteristic functions are positive definite#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with characteristic function \(\varphi_\mu(t) = \int_{\mathbb{R}} e^{itx} \, d\mu(x)\). Then \(\varphi_\mu\) is positive definite: for every \(n \in \mathbb{N}\), all \(t_1, \dots, t_n \in \mathbb{R}\) and all \(z_1, \dots, z_n \in \mathbb{C}\), the sum \(\sum_{i=1}^{n} \sum_{j=1}^{n} \varphi_\mu(t_i - t_j) \, z_i \, \overline{z_j}\) is a nonnegative real number.

theorem charFun_isPositiveDefinite (μ : Measure ℝ) [IsProbabilityMeasure μ] :
    IsPositiveDefinite (charFun μ)

Uses 2

Statement usesPositive definite functions

Proof usesForward direction of Bochner's theorem

TheoremReal-valued characteristic functions are continuous and positive definite#✓fully proved

Let \(\varphi : \mathbb{R} \to \mathbb{R}\) be a real-valued characteristic function, that is, a function whose composition with the inclusion \(\mathbb{R} \to \mathbb{C}\) is the characteristic function of a probability measure on \(\mathbb{R}\). Then \(\varphi\) is continuous, \(\varphi\) is positive definite in the sense that its composition with the inclusion \(\mathbb{R} \to \mathbb{C}\) is positive definite, and \(\varphi(0) = 1\).

theorem bochner_forward_real (φ : ℝ → ℝ) (hφ : IsCharacteristicFunReal φ) :
    Continuous φ ∧ IsPositiveDefiniteReal φ ∧ φ 0 = 1

Uses 5

Statement usesReal-valued characteristic functions · Positive definite real-valued functions

Proof usesCharacteristic functions · Positive definite functions · Forward direction of Bochner's theorem

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.