English
Let Ω be a space with a finite measure μ. For a real-valued observable X and a real parameter t, the tilted measure μ_tilted(t X) assigns to a measurable s the ENNReal value of the integral of e^{t X} with a normalizing factor given by the cumulant generating function. Equivalently, the measure is absolutely continuous with respect to μ with density proportional to e^{t X} up to the normalizing constant exp(cgf X μ t).
Русский
Пусть Ω — множество с мерой μ (конечная мера). Пусть X: Ω→ℝ и t∈ℝ. Смещённая мера μ_tilted(t X) присваивает измеримому множеству s число μ_tilted(t X)(s), равное ENNReal.ofReal(∫_{a∈s} e^{t X(a) − cgf(X, μ, t)} dμ). Эквивалентно, плотность μ_tilted(t X) по отношению к μ пропорциональна e^{t X}, нормируемая mgf.
LaTeX
$$$\\mu^{\\sim}_{tX}(s) = \\operatorname{ENNReal}.ofReal\\left(\\int_{a \\in s} e^{t X(a) - \\operatorname{cgf}(X, \\mu, t)} \\, d\\mu(a)\\right)$$$
Lean4
theorem tilted_mul_apply_eq_ofReal_integral_cgf [SFinite μ] (s : Set Ω) (ht : Integrable (fun ω ↦ exp (t * X ω)) μ) :
μ.tilted (t * X ·) s = ENNReal.ofReal (∫ a in s, exp (t * X a - cgf X μ t) ∂μ) :=
by
rcases eq_zero_or_neZero μ with rfl | hμ
· simp
· simp_rw [tilted_mul_apply_eq_ofReal_integral_mgf s, exp_sub]
rwa [exp_cgf]
