normalize_apply

Mathlib.Probability.ProbabilityMassFunction.Constructions

URI: https://scilib.ai/kg/mathlib#PMF.normalize_apply

Lean4

@[simp]
theorem normalize_apply (a : α) : (normalize f hf0 hf) a = f a * (∑' x, f x)⁻¹ :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru