mul_log_le_toReal_klDiv — Mathlib

English

A variant of the lower bound: μ.univ * log( μ.univ/ν.univ ) + ν.univ − μ.univ ≤ (klDiv μ ν).toReal, under AC and integrability (with a simplification).

Русский

Вариант нижней границы: μ.univ * log( μ.univ/ν.univ ) + ν.univ − μ.univ ≤ (klDiv μ ν).toReal при AC и интегрируемости (с упрощением).

LaTeX

$$$μ.real univ * \\log\\left(\\frac{μ.real univ}{ν.real univ}\\right) + ν.real univ - μ.real univ ≤ (klDiv\\,μ\\,ν).toReal$$$

Lean4

theorem mul_log_le_toReal_klDiv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal :=
  by
  by_cases hμ : μ = 0
  · simp [hμ, measureReal_def]
  by_cases hν : ν = 0
  · refine absurd ?_ hμ
    rw [hν] at hμν
    exact Measure.absolutelyContinuous_zero_iff.mp hμν
  refine (le_of_eq ?_).trans (mul_klFun_le_toReal_klDiv hμν h_int)
  have : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ := by rw [mul_div_cancel₀];
    simp [ENNReal.toReal_eq_zero_iff, hν, measureReal_def]
  rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]

Похожие утверждения