integrable_klFun_rnDeriv_iff — Mathlib

English

klFun is not differentiable within (−∞, 0) at 0.

Русский

klFun не дифференцируема внутри (−∞,0) в 0.

LaTeX

$$$\\neg\\DifferentiableWithinAt(\\mathbb{R}, \\mathrm{klFun}, (-\\infty,0), 0)$$$

Lean4

/-- For two finite measures `μ ≪ ν`, the function `x ↦ klFun (μ.rnDeriv ν x).toReal` is integrable
with respect to `ν` iff `llr μ ν` is integrable with respect to `μ`. -/
theorem integrable_klFun_rnDeriv_iff (hμν : μ ≪ ν) :
    Integrable (fun x ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ :=
  by
  suffices
    Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)) ν ↔
      Integrable (llr μ ν) μ
    by
    convert this using 3 with x
    rw [klFun, add_sub_assoc]
  rw [integrable_add_iff_integrable_left', integrable_rnDeriv_mul_log_iff hμν]
  fun_prop

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