English
Let f: α → ℝ and μ be a measure on α. If exp(f) is μ-integrable, then for every normed additive group E and every function g: α → E, g is integrable with respect to the tilted measure μ tilted by f if and only if exp(f) · g is μ-integrable.
Русский
Пусть f: α → ℝ и μ — мера на α. Если exp(f) интегрируема по μ, то для любой нормированной абелевой группы E и любой функции g: α → E интегрируемость g понаклонённой к f мере μ эквивалентна интегрируемости exp(f) · g по μ.
LaTeX
$$$\\text{If } \\int e^{f} \\,d\\mu < \\infty \\text{ then } \\mathrm{Integrable}(g;\\mu^{\\tilde f}) \\iff \\mathrm{Integrable}(e^{f}\\cdot g;\\mu).$$$
Lean4
theorem integrable_tilted_iff {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : α → ℝ}
(hf : Integrable (fun x ↦ exp (f x)) μ) (g : α → E) :
Integrable g (μ.tilted f) ↔ Integrable (fun x ↦ exp (f x) • g x) μ :=
by
by_cases hμ : μ = 0
· simp [hμ]
have hf_meas : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
rw [Measure.tilted, integrable_withDensity_iff_integrable_smul₀' (by fun_prop) (by simp)]
calc
Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
_ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ :=
by
congr! with a
rw [ENNReal.toReal_ofReal]
positivity
_ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ :=
by
congr! 2 with a
rw [smul_smul, div_eq_inv_mul]
_ ↔ Integrable (fun x ↦ exp (f x) • g x) μ :=
by
rw [integrable_fun_smul_iff]
simp only [ne_eq, inv_eq_zero]
have : NeZero μ := ⟨hμ⟩
exact (integral_exp_pos hf).ne'
