English
If f is integrable with respect to μ, then for any measurable set s, μ.tilted f (s) = ENNReal.ofReal (∫_s e^{f} dμ / ∫ e^{f} dμ). If f is not integrable, the tilted value is 0 on s.
Русский
Если f интегрируем по μ, то μ.tilted f (s) = ENNReal.ofReal (∫_s e^{f} dμ / ∫ e^{f} dμ); иначе 0.
LaTeX
$$$$\\mu^{\\mathrm{tilted}} f (s) = \\begin{cases} \\mathrm{ENNReal.ofReal}\\left(\\dfrac{\\int_{s} e^{f} d\\mu}{\\int e^{f} d\\mu}\\right), & \\text{если } f \\text{ интегрируема}, \\\\ 0, & \\text{иначе}. \\end{cases}$$$$
Lean4
theorem tilted_apply_eq_ofReal_integral' {s : Set α} (f : α → ℝ) (hs : MeasurableSet s) :
μ.tilted f s = ENNReal.ofReal (∫ a in s, exp (f a) / ∫ x, exp (f x) ∂μ ∂μ) :=
by
by_cases hf : Integrable (fun x ↦ exp (f x)) μ
· rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal]
· exact hf.integrableOn.div_const _
· exact ae_of_all _ (fun _ ↦ by positivity)
·
simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero, Pi.zero_apply, integral_undef hf,
div_zero, integral_zero, ENNReal.ofReal_zero]
