cgf_const — Mathlib

English

Let μ be a probability measure and c ∈ R. For the constant function f(ω) ≡ c, the cumulant generating function is cgf(f; μ; t) = t c.

Русский

Пусть μ — распределение с суммой массы 1 и пусть f(ω) ≡ c. Тогда для константной функции имеет cgf(f; μ; t) = t c.

LaTeX

$$$\operatorname{cgf}(\text{const } c)\;\mu\;t = t c$$$

Lean4

@[simp]
theorem cgf_const [IsProbabilityMeasure μ] (c : ℝ) : cgf (fun _ => c) μ t = t * c := by
  simp only [cgf, mgf_const, log_exp]

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