awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 : α), 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
have 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
Tactic: simp only [integral_smul_nnreal_measure, measureReal_nnreal_smul_apply]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 : ℝ)
⊢ 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
have 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
Tactic: rw [integral_congr_ae h_llr, integral_add h_int (integrable_const _)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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 : ℝ)
⊢ 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
have h_smul : ∀ (a : ℝ), c • a = (↑c : ℝ) * a
Tactic: have h_smul (a : ℝ) : c • a = c * a := rfl
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • 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
have 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
Tactic: simp [h_smul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have pos : ∀ (hc : c = 0), (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg : ∀ (hc : ¬c = 0), (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 (c⁻¹ • μ) ν).toReal
have pos : (klDiv μ 0).toReal = 0
Tactic: simp only [hc, zero_smul, NNReal.coe_zero, inv_zero, klDiv_zero_left, zero_mul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : c = 0
⊢ (klDiv μ 0).toReal = 0
have 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
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
Cleared hypotheses: μ, inst, hμν, h_int
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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
⊢ (klDiv μ 0).toReal = 0
have pos₁ : ∀ (hμ : NeZero μ), (klDiv μ 0).toReal = 0
Tactic: rcases eq_zero_or_neZero μ with rfl | hμ
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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 (c⁻¹ • μ) ν).toReal
have h_llr_left : llr (c⁻¹ • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)
Tactic: have h_llr_left := llr_smul_nnreal_left hμν c⁻¹ (by simpa)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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⁻¹ : ℝ)
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have h_llr_right : llr μ (c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
Tactic: have h_llr_right := llr_smul_nnreal_right hμν c (by simpa)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 : ℝ)
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg : ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
  (↑c : ℝ) * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
Tactic: rw [toReal_klDiv, toReal_klDiv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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)
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg₁ : c⁻¹ • μ ≪ ν
Tactic: rw [toReal_klDiv, toReal_klDiv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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⁻¹ • μ ≪ ν
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg₂ : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
Tactic: rw [toReal_klDiv, toReal_klDiv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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⁻¹ • μ)
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg₃ : μ ≪ c • ν
Tactic: rw [toReal_klDiv, toReal_klDiv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν
⊢ (klDiv μ (c • ν)).toReal = (↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal
have neg₄ : Integrable (llr μ (c • ν)) μ
Tactic: rw [toReal_klDiv, toReal_klDiv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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⁻¹ • μ)
have neg : Integrable (llr (c⁻¹ • μ) ν) μ
Tactic: refine Integrable.smul_measure_nnreal ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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⁻¹ • μ) ν) μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)) μ
Tactic: rw [integrable_congr h_llr_left]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)) μ
have funProp : ‖log (↑c⁻¹ : ℝ)‖ₑ ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν)) μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ
Tactic: rw [integrable_congr h_llr_right]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ
have funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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 : ℝ)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
have h_smul : ∀ (c : ℝ≥0) (a : ℝ), c • a = (↑c : ℝ) * a
Tactic: have h_smul (c : ℝ≥0) (a : ℝ) : c • a = c * a := rfl
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (c • ν).real univ - μ.real univ =
    (↑c : ℝ) * (∫ (a : α), llr (c⁻¹ • μ) ν a ∂c⁻¹ • μ + ν.real univ - (c⁻¹ • μ).real univ)
have neg : ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
  (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
Tactic: simp only [measureReal_nnreal_smul_apply, integral_smul_nnreal_measure, h_smul, NNReal.coe_inv]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have h_llr_smul_inv : 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)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
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∞) • ν)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have h_llr_smul_inv₁ : llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)
Tactic: simp only [← ENNReal.coe_inv hc, Measure.coe_nnreal_smul] at h_llr_smul_inv
Cleared hypotheses: h_llr_smul_inv
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have neg : ∫ (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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have neg₁ : ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
  (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ + ν.real univ) - (↑c : ℝ) * ((↑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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have neg₂ : ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
  (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr μ (c • ν) a ∂μ) + (↑c : ℝ) * ν.real univ -
    (↑c : ℝ) * ((↑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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have neg₃ : ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - (↑c : ℝ) * ((↑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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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)
⊢ ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
    (↑c : ℝ) * ((↑c : ℝ)⁻¹ * ∫ (a : α), llr (c⁻¹ • μ) ν a ∂μ + ν.real univ - (↑c : ℝ)⁻¹ * μ.real univ)
have neg₄ : ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.real univ =
  ∫ (a : α), llr μ (c • ν) a ∂μ + (↑c : ℝ) * ν.real univ - μ.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)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 = (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ
have rw : (↑c : ℝ) *
    ((↑c⁻¹ : ℝ) * (klDiv μ ν).toReal + (1 - (↑c⁻¹ : ℝ)) * ν.real univ + (↑c⁻¹ : ℝ) * log (↑c⁻¹ : ℝ) * μ.real univ) =
  (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⁻¹]