Lattice distributions

DefinitionLattice random variable#✓fully proved

A measure \(\mu\) on \(\mathbb{R}\) with characteristic function \(\varphi(t) = \int e^{itx} \, d\mu(x)\) is a lattice random variable if \(\varphi(l) = 1\) for some real \(l \ne 0\) and \(\varphi(t) \ne 1\) for some real \(t\).

For a probability measure, the second condition says that \(\mu\) is not the point mass at \(0\).

def IsLatticeRV (μ : Measure ℝ) : Prop :=
  (∃ l : ℝ, l ≠ 0 ∧ charFun μ l = 1) ∧ ¬ (∀ t : ℝ, charFun μ t = 1)

Used by 1

Used byLattice random variables are supported on a lattice

TheoremA characteristic function equal to one detects lattice support#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) with characteristic function \(\varphi(t) = \int e^{itx} \, d\mu(x)\), and let \(l \ne 0\) be real. Then \(\varphi(l) = 1\) if and only if \(\mu\) gives mass \(1\) to the lattice \(\{(2\pi / l) k : k \in \mathbb{Z}\}\).

Forward direction: \(\operatorname{Re} \varphi(l) = \int \cos(lx) \, d\mu(x) = 1\) forces \(\int (1 - \cos(lx)) \, d\mu(x) = 0\), hence \(\cos(lx) = 1\) almost everywhere, hence \(lx \in 2\pi\mathbb{Z}\) almost everywhere. Backward direction: on the lattice the integrand \(e^{ilx}\) is identically \(1\).

theorem charFun_eq_one_iff_measure_eq_one_of_lattice {μ : Measure ℝ}
    [IsProbabilityMeasure μ] {l : ℝ} (hl : l ≠ 0) :
    charFun μ l = 1 ↔
      μ {x : ℝ | ∃ k : ℤ, x = (2 * Real.pi / l) * k} = 1

Used by 1

Used byLattice random variables are supported on a lattice

TheoremLattice random variables are supported on a lattice#✓fully proved

Let \(\mu\) be a probability measure on \(\mathbb{R}\) that is a lattice random variable. Then there is a real number \(h \ne 0\) such that \(\mu\) gives mass \(1\) to the lattice \(\{hk : k \in \mathbb{Z}\}\).

One can take \(h = 2\pi / l\) for a nonzero frequency \(l\) at which the characteristic function of \(\mu\) equals \(1\). The condition that the characteristic function is not identically \(1\) is not needed.

theorem IsLatticeRV.exists_lattice_support {μ : Measure ℝ} [IsProbabilityMeasure μ]
    (h : IsLatticeRV μ) : ∃ hstep : ℝ, hstep ≠ 0 ∧
      μ {x : ℝ | ∃ k : ℤ, x = hstep * k} = 1

Uses 2

Statement usesLattice random variable

Proof usesA characteristic function equal to one detects lattice support

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.