-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
lemma mul_log_le_toReal_klDiv (hμν : μ ≪ ν) (h_int : Integrable (llr μ ν) μ) :
    (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal
      ≤ (klDiv μ ν).toReal

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Tactic:
by_cases hν : ν = 0

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Tactic:
rw [hν] at hμν

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ 0
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (ν univ).toReal * ((μ univ).toReal / (ν univ).toReal) = (μ univ).toReal

Tactic:
rw [mul_div_cancel₀]

Result:
case hb
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (ν univ).toReal ≠ 0

Proof state:
case hb
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (ν univ).toReal ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Tactic:
by_cases hμ : μ = 0

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : μ = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : (ν univ).toReal * ((μ univ).toReal / (ν univ).toReal) = (μ univ).toReal
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal =
    (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal)

Tactic:
rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Tactic:
refine absurd ?_ hμ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : μ = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Tactic:
simp [hμ]

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ 0
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Tactic:
exact Measure.absolutelyContinuous_zero_iff.mp hμν

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal =
    (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal)

Tactic:
have : (ν univ).toReal * ((μ univ).toReal / (ν univ).toReal) = (μ univ).toReal := by
  rw [mul_div_cancel₀]; simp [ENNReal.toReal_eq_zero_iff, hν]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : (ν univ).toReal * ((μ univ).toReal / (ν univ).toReal) = (μ univ).toReal
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal =
    (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal)

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal ≤ (klDiv μ ν).toReal

Tactic:
refine (le_of_eq ?_).trans (mul_klFun_le_toReal_klDiv hμν h_int)

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ (μ univ).toReal * log ((μ univ).toReal / (ν univ).toReal) + (ν univ).toReal - (μ univ).toReal =
    (ν univ).toReal * klFun ((μ univ).toReal / (ν univ).toReal)