Genericity and UD–random reals

WESLEY CALVERT and JOHANNA N.Y. FRANKLIN

This concerns the second sentence in the Introduction in the paper.

We define uniform distribution and prove that the constant 0 sequence is not uniformly distributed.

def uniformly_distributed_at (x : ℕ → ↑(Set.Ico 0 1)) (a : ℝ) (b : ℝ) (ε : ℝ) : Prop

The triple (a,b,ε) satisfies the conditions for uniform distribution of x.

Equations

• uniformly_distributed_at x a b ε = ∃ (n₀ : ℕ), ∀ n ≥ n₀, |↑(Finset.filter (fun (i : Fin n) => a < ↑(x ↑i) ∧ ↑(x ↑i) < b) Finset.univ).card - (b - a) * ↑n| < ↑n * ε

def uniformly_distributed (x : ℕ → ↑(Set.Ico 0 1)) : Prop

The sequence x is uniformly distributed in the half-open unit interval.

Equations

• uniformly_distributed x = ∀ (a b ε : ℝ), 0 ≤ a → a < b → b ≤ 1 → ε > 0 → uniformly_distributed_at x a b ε

theorem zero_not_uniformly_distributed : ¬uniformly_distributed fun (x : ℕ) => ⟨0, ⋯⟩

The constant zero sequence is not uniformly distributed.