awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞

Tactic:
exact if_neg (not_and_of_not_left _ h)

Premises used: not_and_of_not_left, if_neg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
rw :
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞
⊢ klDiv μ ν = ∞

Tactic:
rw [klDiv_def]

Premises used: InformationTheory.klDiv_def
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞

Tactic:
if_neg (not_and_of_not_right _ h)

Premises used: not_and_of_not_right, if_neg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    ∞

Tactic:
exact if_neg (not_and_of_not_right _ h)

Premises used: not_and_of_not_right, if_neg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ llr μ μ =ᶠ[ae μ] 0

Tactic:
have h := llr_self μ
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
rw : ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0
hc : μ ≪ μ ∧ Integrable (llr μ μ) μ
⊢ klDiv μ μ = 0

Tactic:
rw [klDiv_def, if_pos]

Premises used: InformationTheory.klDiv_def, if_pos
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ ENNReal.ofReal (∫ (x : α), llr μ μ x ∂μ + μ.real univ - μ.real univ) = 0

Tactic:
simp [integral_congr_ae h]

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
hc : μ ≪ μ ∧ Integrable (ε := ℝ) 0 μ
⊢ μ ≪ μ ∧ Integrable (llr μ μ) μ

Tactic:
rw [integrable_congr h]

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable (ε := ℝ) 0 μ

Tactic:
⟨Measure.AbsolutelyContinuous.rfl, integrable_zero _ _ μ⟩

Premises used: MeasureTheory.integrable_zero, And.intro, MeasureTheory.Measure.AbsolutelyContinuous.rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h : llr μ μ =ᶠ[ae μ] 0
⊢ μ ≪ μ ∧ Integrable (ε := ℝ) 0 μ

Tactic:
exact ⟨Measure.AbsolutelyContinuous.rfl, integrable_zero _ _ μ⟩
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst : IsFiniteMeasure ν
⊢ klDiv 0 ν =
    ENNReal.ofReal
      ((@integral _ _ _ _ mα 0 fun (x : α) ↦ llr 0 ν x) + ν.real univ - Measure.real.{u_1} (α := α) (m := mα) 0 univ)

Tactic:
klDiv_of_ac_of_integrable (Measure.AbsolutelyContinuous.zero _) integrable_zero_measure

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.zero, InformationTheory.klDiv_of_ac_of_integrable, MeasureTheory.integrable_zero_measure
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst : IsFiniteMeasure ν
h :
  (ν : (a : Set α) → ℝ≥0∞) univ =
    ENNReal.ofReal
      ((@integral _ _ _ _ mα 0 fun (x : α) ↦ llr 0 ν x) + ν.real univ - Measure.real.{u_1} (α := α) (m := mα) 0 univ)
⊢ klDiv 0 ν = (ν : (a : Set α) → ℝ≥0∞) univ

Tactic:
convert! klDiv_of_ac_of_integrable (Measure.AbsolutelyContinuous.zero _) integrable_zero_measure

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.zero, InformationTheory.klDiv_of_ac_of_integrable, MeasureTheory.integrable_zero_measure
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst : IsFiniteMeasure ν
⊢ (ν : (a : Set α) → ℝ≥0∞) univ =
    ENNReal.ofReal
      ((@integral _ _ _ _ mα 0 fun (x : α) ↦ llr 0 ν x) + ν.real univ - Measure.real.{u_1} (α := α) (m := mα) 0 univ)

Tactic:
simp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : NeZero μ
⊢ klDiv μ 0 = ∞

Tactic:
klDiv_of_not_ac (Measure.absolutelyContinuous_zero_iff.mp.mt (NeZero.ne _))

Premises used: Function.mt, Iff.mp, MeasureTheory.Measure.absolutelyContinuous_zero_iff, InformationTheory.klDiv_of_not_ac, NeZero.ne
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
mp : klDiv μ ν = ∞ → μ ≪ ν → ¬Integrable (llr μ ν) μ
mpr : (μ ≪ ν → ¬Integrable (llr μ ν) μ) → klDiv μ ν = ∞
⊢ klDiv μ ν = ∞ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
constructor
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : klDiv μ ν = ∞
mp : ∀ (h : μ ≪ ν ∧ Integrable (llr μ ν) μ), klDiv μ ν ≠ ∞
⊢ μ ≪ ν → ¬Integrable (llr μ ν) μ

Tactic:
contrapose! h
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
simp [klDiv_of_ac_of_integrable h.1 h.2]

Premises used: InformationTheory.klDiv_of_ac_of_integrable, And.right, And.left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
mpr : ∀ (h : ¬Integrable (llr μ ν) μ), klDiv μ ν = ∞
mpr₁ : ∀ (h : ¬μ ≪ ν), klDiv μ ν = ∞
⊢ klDiv μ ν = ∞

Tactic:
rcases or_not_of_imp h with (h | h)

Premises used: or_not_of_imp
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h_1 : μ ≪ ν → ¬Integrable (llr μ ν) μ
h : ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞

Tactic:
simp [h]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h_1 : μ ≪ ν → ¬Integrable (llr μ ν) μ
h : ¬μ ≪ ν
⊢ klDiv μ ν = ∞

Tactic:
simp [h]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ klDiv μ ν ≠ ∞ ↔ μ ≪ ν ∧ Integrable (llr μ ν) μ

Tactic:
simp [ne_eq, klDiv_eq_top_iff]

Premises used: InformationTheory.klDiv_eq_top_iff, ne_eq
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv μ ν ≠ ∞

Tactic:
klDiv_ne_top_iff.mpr ⟨hμν, h_int⟩

Premises used: Iff.mpr, InformationTheory.klDiv_ne_top_iff, And.intro
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
rw :
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞
⊢ klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
rw [klDiv_def]

Premises used: InformationTheory.klDiv_def
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
rw rw₁ :
  ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
rw [integral_klFun_rnDeriv h.1 h.2]

Premises used: InformationTheory.integral_klFun_rnDeriv, And.right, And.left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
exact if_ctx_congr Iff.rfl (fun h ↦ by rw [integral_klFun_rnDeriv h.1 h.2]) fun _ ↦ rfl

Premises used: if_ctx_congr, Iff.rfl, rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
rw :
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ klDiv μ ν = if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
rw [klDiv_eq_integral_klFun]

Premises used: InformationTheory.klDiv_eq_integral_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
pos :
  ∀ (hμν : μ ≪ ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
neg :
  ∀ (hμν : ¬μ ≪ ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
by_cases hμν : μ ≪ ν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : ¬μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
simp [hμν]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
pos :
  ∀
    (h_int_iff :
      ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
        Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
pos₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
pos₂ : (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
have h_int_iff := lintegral_ofReal_ne_top_iff_integrable
    (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Measurable (β := ℝ) fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, InformationTheory.klFun_nonneg, MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, InformationTheory.klFun_nonneg, MeasureTheory.ae_of_all
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
pos :
  ∀ (h_int : Integrable (llr μ ν) μ),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
neg :
  ∀ (h_int : ¬Integrable (llr μ ν) μ),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
pos :
  ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
simp only [hμν, h_int, and_self, ↓reduceIte]

Premises used: and_self, reduceIte
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
pos : Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
pos₁ : (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal
⊢ ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

Tactic:
rw [ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int pos pos₁ pos₂ pos₃ : 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, InformationTheory.klFun_nonneg, MeasureTheory.ae_of_all, Filter.EventuallyLE
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal

Tactic:
exact ae_of_all _ fun _ ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, InformationTheory.klFun_nonneg, MeasureTheory.ae_of_all
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
    ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν

Tactic:
rw [← not_iff_not, ne_eq, Decidable.not_not] at h_int_iff

Premises used: not_iff_not, ne_eq, Decidable.not_not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
h_int_iff₁ :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
    ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ ¬Integrable (llr μ ν) μ

Tactic:
rw [← not_iff_not, ne_eq, Decidable.not_not] at h_int_iff

Premises used: not_iff_not, ne_eq, Decidable.not_not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
    ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
neg :
  (if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞

Tactic:
symm
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
    ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞) =
    if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞

Tactic:
simp [hμν, h_int, h_int_iff, 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_ac : μ ≪ ν
⊢ klDiv μ ν = ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν

Tactic:
simp [klDiv_eq_lintegral_klFun, h_ac]

Premises used: InformationTheory.klDiv_eq_lintegral_klFun
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw : LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ

Tactic:
rw [← integral_klFun_rnDeriv hμν h_int]

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

Tactic:
integral_nonneg fun x ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: MeasureTheory.integral_nonneg, ENNReal.toReal_nonneg, InformationTheory.klFun_nonneg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
exact integral_nonneg fun x ↦ klFun_nonneg ENNReal.toReal_nonneg

Premises used: MeasureTheory.integral_nonneg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw : 0 ≤ ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ

Tactic:
rw [klDiv_of_ac_of_integrable h h_int, ENNReal.toReal_ofReal]

Premises used: InformationTheory.klDiv_of_ac_of_integrable, ENNReal.toReal_ofReal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ

Tactic:
integral_llr_add_sub_measure_univ_nonneg h h_int

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

Tactic:
exact integral_llr_add_sub_measure_univ_nonneg h h_int

Premises used: InformationTheory.integral_llr_add_sub_measure_univ_nonneg
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
pos : ∀ (h_int : Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

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

Premises used: MeasureTheory.Integrable, MeasureTheory.llr