The uniform vector on a finset

Finset.uniform s is the indicator of s scaled to a probability vector: (#s)⁻¹ on s, 0 off it, and the zero vector when s is empty — the exact (ℚ-valued) uniform distribution as a plain function, for consumers that compute with probability vectors rather than measures. uniform_eq_indicator connects it to Set.indicator, and its inner products are mathlib's Finset.expect: ∑ a, s.uniform a * f a = 𝔼 a ∈ s, f a.

Main definitions

• Finset.uniform s — (#s)⁻¹ on s, 0 off it.

Main statements

• uniform_pos_iff, uniform_injective — the support is s, and determines it.
• sum_uniform_mul — the inner product with f is the expectation of f on s.
• sum_uniform_argmax_mul — the expectation of f on its argmax is its maximum.
• sum_mul_le_of_support — a sub-probability average of f supported on s is at most the maximum of f on s.

def Finset.uniform {α : Type u_1} {K : Type u_2} [DecidableEq α] [Semifield K] (s : Finset α) : α → K

The uniform vector on s: (#s)⁻¹ on s, 0 off it.

Equations

• s.uniform a = if a ∈ s then (↑s.card)⁻¹ else 0

theorem Finset.uniform_apply {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Semifield K] : s.uniform a = if a ∈ s then (↑s.card)⁻¹ else 0

theorem Finset.uniform_eq_indicator {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Semifield K] : s.uniform = (↑s).indicator fun (x : α) => (↑s.card)⁻¹

@[simp]

theorem Finset.uniform_of_mem {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Semifield K] (h : a ∈ s) : s.uniform a = (↑s.card)⁻¹

@[simp]

theorem Finset.uniform_of_notMem {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Semifield K] (h : a ∉ s) : s.uniform a = 0

theorem Finset.sum_uniform_mul {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Semifield K] [CharZero K] [Fintype α] (f : α → K) : ∑ a : α, s.uniform a * f a = s.expect fun (a : α) => f a

The inner product with the uniform vector is the expectation on s.

theorem Finset.sum_uniform {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Semifield K] [CharZero K] [Fintype α] : ∑ a : α, s.uniform a = if s = ∅ then 0 else 1

theorem Finset.uniform_nonneg {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : 0 ≤ s.uniform a

theorem Finset.uniform_le_one {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : s.uniform a ≤ 1

theorem Finset.uniform_pos_iff {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} {a : α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] : 0 < s.uniform a ↔ a ∈ s

theorem Finset.uniform_injective {α : Type u_1} {K : Type u_2} [DecidableEq α] [Field K] [LinearOrder K] [IsStrictOrderedRing K] : Function.Injective uniform

The uniform vector determines the finset.

theorem Finset.sum_uniform_le_one {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Fintype α] : ∑ a : α, s.uniform a ≤ 1

theorem Finset.sum_uniform_argmax_mul {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Fintype α] (f : α → K) {a₀ : α} (h : a₀ ∈ s.argmax f) : ∑ a : α, (s.argmax f).uniform a * f a = f a₀

The expectation of f on its argmax is its maximum.

theorem Finset.sum_mul_le_of_support {α : Type u_1} {K : Type u_2} [DecidableEq α] {s : Finset α} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Fintype α] (w f : α → K) (hw : ∀ (a : α), 0 ≤ w a) (hsum : ∑ a : α, w a ≤ 1) (hsupp : ∀ a ∉ s, w a = 0) (hf : ∀ (a : α), 0 ≤ f a) {a₀ : α} (h : a₀ ∈ s.argmax f) : ∑ a : α, w a * f a ≤ f a₀

A sub-probability average of a nonnegative f, with weights supported on s, is at most the maximum of f on s.