awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
⊢ c⁻¹ ≠ 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μν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
⊢ llr μ (c⁻¹ • (↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ((↑c : ℝ≥0∞) • ν) x - log (↑c⁻¹ : ℝ)

Tactic:
have h := llr_smul_nnreal_right (hμν.smul_right hc') c⁻¹ (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
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • (↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ((↑c : ℝ≥0∞) • ν) x - log (↑c⁻¹ : ℝ)
⊢ llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)

Tactic:
simp only [Measure.coe_nnreal_smul, NNReal.coe_inv, log_inv, sub_neg_eq_add] at h

Premises used: NNReal.coe_inv, Real.log_inv, sub_neg_eq_add, MeasureTheory.Measure.coe_nnreal_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 • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)
neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)) μ
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ

Tactic:
rw [integrable_congr h]

Premises used: MeasureTheory.integrable_congr
-- 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 • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)
funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ (c • ν) 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
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:
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 μ ν) μ
refine : 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 ν
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 μ ν) μ
⊢ c⁻¹ ≠ 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μν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
rw : 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, Inv.inv
-- 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 μ ν) μ
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
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:
have h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ) := by
    refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_left hμν c⁻¹ (by simpa))]
    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 μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ c ≠ 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μν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
rw : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ
⊢ Integrable (llr μ (c • ν)) μ

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

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_smul_nnreal_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μν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (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 ν
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_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr μ (c • ν)) μ

Tactic:
have h_int_right : Integrable (llr μ (c • ν)) μ := by
    rw [integrable_congr (llr_smul_nnreal_right hμν c (by simpa))]
    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 μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
pos : ENNReal.ofReal ((↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
rw [← ENNReal.ofReal_toReal (klDiv_ne_top hμν_right h_int_right),
    toReal_klDiv_smul_right_eq_smul_left hμν h_int c]

Premises used: ENNReal.ofReal_toReal, InformationTheory.toReal_klDiv_smul_right_eq_smul_left, InformationTheory.klDiv_ne_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 μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
pos : (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv (c⁻¹ • μ) ν).toReal = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
⊢ ENNReal.ofReal ((↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
simp only [NNReal.zero_le_coe, ENNReal.ofReal_mul, ENNReal.ofReal_coe_nnreal]

Premises used: ENNReal.ofReal_mul, ENNReal.ofReal_coe_nnreal, NNReal.zero_le_coe
-- 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_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
pos : klDiv (c⁻¹ • μ) ν ≠ ∞
⊢ (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv (c⁻¹ • μ) ν).toReal = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν

Tactic:
rw [ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- 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_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
⊢ klDiv (c⁻¹ • μ) ν ≠ ∞

Tactic:
klDiv_ne_top (hμν.smul_left _) h_int_left

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, InformationTheory.klDiv_ne_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 μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
h_int_right : Integrable (llr μ (c • ν)) μ
⊢ klDiv (c⁻¹ • μ) ν ≠ ∞

Tactic:
exact klDiv_ne_top (hμν.smul_left _) h_int_left

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.smul_left, InformationTheory.klDiv_ne_top
-- Module: Mathlib.InformationTheory.KullbackLeibler.Basic
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
pos : ∀ (hc : c = 0), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
neg : ∀ (hc : ¬c = 0), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν

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

Tactic:
simp [hc]
-- 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 α
μ_1 ν : Measure α
inst : IsFiniteMeasure μ_1
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
μ : Measure α
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
⊢ ∀ (μ : Measure α), μ = c⁻¹ • c • μ

Tactic:
have hμ_smul (μ : Measure α) : μ = 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
pos : ∀ (hμν : μ ≪ ν), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
neg : ∀ (hμν : ¬μ ≪ ν), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν

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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
neg : ¬c • μ ≪ c • ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν

Tactic:
rw [klDiv_of_not_ac hμν, 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
⊢ ¬c • μ ≪ 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
neg : ∀ (h_contra : c • μ ≪ c • ν), μ ≪ ν
⊢ ¬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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
h_contra : c • μ ≪ c • ν
neg : c⁻¹ • c • μ ≪ c⁻¹ • c • ν
⊢ μ ≪ ν

Tactic:
rw [hμ_smul μ, 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
h_contra : c • μ ≪ c • ν
⊢ c⁻¹ • c • μ ≪ c⁻¹ • c • ν

Tactic:
h_contra.smul _

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
h_contra : c • μ ≪ c • ν
⊢ c⁻¹ • c • μ ≪ c⁻¹ • c • ν

Tactic:
exact h_contra.smul _

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
pos : ∀ (h_int : Integrable (llr μ ν) μ), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * 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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
neg : ¬Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν

Tactic:
rw [klDiv_of_not_integrable h_int, 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (llr (c • μ) (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
neg : ∀ (h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)), Integrable (llr μ ν) μ
⊢ ¬Integrable (llr (c • μ) (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
neg : Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c⁻¹ • c • μ)
⊢ Integrable (llr μ ν) μ

Tactic:
rw [hμ_smul μ, 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
neg : Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ c⁻¹ ≠ 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
neg : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c • μ)

Tactic:
rw [integrable_congr (llr_smul_nnreal_same (hμν.smul c) c⁻¹ (by simpa))]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_smul_nnreal_same, Inv.inv, MeasureTheory.Measure.AbsolutelyContinuous.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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ Integrable (llr (c • μ) (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
pos : ENNReal.ofReal (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv μ ν).toReal
rw : Integrable (llr (c • μ) (c • ν)) (c • μ)
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν

Tactic:
rw [← ENNReal.ofReal_toReal (klDiv_ne_top (hμν.smul c) _),
    ← ENNReal.ofReal_toReal (klDiv_ne_top hμν h_int)]

Premises used: ENNReal.ofReal_toReal, MeasureTheory.Measure.AbsolutelyContinuous.smul, InformationTheory.klDiv_ne_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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
refine : Integrable (llr (c • μ) (c • ν)) μ
⊢ Integrable (llr (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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int rw : Integrable (llr μ ν) μ
⊢ Integrable (llr (c • μ) (c • ν)) μ

Tactic:
rw [integrable_congr (llr_smul_nnreal_same hμν c hc)]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.llr_smul_nnreal_same
-- 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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr μ ν) μ

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 : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv μ ν).toReal

Tactic:
simp [toReal_klDiv_smul_same hμν h_int]

Premises used: InformationTheory.toReal_klDiv_smul_same