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 μ ν) μ
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∞) ≠ ∞

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_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
⊢ llr ((↑c : ℝ≥0∞)⁻¹ • μ) ν =ᶠ[ae μ] llr μ ((↑c : ℝ≥0∞) • ν)

Tactic:
have h_llr_smul_inv := llr_smul_inv_left_eq_smul_right hμν c (by simpa) (by 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_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
h_llr_smul_inv : llr ((↑c : ℝ≥0∞)⁻¹ • μ) ν =ᶠ[ae μ] llr μ ((↑c : ℝ≥0∞) • ν)
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)

Tactic:
simp only [← ENNReal.coe_inv hc, Measure.coe_nnreal_smul] at h_llr_smul_inv

Premises used: ENNReal.coe_inv, MeasureTheory.Measure.coe_nnreal_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_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
h_llr_smul_inv : llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (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⁻¹ : ℝ)
h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = (↑c : ℝ) * a
h_llr_smul_inv : llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)
neg :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
neg₁ :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ + ν.real univ) - (↑c : ℝ) * ((↑c : ℝ)⁻¹ * μ.real univ)
neg₂ :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ) + (↑c : ℝ) * ν.real univ -
      (↑c : ℝ) * ((↑c : ℝ)⁻¹ * μ.real univ)
neg₃ :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - (↑c : ℝ) * ((↑c : ℝ)⁻¹ * μ.real univ)
neg₄ neg₅ :
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)

Tactic:
rw [integral_congr_ae h_llr_smul_inv, mul_sub, mul_add, mul_inv_cancel_left₀ (by simpa),
    mul_inv_cancel_left₀ (by simpa)]

Premises used: mul_inv_cancel_left₀, mul_sub, MeasureTheory.integral_congr_ae, mul_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
rw :
  (↑c : ℝ) *
      ((↑c⁻¹ : ℝ) * (klDiv μ ν).toReal + (1 - (↑c⁻¹ : ℝ)) * ν.real univ + (↑c⁻¹ : ℝ) * log (↑c⁻¹ : ℝ) * μ.real univ) =
    (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ
⊢ (klDiv μ (c • ν)).toReal = (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ

Tactic:
rw [toReal_klDiv_smul_right_eq_smul_left hμν h_int c, toReal_klDiv_smul_left hμν h_int c⁻¹]

Premises used: Inv.inv, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, InformationTheory.toReal_klDiv_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
simp :
  (↑c : ℝ) *
      ((↑c : ℝ)⁻¹ * (klDiv μ ν).toReal + (1 - (↑c : ℝ)⁻¹) * ν.real univ - (↑c : ℝ)⁻¹ * log (↑c : ℝ) * μ.real univ) =
    (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ
⊢ (↑c : ℝ) *
      ((↑c⁻¹ : ℝ) * (klDiv μ ν).toReal + (1 - (↑c⁻¹ : ℝ)) * ν.real univ + (↑c⁻¹ : ℝ) * log (↑c⁻¹ : ℝ) * μ.real univ) =
    (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ

Tactic:
simp only [NNReal.coe_inv, log_inv, mul_neg, neg_mul, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, NNReal.coe_inv, neg_mul, Real.log_inv, mul_neg
-- 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 : ℝ) *
      ((↑c : ℝ)⁻¹ * (klDiv μ ν).toReal + (1 - (↑c : ℝ)⁻¹) * ν.real univ - (↑c : ℝ)⁻¹ * log (↑c : ℝ) * μ.real univ) =
    (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ

Tactic:
field_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
pos : ∀ (hc : c = 0), (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
neg : ∀ (hc : ¬c = 0), (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
⊢ (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).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
⊢ (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal

Tactic:
simp [hc]
-- 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
neg : c • μ ≪ ν
neg₁ : Integrable (llr (c • μ) ν) (c • μ)
⊢ (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal

Tactic:
rw [toReal_klDiv_smul_right_eq_smul_left, smul_smul, inv_mul_cancel₀ hc, one_smul]

Premises used: smul_smul, one_smul, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, inv_mul_cancel₀
-- 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 • μ ≪ ν

Tactic:
hμν.smul_left c

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
⊢ c • μ ≪ ν

Tactic:
exact hμν.smul_left c

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
⊢ 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
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
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ
⊢ Integrable (llr (c • μ) ν) μ

Tactic:
rw [integrable_congr (llr_smul_nnreal_left hμν c (by simpa))]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_smul_nnreal_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
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 ν
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
have hc' : (c : ℝ≥0∞) ≠ 0 := by simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
rw : μ = (c * c⁻¹) • μ
rw₁ : μ = HSMul.hSMul (α := ℝ≥0) 1 μ
rw₂ rw₃ : μ = μ
⊢ μ = c • c⁻¹ • μ

Tactic:
rw [smul_smul, mul_inv_cancel₀ hc, one_smul]

Premises used: mul_inv_cancel₀, smul_smul, one_smul
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
⊢ μ = c • c⁻¹ • μ

Tactic:
have hμ_smul : μ = c • (c⁻¹ • μ) := by rw [smul_smul, mul_inv_cancel₀ hc, one_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
rw : ν = (c⁻¹ * c) • ν
rw₁ : ν = HSMul.hSMul (α := ℝ≥0) 1 ν
rw₂ rw₃ : ν = ν
⊢ ν = c⁻¹ • c • ν

Tactic:
rw [smul_smul, inv_mul_cancel₀ hc, one_smul]

Premises used: smul_smul, one_smul, inv_mul_cancel₀
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
⊢ ν = c⁻¹ • c • ν

Tactic:
have hν_smul : ν = c⁻¹ • (c • ν) := by rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
pos : ∀ (hμν : μ ≪ ν), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
neg : ∀ (hμν : ¬μ ≪ ν), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
by_cases hμν : μ ≪ ν
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
neg : ¬c⁻¹ • μ ≪ ν
neg₁ : ¬μ ≪ c • ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
rw [klDiv_of_not_ac, klDiv_of_not_ac, ENNReal.mul_top hc']

Premises used: ENNReal.mul_top, InformationTheory.klDiv_of_not_ac
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ ¬c⁻¹ • μ ≪ ν

Tactic:
fun h_contra ↦ hμν ?_

Premises used: Not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
neg : ∀ (h_contra : c⁻¹ • μ ≪ ν), μ ≪ ν
⊢ ¬c⁻¹ • μ ≪ ν

Tactic:
refine fun h_contra ↦ hμν ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : c⁻¹ • μ ≪ ν
neg : c • c⁻¹ • μ ≪ ν
⊢ μ ≪ ν

Tactic:
rw [hμ_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : c⁻¹ • μ ≪ ν
⊢ c • c⁻¹ • μ ≪ ν

Tactic:
h_contra.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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : c⁻¹ • μ ≪ ν
⊢ c • c⁻¹ • μ ≪ ν

Tactic:
exact h_contra.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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ ¬μ ≪ c • ν

Tactic:
fun h_contra ↦ hμν ?_

Premises used: Not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
neg : ∀ (h_contra : μ ≪ c • ν), μ ≪ ν
⊢ ¬μ ≪ c • ν

Tactic:
refine fun h_contra ↦ hμν ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
neg : μ ≪ c⁻¹ • c • ν
⊢ μ ≪ ν

Tactic:
rw [hν_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ (↑c⁻¹ : ℝ≥0∞) ≠ 0

Tactic:
simpa
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ c⁻¹ • c • ν

Tactic:
exact h_contra.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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
⊢ μ ≪ (↑c : ℝ≥0∞) • ν

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

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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
neg : ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
neg₁ : ¬Integrable (llr μ (c • ν)) μ
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
rw [klDiv_of_not_integrable, klDiv_of_not_integrable, ENNReal.mul_top hc']

Premises used: InformationTheory.klDiv_of_not_integrable, ENNReal.mul_top
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
fun h_contra ↦ h_int ?_

Premises used: Not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
neg : ∀ (h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)), Integrable (llr μ ν) μ
⊢ ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
refine fun h_contra ↦ h_int ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
neg : Integrable (llr (c • c⁻¹ • μ) ν) (c • c⁻¹ • μ)
⊢ Integrable (llr μ ν) μ

Tactic:
rw [hμ_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
neg : Integrable (llr (c • c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr (c⁻¹ • μ) ν x + log (↑c : ℝ)) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c⁻¹ • μ)

Tactic:
rw [integrable_congr (llr_smul_nnreal_left (hμν.smul_left _) c hc)]

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, MeasureTheory.integrable_congr, MeasureTheory.llr_smul_nnreal_left
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr (c⁻¹ • μ) ν x + log (↑c : ℝ)) (c⁻¹ • μ)

Tactic:
fun_prop
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (llr μ (c • ν)) μ

Tactic:
fun h_contra ↦ h_int ?_

Premises used: Not
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
neg : ∀ (h_contra : Integrable (llr μ (c • ν)) μ), Integrable (llr μ ν) μ
⊢ ¬Integrable (llr μ (c • ν)) μ

Tactic:
refine fun h_contra ↦ h_int ?_
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
neg : Integrable (llr μ (c⁻¹ • c • ν)) μ
⊢ Integrable (llr μ ν) μ

Tactic:
rw [hν_smul]
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ IsFiniteMeasure (c • ν)

Tactic:
infer_instance
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)

Tactic:
have : IsFiniteMeasure ((c : ℝ≥0∞) • ν) := by
        simp only [Measure.coe_nnreal_smul]
        infer_instance