_aux_Mathlib_Probability_Notation___macroRules_ProbabilityTheory_term∂_/∂__1

English

The sum of coefficients of a PMF is not top; in particular, it is not infinite.

Русский

Сумма коэффициентов PMF не бесконечна.

LaTeX

$$$\sum' a, \mathrm{p}(a) \neq \infty$$$

Lean4

@[scoped macro ProbabilityTheory.«term∂_/∂_»]
public meta def «_aux_Mathlib_Probability_Notation___macroRules_ProbabilityTheory_term∂_/∂__1» : Macro✝ := fun
  | `(∂$P/∂$Q) => ``(MeasureTheory.Measure.rnDeriv $P $Q)
  | _ => no_error_if_unused% throw✝ Lean.Macro.Exception.unsupportedSyntax✝

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