English
Let μ be a finite measure with μ(Ω) ≠ 0 and let c ∈ R. If f is the constant function f(ω) = c for all ω, then the cumulant generating function satisfies cgf(f; μ; t) = log μ(Ω) + t c.
Русский
Пусть μ — конечная мера на Ω с μ(Ω) ≠ 0, и пусть f(ω) = c константа. Тогда каноническая функция кумулянтов выполняет cgf(f; μ; t) = log μ(Ω) + t c.
LaTeX
$$$\operatorname{cgf}(\text{const } c)\;\mu\;t = \log(\mu(\Omega)) + t c$$$
Lean4
@[simp]
theorem cgf_const' [IsFiniteMeasure μ] (hμ : μ ≠ 0) (c : ℝ) : cgf (fun _ => c) μ t = log (μ.real Set.univ) + t * c :=
by
simp only [cgf, mgf_const']
rw [log_mul _ (exp_pos _).ne']
· rw [log_exp _]
· rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]
simp only [hμ, not_false_iff]
