PMF constructors and ℝ-coercion utilities beyond mathlib's basic surface

Two layers:

ℝ-coercion utilities — toRealFn, sum_toRealFn_eq_one, and nonneg/≤1 lemmas. The standard way to access a PMF α's masses as ℝ-valued (via ENNReal.toReal) without losing the 0 ≤ · ≤ 1 / sum-to-1 invariants.

ℝ-valued constructor — PMF.ofRealWeightFn, the canonical entry point for "I have non-negative ℝ weights and want a PMF":

Constructor	Input	Specialises
PMF.ofRealWeightFn	(α → ℝ) non-negative + element-witness positivity (Fintype)	lifts via ENNReal.ofReal and routes through mathlib's PMF.normalize

The constructor takes a specific positive witness (a : α) (h : 0 < f a) rather than the existential form (∃ a, 0 < f a). This avoids Classical.choose in the body and matches the shape of mathlib's own PMF.normalize hypotheses (tsum f ≠ 0, which is tsum_ne_zero_iff- equivalent to a single witness via ENNReal.summable.tsum_ne_zero_iff). For consumers holding 0 < ∑ a, f a instead, derive a witness via Finset.sum_pos.

[UPSTREAM] candidate: ofRealWeightFn fits cleanly into Mathlib/Probability/ProbabilityMassFunction/Constructions.lean as the standard "non-negative real weights" entry point, paralleling ofFintype (already-normalised ℝ≥0∞) and normalize (general ℝ≥0∞).

Note on PMF.normalize for Fintype ℝ≥0∞-valued weights: there is no wrapper — call PMF.normalize f hf0 hf directly. The hypothesis boilerplate at Fintype call sites is:

PMF.normalize f
  (ENNReal.summable.tsum_ne_zero_iff.mpr ⟨a, h_pos⟩)
  (ENNReal.tsum_ne_top_of_fintype h_finite)

A normalizeOfFintype wrapper around this pattern was tried and removed (0.231.X) — it bundled marginal value at the cost of an extra layer.

theorem ENNReal.tsum_ne_top_of_fintype {α : Type u_1} [Fintype α] {f : α → ENNReal} (h : ∀ (a : α), f a ≠ ⊤) : ∑' (a : α), f a ≠ ⊤

On a finite type, an ENNReal tsum is finite iff every term is. Convenience composition of tsum_fintype + ENNReal.sum_ne_top — the combined form is the natural hypothesis shape for PMF.normalize / PMF.posterior consumers.

noncomputable def PMF.toRealFn {α : Type u_1} (p : PMF α) : α → ℝ

Coerce a PMF α's mass function from ℝ≥0∞ to ℝ.

Equations

• p.toRealFn a = (p a).toReal

theorem PMF.toRealFn_nonneg {α : Type u_1} (p : PMF α) (a : α) : 0 ≤ p.toRealFn a

theorem PMF.toRealFn_le_one {α : Type u_1} (p : PMF α) (a : α) : p.toRealFn a ≤ 1

@[simp]

theorem PMF.uniformOfFintype_toRealFn {α : Type u_1} [Fintype α] [Nonempty α] (a : α) : (uniformOfFintype α).toRealFn a = (↑(Fintype.card α))⁻¹

Mass of the uniform distribution, in ℝ.

theorem PMF.sum_toRealFn_eq_one {α : Type u_1} [Fintype α] (p : PMF α) : ∑ a : α, p.toRealFn a = 1

For a [Fintype α] PMF, the toReal-coerced masses sum to 1.

Convex mixture

noncomputable def PMF.mix {α : Type u_1} (r : NNReal) (hr : r ≤ 1) (p q : PMF α) : PMF α

Convex combination of two PMFs at rate r: draw a Bernoulli-r coin, then sample q on heads and p on tails. Normalization is free from bind — no Fintype, no sum proof.

Equations

• PMF.mix r hr p q = (PMF.bernoulli r hr).bind fun (b : Bool) => bif b then q else p

@[simp]

theorem PMF.mix_apply {α : Type u_1} (r : NNReal) (hr : r ≤ 1) (p q : PMF α) (a : α) : (mix r hr p q) a = (1 - ↑r) * p a + ↑r * q a

theorem PMF.toRealFn_mix {α : Type u_1} (r : NNReal) (hr : r ≤ 1) (p q : PMF α) (a : α) : (mix r hr p q).toRealFn a = (1 - ↑r) * p.toRealFn a + ↑r * q.toRealFn a

The mixture in ℝ: (1 − r)·p + r·q pointwise.

noncomputable def PMF.ofRealWeightFn {α : Type u_1} [Fintype α] (f : α → ℝ) (_h_nonneg : ∀ (a : α), 0 ≤ f a) (h_pos : 0 < ∑ a : α, f a) : PMF α

Normalize non-negative ℝ weights with positive total into a PMF. The _h_nonneg hypothesis is unused in the body (ENNReal.ofReal clamps negatives silently) but is kept so the spec lemmas characterise the result faithfully.

Equations

• PMF.ofRealWeightFn f _h_nonneg h_pos = PMF.normalize (fun (x : α) => ENNReal.ofReal (f x)) ⋯ ⋯

@[simp]

theorem PMF.ofRealWeightFn_apply {α : Type u_1} [Fintype α] (f : α → ℝ) (h_nonneg : ∀ (a : α), 0 ≤ f a) (h_pos : 0 < ∑ a : α, f a) (b : α) : (ofRealWeightFn f h_nonneg h_pos) b = ENNReal.ofReal (f b) * (∑ x : α, ENNReal.ofReal (f x))⁻¹

Closed-form value of ofRealWeightFn in ℝ≥0∞.

theorem PMF.ofRealWeightFn_toRealFn_apply {α : Type u_1} [Fintype α] (f : α → ℝ) (h_nonneg : ∀ (a : α), 0 ≤ f a) (h_pos : 0 < ∑ a : α, f a) (b : α) : (ofRealWeightFn f h_nonneg h_pos).toRealFn b = f b / ∑ x : α, f x

Closed form in ℝ: each mass is its weight divided by the total.

theorem PMF.support_ofRealWeightFn {α : Type u_1} [Fintype α] (f : α → ℝ) (h_nonneg : ∀ (a : α), 0 ≤ f a) (h_pos : 0 < ∑ a : α, f a) : (ofRealWeightFn f h_nonneg h_pos).support = {x : α | 0 < f x}

Support of ofRealWeightFn: the strictly-positive weights.

theorem PMF.ofRealWeightFn_toRealFn_eq {α : Type u_1} [Fintype α] (f : α → ℝ) (h_nonneg : ∀ (a : α), 0 ≤ f a) (h_pos : 0 < ∑ a : α, f a) (h_sum_one : ∑ a : α, f a = 1) : (ofRealWeightFn f h_nonneg h_pos).toRealFn = f

Already-normalised weights are recovered exactly.

Iterated conditioning

theorem PMF.filter_filter {α : Type u_1} (p : PMF α) {s s' : Set α} (hss : s' ⊆ s) (h : ∃ a ∈ s, a ∈ p.support) (h'' : ∃ a ∈ s', a ∈ p.support) (h' : ∃ a ∈ s', a ∈ (p.filter s h).support) : (p.filter s h).filter s' h' = p.filter s' h''

Iterated conditioning collapses: filtering on s, then on a subevent s' ⊆ s, is filtering on s' directly. Incremental Bayesian update by restriction agrees with direct conditioning ([Lev08]'s eqs. (5)–(8)). [UPSTREAM] candidate for Mathlib/Probability/ProbabilityMassFunction.

theorem PMF.tsum_indicator_filter_of_subset {α : Type u_1} (p : PMF α) {s s' : Set α} (hss : s' ⊆ s) (h : ∃ a ∈ s, a ∈ p.support) : ∑' (a : α), s'.indicator (⇑(p.filter s h)) a = (∑' (a : α), s'.indicator (⇑p) a) / ∑' (a : α), s.indicator (⇑p) a

Conditional mass of a subevent under filtering: for s' ⊆ s, the filtered distribution gives s' the mass p(s') / p(s).

theorem PMF.toMeasure_ne_zero {α : Type u_1} [MeasurableSpace α] (p : PMF α) {s : Set α} (hs : MeasurableSet s) (h : ∃ a ∈ s, a ∈ p.support) : p.toMeasure s ≠ 0

A set meeting the support has nonzero measure.

theorem PMF.toMeasure_filter {α : Type u_1} [MeasurableSpace α] (p : PMF α) {s : Set α} (hs : MeasurableSet s) (h : ∃ a ∈ s, a ∈ p.support) : (p.filter s h).toMeasure = p.toMeasure[|s]

PMF.filter is Measure.cond: conditioning a PMF on an event agrees with the measure-theoretic conditional measure. [UPSTREAM] candidate — it connects mathlib's two conditioning notions.