-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
/-- **Converse Gibbs' inequality**: the Kullback-Leibler divergence between two finite measures is
zero if and only if the two measures are equal. -/
lemma klDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
    klDiv μ ν = 0 ↔ μ = ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1

Tactic:
filter_upwards [h] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ μ.rnDeriv ν x = 1 x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ klDiv μ ν ≠ ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ Measurable fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)

Tactic:
fun_prop

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ μ.rnDeriv ν x = 1 x

Tactic:
simp only [Pi.zero_apply, ENNReal.ofReal_eq_zero] at hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ μ.rnDeriv ν x = 1 x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
⊢ klDiv μ ν = 0 ↔ μ = ν

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ h ▸ klDiv_self _⟩

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ μ = ν

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ μ.rnDeriv ν x = 1 x

Tactic:
have hx' : klFun (μ.rnDeriv ν x).toReal = 0 := le_antisymm hx (klFun_nonneg ENNReal.toReal_nonneg)

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
⊢ μ.rnDeriv ν x = 1 x

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
⊢ μ.rnDeriv ν x = 1 x

Tactic:
rwa [klFun_eq_zero_iff ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff] at hx'

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ μ = ν

Tactic:
have h_ne : klDiv μ ν ≠ ⊤ := by simp [h]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : klDiv μ ν ≠ ⊤
⊢ μ = ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Tactic:
rw [klDiv_eq_lintegral_klFun, if_pos h_ne.1, lintegral_eq_zero_iff (by fun_prop)] at h

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : klDiv μ ν ≠ ⊤
⊢ μ = ν

Tactic:
rw [klDiv_ne_top_iff] at h_ne

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν

Tactic:
refine (Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
h : (fun x => ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) =ᶠ[ae ν] 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1