Uniform experiments as averages

An experiment that starts by drawing a uniformly from a finite type and then runs f a outputs b with probability the average over a of the probability that f a outputs b (toReal_uniformOfFintype_bind_apply). In particular, a Boolean function g of a uniform sample is true with probability the density of the set where g is true (toReal_uniformOfFintype_map_apply_true). These translate experiments written with PMF.bind into the vocabulary of Finset.expect (𝔼) and Finset.dens.

Main results

• Cslib.Probability.PMF.sum_le_affine: average pointwise affine bounds.

• Cslib.Probability.PMF.sum_map_mul, .sum_bind_mul: average deterministic and random scores.

• Cslib.Probability.PMF.toReal_uniformOfFintype_bind_apply: a uniform first stage averages the second stages.

• Cslib.Probability.PMF.toReal_uniformOfFintype_map_apply: output probabilities are densities.

• Cslib.Probability.PMF.toReal_uniformOfFintype_map_apply_true: the probability that a Boolean function of a uniform sample is true is a density.

theorem Cslib.Probability.PMF.sum_map_mul {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : PMF α) (f : α → β) (score : β → ℝ) : ∑ b : β, ((PMF.map f p) b).toReal * score b = ∑ a : α, (p a).toReal * score (f a)

Averaging a score after a deterministic map averages its composite with that map. Adapted from the cslib crypto branch at 5ff69ca.

theorem Cslib.Probability.PMF.sum_bind_mul {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : PMF α) (kernel : α → PMF β) (score : β → ℝ) : ∑ b : β, ((p.bind kernel) b).toReal * score b = ∑ a : α, (p a).toReal * ∑ b : β, ((kernel a) b).toReal * score b

Averaging a score after a random choice averages its conditional scores. Adapted from the cslib crypto branch at 5ff69ca.

theorem Cslib.Probability.PMF.sum_affine {α : Type u_1} [Fintype α] (p : PMF α) (a b : ℝ) (score : α → ℝ) : ∑ x : α, (p x).toReal * (a + b * score x) = a + b * ∑ x : α, (p x).toReal * score x

The expectation of an affine score is the affine function of its expectation. Adapted from the cslib crypto branch at 5ff69ca.

theorem Cslib.Probability.PMF.sum_le_affine {α : Type u_1} [Fintype α] (p : PMF α) {a b : ℝ} {score bound : α → ℝ} (h : ∀ (x : α), score x ≤ a + b * bound x) : ∑ x : α, (p x).toReal * score x ≤ a + b * ∑ x : α, (p x).toReal * bound x

Pointwise affine bounds survive averaging over a finite distribution.

theorem Cslib.Probability.PMF.sum_mul_le {α : Type u_1} [Fintype α] (p : PMF α) (score : α → ℝ) (bound : ℝ) (hscore : ∀ (a : α), score a ≤ bound) : ∑ a : α, (p a).toReal * score a ≤ bound

A uniform upper bound on a score also bounds its expectation.

theorem Cslib.Probability.PMF.toReal_uniformOfFintype_bind_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] (f : α → PMF β) (b : β) : (((uniformOfFintype α).bind f) b).toReal = Finset.univ.expect fun (a : α) => ((f a) b).toReal

An experiment whose first stage draws a uniformly outputs b with probability the average over a of the probability that the second stage f a outputs b.

theorem Cslib.Probability.PMF.toReal_uniformOfFintype_map_apply {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [DecidableEq β] (f : α → β) (b : β) : ((PMF.map f (uniformOfFintype α)) b).toReal = ↑{a : α | f a = b}.dens

The mass of an output of a uniform sample is the density of its fiber.

theorem Cslib.Probability.PMF.toReal_uniformOfFintype_map_apply_true {α : Type u_1} [Fintype α] [Nonempty α] (g : α → Bool) : ((PMF.map g (uniformOfFintype α)) true).toReal = ↑{a : α | g a = true}.dens

A Boolean function g of a uniform sample is true with probability the density of the set where g is true.