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

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.

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

Construct a PMF α over a Fintype from a non-negative ℝ-valued weight function with one positivity witness. Lifts to ℝ≥0∞ via ENNReal.ofReal and routes through mathlib's PMF.normalize.

The _h_nonneg hypothesis is unused in the body (ENNReal.ofReal clamps negatives to 0 silently), but is kept on the signature because the spec lemmas support_ofRealWeightFn and ofRealWeightFn_toRealFn_eq require non-negativity to characterise the result faithfully.

Equations

• PMF.ofRealWeightFn f _h_nonneg a 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) (a : α) (h_pos : 0 < f a) (b : α) : (ofRealWeightFn f h_nonneg a h_pos) b = ENNReal.ofReal (f b) * (∑ x : α, ENNReal.ofReal (f x))⁻¹

Closed-form value of ofRealWeightFn: each mass is the ENNReal.ofReal of the weight, divided by the sum of ofReal-lifted weights.

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

Support of ofRealWeightFn is the set of strictly-positive weights — non-negative weights of 0 get cast to ENNReal.ofReal 0 = 0 and drop out.

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

Round-trip: when f is already normalised (sums to 1 in ℝ), ofRealWeightFn's normalisation divides by 1, recovering f exactly through toRealFn.