-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma integral_klFun_rnDeriv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν
      = ∫ x, llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
  mul_one]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + (ν univ).toReal - (μ univ).toReal =
    ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a => (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν

case hg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a => 1) ν

case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν

case hg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal) ν

Proof state:
case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + (ν univ).toReal - (μ univ).toReal =
    ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
congr 2

Result:
case e_a.e_a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν = ∫ (x : α), llr μ ν x ∂μ

Proof state:
case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν

Tactic:
refine Integrable.add ?_ (integrable_const _)

Result:
case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν

Proof state:
case hg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun x => (μ.rnDeriv ν x).toReal) ν

Tactic:
fun_prop

Result:
no goals

Proof state:
case hf
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a => (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν

Tactic:
rwa [integrable_rnDeriv_mul_log_iff hμν]

Result:
no goals

Proof state:
case e_a.e_a
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν = ∫ (x : α), llr μ ν x ∂μ

Tactic:
exact integral_rnDeriv_smul hμν

Result:
no goals

Proof state:
case hg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (fun a => 1) ν

Tactic:
fun_prop

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal

Tactic:
unfold klFun

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal