awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
pos : ∀ (hμ : μ = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
neg : ∀ (hμ : ¬μ = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : μ = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
simp [hμ]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
pos : ∀ (hν : ν = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
neg : ∀ (hν : ¬ν = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
by_cases hν : ν = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
absurd ?_ hμ

Premises used: absurd
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
pos : μ = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
refine absurd ?_ hμ

Premises used: absurd
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ ≪ 0

Tactic:
rw [hν] at hμν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
hμν₁ : μ ≪ 0
⊢ Integrable (llr μ ν) μ

Tactic:
rw [hν] at hμν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
hμν₁ : μ ≪ 0
h_int₁ : Integrable (llr μ ν) μ
⊢ ¬μ = 0

Tactic:
rw [hν] at hμν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
hμν₁ : μ ≪ 0
h_int₁ : Integrable (llr μ ν) μ
hμ₁ : ¬μ = 0
⊢ ν = 0

Tactic:
rw [hν] at hμν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ 0
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Tactic:
Measure.absolutelyContinuous_zero_iff.mp hμν

Premises used: Iff.mp, MeasureTheory.Measure.absolutelyContinuous_zero_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ 0
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0

Tactic:
exact Measure.absolutelyContinuous_zero_iff.mp hμν

Premises used: Iff.mp, MeasureTheory.Measure.absolutelyContinuous_zero_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ NeZero ν

Tactic:
have : NeZero ν := ⟨hν⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ μ ≪ ν'

Tactic:
have hμν' : μ ≪ ν' := hμν.trans (Measure.absolutelyContinuous_smul (by simp))
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
neg :
  ∀ (h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ),
    0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
neg₁ : Integrable (llr μ ν') μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
have h := integral_llr_add_sub_measure_univ_nonneg hμν' ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hν]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹)) μ
⊢ Integrable (llr μ ν') μ

Tactic:
rw [integrable_congr (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν]))]

Premises used: MeasureTheory.integrable_congr, Set.univ, Inv.inv, MeasureTheory.llr_smul_right, DFunLike.coe
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹)) μ

Tactic:
h_int.sub (integrable_const _)

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.integrable_const
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹)) μ

Tactic:
exact h_int.sub (integrable_const _)

Premises used: MeasureTheory.Integrable.sub, MeasureTheory.integrable_const
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ
⊢ Ne (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hν]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ
⊢ 0 ≤
    ∫ (a : α), llr μ ν a ∂μ - μ.real univ * log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹) + ν'.real univ -
      μ.real univ

Tactic:
rw [integral_congr_ae (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν])),
    integral_sub h_int (integrable_const _), integral_const, smul_eq_mul] at h

Premises used: MeasureTheory.integral_congr_ae, Set.univ, MeasureTheory.integral_sub, Inv.inv, MeasureTheory.integral_const, smul_eq_mul, MeasureTheory.llr_smul_right, DFunLike.coe, MeasureTheory.integrable_const
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
h :
  0 ≤
    ∫ (a : α), llr μ ν a ∂μ - μ.real univ * log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹) + ν'.real univ -
      μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ

Tactic:
simpa using h
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν

Premises used: MeasureTheory.mul_le_integral_rnDeriv_of_ac, InformationTheory.convexOn_klFun, InformationTheory.continuous_klFun, Continuous.continuousWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
refine : Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν

Premises used: MeasureTheory.mul_le_integral_rnDeriv_of_ac, InformationTheory.convexOn_klFun, InformationTheory.continuous_klFun, Continuous.continuousWithinAt
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int rwa rwa₁ rwa₂ rwa₃ : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
rwa [integrable_klFun_rnDeriv_iff hμν]

Premises used: InformationTheory.integrable_klFun_rnDeriv_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw rw₁ : Eq (α := ℝ) (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal

Tactic:
rw [toReal_klDiv_eq_integral_klFun hμν]

Premises used: InformationTheory.toReal_klDiv_eq_integral_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
calc : ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
calc₁ : ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ (klDiv μ ν).toReal

Tactic:
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μν]

Premises used: Set.univ, MeasureTheory.Measure.real, HDiv.hDiv, ENNReal.toReal, InformationTheory.klFun, InformationTheory.klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
pos : ∀ (hμ : μ = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
neg : ∀ (hμ : ¬μ = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : μ = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
simp [hμ, measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
pos : ∀ (hν : ν = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
neg : ∀ (hν : ¬ν = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
by_cases hν : ν = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
absurd ?_ hμ

Premises used: absurd
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
pos : μ = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

Tactic:
refine absurd ?_ hμ

Premises used: absurd
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

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

Premises used: LE.le.trans, le_of_eq, InformationTheory.mul_klFun_le_toReal_klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal

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

Premises used: LE.le.trans, le_of_eq, InformationTheory.mul_klFun_le_toReal_klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
hb : ν.real univ ≠ 0
⊢ ν.real univ * (μ.real univ / ν.real univ) = μ.real univ

Tactic:
rw [mul_div_cancel₀]

Premises used: mul_div_cancel₀
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ ν.real univ ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hν, measureReal_def]

Premises used: MeasureTheory.measureReal_def, ENNReal.toReal_eq_zero_iff
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ ν.real univ * (μ.real univ / ν.real univ) = μ.real univ

Tactic:
have : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ := by
    rw [mul_div_cancel₀]; simp [ENNReal.toReal_eq_zero_iff, hν, measureReal_def]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
neg₁ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
      ν.real univ * (μ.real univ / ν.real univ)
neg₂ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
      ν.real univ * (μ.real univ / ν.real univ)
neg₃ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ -
      ν.real univ * (μ.real univ / ν.real univ)
neg₄ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ) * log (μ.real univ / ν.real univ) + ν.real univ -
      ν.real univ * (μ.real univ / ν.real univ)
neg₅ neg₆ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)

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

Premises used: mul_sub, mul_assoc, mul_add, InformationTheory.klFun, mul_one
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
pos :
  ∀ (hμν : μ ≪ ν),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
neg :
  ∀ (hμν : ¬μ ≪ ν),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
by_cases hμν : μ ≪ ν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : ¬μ ≪ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
simp [hμν]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
pos :
  ∀ (h_int : Integrable (llr μ ν) μ),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
neg :
  ∀ (h_int : ¬Integrable (llr μ ν) μ),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
by_cases h_int : Integrable (llr μ ν) μ

Premises used: MeasureTheory.Integrable, MeasureTheory.llr
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
simp [h_int]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
pos :
  ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
    ENNReal.ofReal (klDiv μ ν).toReal
pos₁ : klDiv μ ν ≠ ∞
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν

Tactic:
rw [← ENNReal.ofReal_toReal (a := klDiv μ ν)]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
    ENNReal.ofReal (klDiv μ ν).toReal

Tactic:
ENNReal.ofReal_le_ofReal (mul_log_le_toReal_klDiv hμν h_int)

Premises used: ENNReal.ofReal_le_ofReal, InformationTheory.mul_log_le_toReal_klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
    ENNReal.ofReal (klDiv μ ν).toReal

Tactic:
exact ENNReal.ofReal_le_ofReal (mul_log_le_toReal_klDiv hμν h_int)

Premises used: ENNReal.ofReal_le_ofReal, InformationTheory.mul_log_le_toReal_klDiv