English
An identity relating the integrals of exponentials under tilting: ∫ exp(g) d(μ.tilted f) = ∫ exp(f+g) dμ / ∫ exp(f) dμ.
Русский
Соотношение интегралов экспонент под тильтингом: ∫ exp(g) d(μ.tilted f) = ∫ exp(f+g) dμ / ∫ exp(f) dμ.
LaTeX
$$$$\\int e^{g} \\, d(\\mu^{\\mathrm{tilted}} f) = \\frac{\\int e^{f+g} \\, d\\mu}{\\int e^{f} \\, d\\mu}.$$$$
Lean4
theorem integral_exp_tilted (f g : α → ℝ) :
∫ x, exp (g x) ∂(μ.tilted f) = (∫ x, exp ((f + g) x) ∂μ) / ∫ x, exp (f x) ∂μ := by
cases eq_zero_or_neZero μ with
| inl h => rw [h]; simp
| inr h0 =>
rw [integral_tilted f]
simp_rw [smul_eq_mul]
have : ∀ x, (exp (f x) / ∫ x, exp (f x) ∂μ) * exp (g x) = (exp ((f + g) x) / ∫ x, exp (f x) ∂μ) :=
by
intro x
rw [Pi.add_apply, exp_add]
ring
simp_rw [this, div_eq_mul_inv]
rw [integral_mul_const]
