mul_klFun_le_toReal_klDiv — Mathlib

English

Under AC and integrability, ν(univ) * klFun( μ(univ)/ν(univ) ) ≤ (klDiv μ ν).toReal.

Русский

При условии AC и интегрируемости, ν(univ) * klFun( μ(univ)/ν(univ) ) ≤ (klDiv μ ν).toReal.

LaTeX

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

Lean4

theorem mul_klFun_le_toReal_klDiv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    ν.real univ * klFun (μ.real univ / ν.real univ) ≤ (klDiv μ ν).toReal := by
  calc
    ν.real univ * klFun (μ.real univ / ν.real univ)
    _ ≤ ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν :=
      by
      refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν
      rwa [integrable_klFun_rnDeriv_iff hμν]
    _ = (klDiv μ ν).toReal := by rw [toReal_klDiv_eq_integral_klFun hμν]

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