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_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h_int : Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
simp [toReal_klDiv h h_int, h_eq, measureReal_def]

Premises used: InformationTheory.toReal_klDiv, MeasureTheory.measureReal_def
-- 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∞)
h_int : ¬Integrable (llr μ ν) μ
neg : ENNReal.toReal ∞ = ∫ (a : α), llr μ ν a ∂μ
neg₁ : ENNReal.toReal ∞ = 0
neg₂ neg₃ : Eq (α := ℝ) 0 0
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ

Tactic:
rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]

Premises used: MeasureTheory.integral_undef, InformationTheory.klDiv_of_not_integrable, ENNReal.toReal_top
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
pos : ∀ (h_int : Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

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 μ ν) μ
pos : LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [klDiv_eq_integral_klFun, if_pos ⟨h, h_int⟩, ENNReal.toReal_ofReal]

Premises used: if_pos, InformationTheory.klDiv_eq_integral_klFun, 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 μ ν) μ
⊢ LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
integral_nonneg fun _ ↦ 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 _ ↦ 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 μ ν) μ
neg : (klDiv μ ν).toReal = 0
neg₁ : ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [integral_undef]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
neg : ENNReal.toReal ∞ = 0
neg₁ neg₂ : Eq (α := ℝ) 0 0
⊢ (klDiv μ ν).toReal = 0

Tactic:
rw [klDiv_of_not_integrable h_int, ENNReal.toReal_top]

Premises used: InformationTheory.klDiv_of_not_integrable, ENNReal.toReal_top
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_int neg neg₁ neg₂ neg₃ : ¬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 μ ν) μ
c : ℝ≥0
pos :
  ∀ (hc : c = 0),
    (klDiv (c • μ) ν).toReal =
      (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
neg :
  ∀ (hc : ¬c = 0),
    (klDiv (c • μ) ν).toReal =
      (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

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

Tactic:
simp [hc, 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 μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ c ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)

Tactic:
have h_llr := llr_smul_nnreal_left hμν c (by simpa)
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg :
  ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
neg₁ : Integrable (llr (c • μ) ν) (c • μ)
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

Tactic:
rw [toReal_klDiv hμν h_int, toReal_klDiv (hμν.smul_left c)]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, InformationTheory.toReal_klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ Integrable (llr (c • μ) ν) (c • μ)

Tactic:
Integrable.smul_measure_nnreal ?_

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg : Integrable (llr (c • μ) ν) μ
⊢ Integrable (llr (c • μ) ν) (c • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ
⊢ Integrable (llr (c • μ) ν) μ

Tactic:
rw [integrable_congr h_llr]

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg :
  HSMul.hSMul (β := ℝ) c (∫ (a : α), llr (c • μ) ν a ∂μ) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

Tactic:
simp only [integral_smul_nnreal_measure, measureReal_nnreal_smul_apply]

Premises used: MeasureTheory.integral_smul_nnreal_measure, MeasureTheory.measureReal_nnreal_smul_apply
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg :
  c • HAdd.hAdd (α := ℝ) (∫ (a : α), llr μ ν a ∂μ) (∫ (a : α), log (↑c : ℝ) ∂μ) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ HSMul.hSMul (β := ℝ) c (∫ (a : α), llr (c • μ) ν a ∂μ) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

Tactic:
rw [integral_congr_ae h_llr, integral_add h_int (integrable_const _)]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.integrable_const, MeasureTheory.integral_add
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ ∀ (a : ℝ), c • a = (↑c : ℝ) * a

Tactic:
have h_smul (a : ℝ) : c • a = c * a := rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
h_smul : ∀ (a : ℝ), c • a = (↑c : ℝ) * a
neg :
  (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + μ.real univ * log (↑c : ℝ)) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ c • HAdd.hAdd (α := ℝ) (∫ (a : α), llr μ ν a ∂μ) (∫ (a : α), log (↑c : ℝ) ∂μ) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

Tactic:
simp [h_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
h_smul : ∀ (a : ℝ), c • a = (↑c : ℝ) * a
⊢ (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + μ.real univ * log (↑c : ℝ)) + ν.real univ - (↑c : ℝ) * μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ

Tactic:
ring
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
pos : ∀ (hc : c = 0), (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
neg : ∀ (hc : ¬c = 0), (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal

Tactic:
by_cases hc : c = 0
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c = 0
pos : (klDiv μ 0).toReal = 0
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal

Tactic:
simp only [hc, zero_smul, NNReal.coe_zero, inv_zero, klDiv_zero_left, zero_mul]

Premises used: inv_zero, MulZeroClass.zero_mul, NNReal.coe_zero, InformationTheory.klDiv_zero_left, zero_smul
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c = 0
pos :
  ∀ [IsFiniteMeasure.{u_1} (α := α) (m0 := mα) 0] (hμν : 0 ≪ ν) (h_int : @Integrable _ _ _ _ mα (llr 0 ν) 0),
    (klDiv.{u_1} (α := α) (mα := mα) 0 0).toReal = 0
pos₁ : ∀ (hμ : NeZero μ), (klDiv μ 0).toReal = 0
⊢ (klDiv μ 0).toReal = 0

Tactic:
rcases eq_zero_or_neZero μ with rfl | hμ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
ν : Measure α
inst : IsFiniteMeasure ν
c : ℝ≥0
hc : c = 0
inst_1 : IsFiniteMeasure.{u_1} (α := α) (m0 := mα) 0
hμν : 0 ≪ ν
h_int : @Integrable _ _ _ _ mα (llr 0 ν) 0
⊢ (klDiv.{u_1} (α := α) (mα := mα) 0 0).toReal = 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 μ ν) μ
c : ℝ≥0
hc : c = 0
hμ : NeZero μ
⊢ (klDiv μ 0).toReal = 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 μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ c⁻¹ ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)

Tactic:
have h_llr_left := llr_smul_nnreal_left hμν c⁻¹ (by simpa)
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
⊢ c ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
⊢ llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)

Tactic:
have h_llr_right := llr_smul_nnreal_right hμν c (by simpa)
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
neg :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
neg₁ : c⁻¹ • μ ≪ ν
neg₂ : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
neg₃ : μ ≪ c • ν
neg₄ : Integrable (llr μ (c • ν)) μ
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal

Tactic:
rw [toReal_klDiv, toReal_klDiv]

Premises used: InformationTheory.toReal_klDiv
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ c⁻¹ • μ ≪ ν

Tactic:
hμν.smul_left _

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ c⁻¹ • μ ≪ ν

Tactic:
exact hμν.smul_left _

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
Integrable.smul_measure_nnreal ?_

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
neg : Integrable (llr (c⁻¹ • μ) ν) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
refine Integrable.smul_measure_nnreal ?_

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) μ

Tactic:
rw [integrable_congr h_llr_left]

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
funProp : ‖log (↑c⁻¹ : ℝ)‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)) μ

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ μ ≪ c • ν

Tactic:
exact hμν.smul_right (by simpa)

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_right
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ
⊢ Integrable (llr μ (c • ν)) μ

Tactic:
rw [integrable_congr h_llr_right]

Premises used: MeasureTheory.integrable_congr
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
⊢ ∀ (c : ℝ≥0) (a : ℝ), c • a = (↑c : ℝ) * a

Tactic:
have h_smul (c : ℝ≥0) (a : ℝ) : c • a = c * a := rfl
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = (↑c : ℝ) * a
neg :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)

Tactic:
simp only [measureReal_nnreal_smul_apply, integral_smul_nnreal_measure, h_smul, NNReal.coe_inv]

Premises used: MeasureTheory.integral_smul_nnreal_measure, NNReal.coe_inv, MeasureTheory.measureReal_nnreal_smul_apply
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = (↑c : ℝ) * a
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa