Finite-fintype convenience naming for Mathlib.PMF

PMF α (mathlib) is the canonical probability monad in this library, but its measure-theoretic API names (toOuterMeasure, cond) read awkwardly in linguistic content. This file is a paper-thin naming layer:

• probOfSet p s := p.toOuterMeasure s
• condProbSet p cond target := p.toOuterMeasure (cond ∩ target) / p.toOuterMeasure cond

Both are abbrevs — definitionally equal to the mathlib forms — so any mathlib lemma about toOuterMeasure (e.g. toOuterMeasure_apply_fintype) applies directly and no MeasurableSpace instance is required.

The conditional ratio is unguarded: ENNReal's 0 / 0 = 0 and x ≤ p.toOuterMeasure cond (monotonicity) jointly imply condProbSet p cond target = 0 whenever p.toOuterMeasure cond = 0, which matches ProbabilityTheory.cond's convention.

A handful of lemmas (positivity, monotonicity, partition, complement, finite normalization) are provided for the patterns that recur in Theories/Semantics/Questions/Probabilistic.lean and the corresponding Phenomena/.../Studies/ files. ENNReal arithmetic at consumer sites goes through ennreal_arith (see Linglib.Tactics.ENNRealArith).

@[reducible, inline]

noncomputable abbrev PMF.probOfSet {α : Type u_1} (p : PMF α) (s : Set α) : ENNReal

Probability mass of a set under a finite-fintype PMF, named to match linguistic content. Definitionally p.toOuterMeasure s, so every mathlib lemma about toOuterMeasure applies.

Equations

• p.probOfSet s = p.toOuterMeasure s

@[reducible, inline]

noncomputable abbrev PMF.condProbSet {α : Type u_1} (p : PMF α) (cond target : Set α) : ENNReal

Conditional probability P(target | cond) as a direct ratio. ENNReal's 0/0 = 0 convention plus x ≤ p.toOuterMeasure cond (monotonicity) handle the degenerate case automatically — no if guard needed. Matches ProbabilityTheory.cond_apply's convention.

Equations

• p.condProbSet cond target = p.toOuterMeasure (cond ∩ target) / p.toOuterMeasure cond

theorem PMF.probOfSet_apply {α : Type u_1} [Fintype α] (p : PMF α) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : p.probOfSet s = ∑ a : α, if a ∈ s then p a else 0

probOfSet reduces to the indicator-sum form on a finite type. This is just PMF.toOuterMeasure_apply_fintype rephrased with if-then-else in place of Set.indicator.

@[simp]

theorem PMF.probOfSet_empty {α : Type u_1} [Fintype α] (p : PMF α) : p.probOfSet ∅ = 0

@[simp]

theorem PMF.probOfSet_univ {α : Type u_1} [Fintype α] (p : PMF α) : p.probOfSet Set.univ = 1

theorem PMF.probOfSet_mono {α : Type u_1} (p : PMF α) {s t : Set α} (h : s ⊆ t) : p.probOfSet s ≤ p.probOfSet t

theorem PMF.probOfSet_inter_le_right {α : Type u_1} (p : PMF α) (s t : Set α) : p.probOfSet (s ∩ t) ≤ p.probOfSet t

theorem PMF.probOfSet_inter_le_left {α : Type u_1} (p : PMF α) (s t : Set α) : p.probOfSet (s ∩ t) ≤ p.probOfSet s

theorem PMF.probOfSet_le_one {α : Type u_1} [Fintype α] (p : PMF α) (s : Set α) : p.probOfSet s ≤ 1

probOfSet is bounded by 1.

theorem PMF.probOfSet_ne_top {α : Type u_1} [Fintype α] (p : PMF α) (s : Set α) : p.probOfSet s ≠ ⊤

probOfSet is finite.

theorem PMF.probOfSet_partition {α : Type u_1} [Fintype α] (p : PMF α) (s t : Set α) [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : α) => x ∈ t] : p.probOfSet s = p.probOfSet (s ∩ t) + p.probOfSet (s ∩ tᶜ)

Partition: P(s) = P(s ∩ t) + P(s ∩ tᶜ).

theorem PMF.probOfSet_compl_add {α : Type u_1} [Fintype α] (p : PMF α) (s : Set α) [DecidablePred fun (x : α) => x ∈ s] : p.probOfSet s + p.probOfSet sᶜ = 1

P(s) + P(sᶜ) = 1.

theorem PMF.condProbSet_eq_div {α : Type u_1} (p : PMF α) (cond target : Set α) : p.condProbSet cond target = p.probOfSet (cond ∩ target) / p.probOfSet cond

condProbSet is by definition the ratio. Provided as a named lemma so consumers can rw [condProbSet_eq_div] rather than unfold an abbrev.

theorem PMF.condProbSet_of_zero {α : Type u_1} (p : PMF α) (cond target : Set α) (h : p.probOfSet cond = 0) : p.condProbSet cond target = 0

When P(cond) = 0, the conditional probability is 0.

theorem PMF.condProbSet_compl_sum {α : Type u_1} [Fintype α] (p : PMF α) (cond target : Set α) [DecidablePred fun (x : α) => x ∈ cond] [DecidablePred fun (x : α) => x ∈ target] (h : p.probOfSet cond > 0) : p.condProbSet cond target + p.condProbSet cond targetᶜ = 1

P(target | cond) + P(targetᶜ | cond) = 1 when P(cond) > 0.

theorem PMF.probOfSet_pos_of_condProbSet_gt {α : Type u_1} (p : PMF α) (cond target : Set α) (h : p.condProbSet cond target > p.probOfSet target) : p.probOfSet cond > 0

If P(target | cond) > P(target) then P(cond) > 0.

noncomputable def PMF.impactRatio {α : Type u_1} (p : PMF α) (R A : Set α) : ENNReal

The "impact" of evidence R on proposition A: P(A | R) / P(A). The Bayes-factor face of conditional probability; equals 1 when R provides no information about A, exceeds 1 when R raises A's probability, falls below 1 when R lowers it. Used in probabilistic answerhood (Thomas 2026 Def. 62b) and structurally identical to RSA's posterior-ratio update.

Equations

• p.impactRatio R A = p.condProbSet R A / p.probOfSet A

theorem PMF.condProbSet_strict_anti_of_probOfSet_lt {α : Type u_1} [Fintype α] (p : PMF α) (A R R' : Set α) [DecidablePred fun (x : α) => x ∈ A] [DecidablePred fun (x : α) => x ∈ R] [DecidablePred fun (x : α) => x ∈ R'] (hAR : A ⊆ R) (hAR' : A ⊆ R') (hPosA : p.probOfSet A > 0) (hLt : p.probOfSet R < p.probOfSet R') : p.condProbSet R A > p.condProbSet R' A

When A ⊆ R ⊆ R' and P(R) < P(R') strictly, conditioning on the larger set R' strictly decreases P(A | ·) (for A of positive prior).

Proof: condProbSet R A = P(A∩R)/P(R) = P(A)/P(R) since A ⊆ R, and similarly condProbSet R' A = P(A)/P(R'). The conclusion is then ENNReal strict-antitone-in-denominator, ENNReal.div_lt_div_left.

Conditional expectation given a set

E[f ∣ A] = (∑_{a ∈ A} p(a) · f(a)) / P(A). Mathlib's heavy MeasureTheory.condExp takes a sub-σ-algebra and produces a random variable; the lightweight finite-PMF "expected value given a set" is just a number. Equivalent (via PMF.integral_eq_sum and MeasureTheory.Measure.cond) to ∫ f d(p.toMeasure.cond A); we keep the direct ∑/∑ form for decide-checkability.

noncomputable def PMF.condExpect {α : Type u_1} [Fintype α] (p : PMF α) (A : Set α) (f : α → ENNReal) : ENNReal

Conditional expectation E[f ∣ A]. Set.indicator keeps the signature decidability-free; ENNReal's 0/0 = 0 handles P(A) = 0.

Equations

• p.condExpect A f = (∑ a : α, A.indicator (fun (a : α) => p a * f a) a) / p.probOfSet A

theorem PMF.condExpect_eq_div {α : Type u_1} [Fintype α] (p : PMF α) (A : Set α) (f : α → ENNReal) : p.condExpect A f = (∑ a : α, A.indicator (fun (a : α) => p a * f a) a) / p.probOfSet A

condExpect as an explicit ratio.

theorem PMF.condExpect_indicator {α : Type u_1} [Fintype α] (p : PMF α) (A B : Set α) : p.condExpect A (B.indicator fun (x : α) => 1) = p.condProbSet A B

When the value function is the indicator of B, condExpect reduces to condProbSet.

theorem PMF.condExpect_add {α : Type u_1} [Fintype α] (p : PMF α) (A : Set α) (f g : α → ENNReal) : p.condExpect A (f + g) = p.condExpect A f + p.condExpect A g

Linearity of condExpect in f. Not @[simp]: pointwise addition is the simp normal form, so this lemma is for forward reasoning.

@[simp]

theorem PMF.condExpect_zero {α : Type u_1} [Fintype α] (p : PMF α) (A : Set α) : p.condExpect A 0 = 0