Two-stage experiments

A two-stage experiment μ.bind f gives an outcome b the probability c when every possible second stage does (bind_apply_of_forall), and some possible first stage gives b at least the probability of the whole experiment (exists_bind_apply_le). Continuations need agree, or be compared, only on outcomes the first stage can produce (bind_congr_on_support, le_bind_apply_on_support, bind_apply_mono_on_support). Averages of bounded values are bounded (tsum_mul_le_of_forall_le, tsum_mul_le_card_mul_add), and the pairing law holds for dependent second samples (bind_sigma_apply).

Main results

• Cslib.Probability.PMF.bind_congr_on_support: continuations need agree only on possible inputs.
• Cslib.Probability.PMF.bind_apply_of_forall, Cslib.Probability.PMF.exists_bind_apply_le: outcome probabilities of two-stage experiments.
• Cslib.Probability.PMF.le_bind_apply_on_support, Cslib.Probability.PMF.bind_apply_mono_on_support: comparing continuations at one outcome.
• Cslib.Probability.PMF.tsum_mul_le_of_forall_le, Cslib.Probability.PMF.tsum_mul_le_card_mul_add: averages of bounded values.
• Cslib.Probability.PMF.bind_sigma_apply: the pairing law for dependent second samples.

References

Adapted in part from Probability/PMF.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8.

theorem Cslib.Probability.PMF.bind_sigma_apply {α : Type u_1} {β : α → Type u_3} (p : PMF α) (f : (a : α) → PMF (β a)) (a : α) (b : β a) : (p.bind fun (a : α) => PMF.map (Sigma.mk a) (f a)) ⟨a, b⟩ = p a * (f a) b

The pairing law also holds when the second sample's type depends on the first. Adapted from the cslib crypto branch at 5ff69ca.

theorem Cslib.Probability.PMF.bind_congr_on_support {α : Type u_1} {β : Type u_2} (p : PMF α) (f g : α → PMF β) (h : ∀ a ∈ p.support, f a = g a) : p.bind f = p.bind g

A continuation only needs to agree on outcomes the preceding distribution can produce.

theorem Cslib.Probability.PMF.bind_apply_of_forall {α : Type u_1} {β : Type u_2} (μ : PMF α) {f : α → PMF β} {b : β} {c : ENNReal} (h : ∀ (a : α), (f a) b = c) : (μ.bind f) b = c

If every second stage of a two-stage experiment gives the outcome b probability c, so does the experiment.

theorem Cslib.Probability.PMF.le_bind_apply_on_support {α : Type u_1} {β : Type u_2} (μ : PMF α) {f : α → PMF β} {b : β} {c : ENNReal} (h : ∀ a ∈ μ.support, c ≤ (f a) b) : c ≤ (μ.bind f) b

A lower bound on an outcome's probability for every possible first-stage result bounds its probability in the whole experiment.

theorem Cslib.Probability.PMF.bind_apply_mono_on_support {α : Type u_1} {β : Type u_2} (μ : PMF α) {f g : α → PMF β} (b : β) (h : ∀ a ∈ μ.support, (f a) b ≤ (g a) b) : (μ.bind f) b ≤ (μ.bind g) b

Increasing an outcome's probability on every possible first-stage result increases its probability in the whole experiment. The sample spaces may be infinite.

theorem Cslib.Probability.PMF.exists_bind_apply_le {α : Type u_1} {β : Type u_2} [Finite α] (μ : PMF α) (f : α → PMF β) (b : β) : ∃ a ∈ μ.support, (μ.bind f) b ≤ (f a) b

Some possible outcome of the first stage of a two-stage experiment does at least as well as the experiment.

theorem Cslib.Probability.PMF.tsum_mul_le_of_forall_le {α : Type u_1} (μ : PMF α) {f : α → ENNReal} {B : ENNReal} (h : ∀ (a : α), f a ≤ B) : ∑' (a : α), μ a * f a ≤ B

An average of values at most B is at most B.

theorem Cslib.Probability.PMF.tsum_mul_le_card_mul_add {α : Type u_1} [DecidableEq α] (μ : PMF α) {ε : ENNReal} (hμ : ∀ (a : α), μ a ≤ ε) (T : Finset α) {f : α → ENNReal} {B : ENNReal} (h : ∀ (a : α), f a ≤ (if a ∈ T then 1 else 0) + B) : ∑' (a : α), μ a * f a ≤ ↑T.card * ε + B

Values at most 1 on a finite set T and at most B elsewhere average to at most |T| * ε + B under a distribution giving every point probability at most ε.