map_ofFintype — Mathlib

English

Mapping an PMF from α to β via g distributes over the sum of f along fibers of g.

Русский

Отображение PMF через g распределяет сумму по волокнам g.

LaTeX

$$$ PMF.map g (PMF.ofFintype f h) = PMF.ofFintype (fun b => (\tfrac{\sum a with g a = b, f a}) ) $$$

Lean4

@[simp]
theorem map_ofFintype [Fintype β] (f : α → ℝ≥0∞) (h : ∑ a, f a = 1) (g : α → β) :
    (ofFintype f h).map g =
      ofFintype (fun b ↦ ∑ a with g a = b, f a) (by simpa [Finset.sum_fiberwise_eq_sum_filter univ univ g f]) :=
  by
  ext b : 1
  simp only [sum_filter, eq_comm, map_apply, ofFintype_apply]
  exact tsum_eq_sum fun _ h ↦ (h <| mem_univ _).elim

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