English
For f, g, s with s measurable and μ finite on s, the tilted set lintegral satisfies a product rule with the density against μ.
Русский
Для f, g и измеримого множества s выполняется формула аналогичная правилу произведения плотности.
LaTeX
$$$$\\int_{s} g(x) \\, d(\\mu^{\\mathrm{tilted}} f) = \\int_{s} (\\frac{\\exp(f(x))}{\\int \\exp(f) d\\mu}) \\cdot g(x) \\, d\\mu.$$$$
Lean4
theorem setLIntegral_tilted [SFinite μ] (f : α → ℝ) (g : α → ℝ≥0∞) (s : Set α) :
∫⁻ x in s, g x ∂(μ.tilted f) = ∫⁻ x in s, ENNReal.ofReal (exp (f x) / ∫ x, exp (f x) ∂μ) * g x ∂μ :=
by
by_cases hf : AEMeasurable f μ
· rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
· simp only [Pi.mul_apply]
· refine AEMeasurable.restrict ?_
exact ((measurable_exp.comp_aemeasurable hf).div_const _).ennreal_ofReal
· filter_upwards
simp only [ENNReal.ofReal_lt_top, implies_true]
· have hf' : ¬Integrable (fun x ↦ exp (f x)) μ := by
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)
simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero, lintegral_zero_measure]
rw [integral_undef hf']
simp
