English
For f, g: α → ℝ in a normed space E, the tilted set integral equals the integral against μ of the density times g, i.e., ∫ x in s g(x) d(μ.tilted f) = ∫ x in s ((exp(f(x))/∫ exp(f) dμ) • g(x)) dμ.
Русский
Для f, g: α → ℝ и E-значений, тильтированная сумма равна интегралу плотности, умноженной на g.
LaTeX
$$$$\\int_{s} g(x) \\, d(\\mu^{\\mathrm{tilted}} f) = \\int_{s} \\left(\\frac{e^{f(x)}}{\\int e^{f} d\\mu}\\right) \\cdot g(x) \\, d\\mu.$$$$
Lean4
theorem setIntegral_tilted' (f : α → ℝ) (g : α → E) {s : Set α} (hs : MeasurableSet s) :
∫ x in s, g x ∂(μ.tilted f) = ∫ x in s, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ :=
by
by_cases hf : AEMeasurable f μ
· rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀ _ _ hs]
· congr
· suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ
by
rw [← aemeasurable_coe_nnreal_real_iff]
refine AEMeasurable.restrict ?_
simpa only [NNReal.coe_mk]
exact (measurable_exp.comp_aemeasurable hf).div_const _
· 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, integral_zero_measure]
rw [integral_undef hf']
simp
