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.tsum_map_mul, .tsum_bind_mul: the same laws for extended nonnegative scores over arbitrary types.
• Cslib.Probability.PMF.sq_tsum_le_tsum_sq: Jensen's inequality E[g]² ≤ E[g²] for a [0, 1]-valued score.
• 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.tsum_map_mul {α : Type u_1} {β : Type u_2} (p : PMF α) (g : α → β) (k : β → ENNReal) : ∑' (b : β), (PMF.map g p) b * k b = ∑' (a : α), p a * k (g a)

Expectation of k : β → ℝ≥0∞ under p.map g equals expectation of k ∘ g under p.

theorem Cslib.Probability.PMF.tsum_bind_mul {α : Type u_1} {β : Type u_2} (p : PMF α) (f : α → PMF β) (k : β → ENNReal) : ∑' (b : β), (p.bind f) b * k b = ∑' (a : α), p a * ∑' (b : β), (f a) b * k b

Expectation of k : β → ℝ≥0∞ under p.bind f decomposes as an iterated expectation.

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.sq_tsum_le_tsum_sq {α : Type u_1} (μ : PMF α) {g : α → ℝ} (h0 : ∀ (a : α), 0 ≤ g a) (h1 : ∀ (a : α), g a ≤ 1) : (∑' (a : α), (μ a).toReal * g a) ^ 2 ≤ ∑' (a : α), (μ a).toReal * g a ^ 2

Jensen's inequality E[g]² ≤ E[g²] for a function with values in [0, 1].

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.