ofFintype — Mathlib

English

Given a finite type α and a function f: α → ℝ≥0∞ with total sum 1, define a PMF on α by summing over all a in α.

Русский

Пусть α — конечный тип, f: α → ℝ≥0∞ и сумма по α равна 1; задаём PMF на α суммированием по a ∈ α.

LaTeX

$$$ ofFintype f h : PMF α $$$

Lean4

/-- Given a finite type `α` and a function `f : α → ℝ≥0∞` with sum 1, we get a `PMF`. -/
def ofFintype [Fintype α] (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) : PMF α :=
  ofFinset f Finset.univ h fun a ha => absurd (Finset.mem_univ a) ha

Похожие утверждения