English
If μ ≪ ν and llr μ ν is μ-integrable, then the quantity ∫ llr μ ν dμ + μ.real univ * log(ν.real univ) + 1 − μ.real univ is nonnegative.
Русский
Если μ ≪ ν и llr μ ν интегрируем по μ, то ∫ llr μ ν dμ + μ.real univ * log(ν.real univ) + 1 − μ.real univ ≥ 0.
LaTeX
$$$0 \\le \\int x\\, llr\\,μ\\,ν\\,x\\,∂μ + μ.real univ * \\log(ν.real univ) + 1 - μ.real univ$$$
Lean4
theorem integral_llr_add_mul_log_nonneg (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
0 ≤ ∫ x, llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ :=
by
by_cases hμ : μ = 0
· simp [hμ]
by_cases hν : ν = 0
· refine absurd ?_ hμ
rw [hν] at hμν
exact Measure.absolutelyContinuous_zero_iff.mp hμν
have : NeZero ν := ⟨hν⟩
let ν' := (ν univ)⁻¹ • ν
have hμν' : μ ≪ ν' := hμν.trans (Measure.absolutelyContinuous_smul (by simp))
have h := integral_llr_add_sub_measure_univ_nonneg hμν' ?_
swap
· rw [integrable_congr (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν]))]
exact h_int.sub (integrable_const _)
rw [integral_congr_ae (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν])),
integral_sub h_int (integrable_const _), integral_const, smul_eq_mul] at h
simpa using h
