Boolean distributions and Boolean predicates

The masses of true and false under a Boolean distribution sum to one (apply_true_add_apply_false, and toReal_true_add_toReal_false in real-valued units). Pushing a distribution forward along Boolean predicates (PMF.map), the true-mass is monotone under pointwise implication on the support (map_true_mono), satisfies union bounds (map_true_le_add, and map_true_le_sum over a finite index set with its List.range instance map_any_range_true_le_sum), is the expectation of the predicate's indicator (map_apply_true), and is complemented by negation (map_not_true).

Main results

• Cslib.Probability.PMF.apply_true_add_apply_false, Cslib.Probability.PMF.toReal_true_add_toReal_false, Cslib.Probability.PMF.toReal_false_eq_one_sub, Cslib.Probability.PMF.toReal_true_eq_one_sub: Boolean outcome masses.
• Cslib.Probability.PMF.map_true_mono, Cslib.Probability.PMF.map_true_le_add, Cslib.Probability.PMF.map_true_le_sum, Cslib.Probability.PMF.map_any_range_true_le_sum, Cslib.Probability.PMF.map_apply_true, Cslib.Probability.PMF.map_not_true: monotonicity, union bounds, indicator expectations and complementation for Boolean predicates pushed forward along PMF.map.

theorem Cslib.Probability.PMF.apply_true_add_apply_false (p : PMF Bool) : p true + p false = 1

The probabilities of true and false under a Boolean distribution sum to one.

theorem Cslib.Probability.PMF.toReal_true_add_toReal_false (p : PMF Bool) : (p true).toReal + (p false).toReal = 1

The real-valued probabilities of true and false under a Boolean distribution sum to one.

theorem Cslib.Probability.PMF.toReal_false_eq_one_sub (p : PMF Bool) : (p false).toReal = 1 - (p true).toReal

The real-valued probability of false under a Boolean distribution is one minus the probability of true.

theorem Cslib.Probability.PMF.toReal_true_eq_one_sub (p : PMF Bool) : (p true).toReal = 1 - (p false).toReal

The real-valued probability of true under a Boolean distribution is one minus the probability of false.

theorem Cslib.Probability.PMF.map_true_mono {α : Type u_1} (p : PMF α) {E F : α → Bool} (h : ∀ a ∈ p.support, E a = true → F a = true) : (PMF.map E p) true ≤ (PMF.map F p) true

Pointwise implication on the support makes the mapped true-mass monotone.

theorem Cslib.Probability.PMF.map_true_le_add {α : Type u_1} (p : PMF α) {E A B : α → Bool} (h : ∀ a ∈ p.support, E a = true → A a = true ∨ B a = true) : (PMF.map E p) true ≤ (PMF.map A p) true + (PMF.map B p) true

Union bound for two Boolean predicates pushed forward along p.map.

theorem Cslib.Probability.PMF.map_true_le_sum {α : Type u_1} {ι : Type u_2} (p : PMF α) (s : Finset ι) {E : α → Bool} {F : ι → α → Bool} (h : ∀ a ∈ p.support, E a = true → ∃ i ∈ s, F i a = true) : (PMF.map E p) true ≤ ∑ i ∈ s, (PMF.map (F i) p) true

Union bound over a finite family of Boolean predicates pushed forward along p.map: if every possible outcome satisfying E satisfies some F i with i ∈ s, the true-mass of E is at most the sum of the true-masses of the F i.

theorem Cslib.Probability.PMF.map_any_range_true_le_sum {α : Type u_1} (p : PMF α) (K : ℕ) (F : ℕ → α → Bool) : (PMF.map (fun (a : α) => (List.range K).any fun (j : ℕ) => F j a) p) true ≤ ∑ j ∈ Finset.range K, (PMF.map (F j) p) true

Union bound for List.any over List.range K pushed forward along p.map: the List.range instance of map_true_le_sum.

theorem Cslib.Probability.PMF.map_apply_true {α : Type u_1} (p : PMF α) (E : α → Bool) : (PMF.map E p) true = ∑' (a : α), p a * if E a = true then 1 else 0

The true-mass of a Boolean predicate pushed forward along p.map is the expectation of its indicator.

theorem Cslib.Probability.PMF.map_not_true {α : Type u_1} (p : PMF α) (E : α → Bool) : (PMF.map (fun (a : α) => !E a) p) true = 1 - (PMF.map E p) true

Negating a Boolean predicate complements its true-mass in ℝ≥0∞.