awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
Tactic: have : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ := by
    rw [mul_div_cancel₀]; simp [ENNReal.toReal_eq_zero_iff, hν, measureReal_def]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg₁ : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
    ν.real univ * (μ.real univ / ν.real univ)
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
neg₁ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
      ν.real univ * (μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg₂ : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
    ν.real univ * (μ.real univ / ν.real univ)
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
neg₁ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
      ν.real univ * (μ.real univ / ν.real univ)
neg₂ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
      ν.real univ * (μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg₃ : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ -
    ν.real univ * (μ.real univ / ν.real univ)
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
neg₁ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
      ν.real univ * (μ.real univ / ν.real univ)
neg₂ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
      ν.real univ * (μ.real univ / ν.real univ)
neg₃ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ -
      ν.real univ * (μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg₄ : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * (μ.real univ / ν.real univ) * log (μ.real univ / ν.real univ) + ν.real univ -
    ν.real univ * (μ.real univ / ν.real univ)
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
neg :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1 - μ.real univ / ν.real univ)
neg₁ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ) + 1) -
      ν.real univ * (μ.real univ / ν.real univ)
neg₂ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ * 1 -
      ν.real univ * (μ.real univ / ν.real univ)
neg₃ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ * log (μ.real univ / ν.real univ)) + ν.real univ -
      ν.real univ * (μ.real univ / ν.real univ)
neg₄ :
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * (μ.real univ / ν.real univ) * log (μ.real univ / ν.real univ) + ν.real univ -
      ν.real univ * (μ.real univ / ν.real univ)
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
    ν.real univ * klFun (μ.real univ / ν.real univ)
have neg₅ : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ
Tactic: rw [klFun, mul_sub, mul_add, mul_one, ← mul_assoc, this]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have pos : ∀ (hμν : μ ≪ ν), ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
Tactic: by_cases hμν : μ ≪ ν
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
pos :
  ∀ (hμν : μ ≪ ν),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have neg : ∀ (hμν : ¬μ ≪ ν), ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
Tactic: by_cases hμν : μ ≪ ν
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have pos : ∀ (h_int : Integrable (llr μ ν) μ),
  ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
Tactic: by_cases h_int : Integrable (llr μ ν) μ
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
pos :
  ∀ (h_int : Integrable (llr μ ν) μ),
    ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ),
  ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
Tactic: by_cases h_int : Integrable (llr μ ν) μ
-- 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 μ ν) μ
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have pos : ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
  ENNReal.ofReal (klDiv μ ν).toReal
Tactic: rw [← ENNReal.ofReal_toReal (a := 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 μ ν) μ
pos :
  ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤
    ENNReal.ofReal (klDiv μ ν).toReal
⊢ ENNReal.ofReal (μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ) ≤ klDiv μ ν
have pos₁ : klDiv μ ν ≠ ∞
Tactic: rw [← ENNReal.ofReal_toReal (a := 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 μ ν) μ
⊢ klDiv μ ν ≠ ∞
have pos : μ ≪ ν ∧ Integrable (llr μ ν) μ
Tactic: rw [klDiv_ne_top_iff]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ klDiv μ ν = 0 ↔ μ = ν
have refine : ∀ (h : klDiv μ ν = 0), μ = ν
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h ▸ klDiv_self _⟩
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
⊢ μ = ν
have h_ne : klDiv μ ν ≠ ∞
Tactic: have h_ne : klDiv μ ν ≠ ⊤ := by simp [h]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : klDiv μ ν ≠ ∞
⊢ μ = ν
have h_ne₁ : μ ≪ ν ∧ Integrable (llr μ ν) μ
Tactic: rw [klDiv_ne_top_iff] at h_ne
Cleared hypotheses: h_ne
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : klDiv μ ν = 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν
have h₁ : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
Tactic: rw [klDiv_eq_lintegral_klFun, if_pos h_ne.1, lintegral_eq_zero_iff (by fun_prop)] at h
Cleared hypotheses: h, h_ne
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ = ν
have refine : μ.rnDeriv ν =ᶠ[ae ν] 1
Tactic: refine (Measure.rnDeriv_eq_one_iff_eq h_ne.1).mp ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ μ.rnDeriv ν =ᶠ[ae ν] 1
have h₁ : ∀ (x : α) (hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x), μ.rnDeriv ν x = 1 x
Tactic: filter_upwards [h] with x hx
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) = 0 x
⊢ μ.rnDeriv ν x = 1 x
have hx₁ : klFun (μ.rnDeriv ν x).toReal ≤ 0
Tactic: simp only [Pi.zero_apply, ENNReal.ofReal_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
⊢ μ.rnDeriv ν x = 1 x
have hx' : klFun (μ.rnDeriv ν x).toReal = 0
Tactic: have hx' : klFun (μ.rnDeriv ν x).toReal = 0 := le_antisymm hx (klFun_nonneg ENNReal.toReal_nonneg)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
⊢ μ.rnDeriv ν x = 1 x
have h₁ : ∀ (hx' : (μ.rnDeriv ν x).toReal = 1), μ.rnDeriv ν x = 1 x
Tactic: rwa [klFun_eq_zero_iff ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : (ae ν).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal)) 0
h_ne : μ ≪ ν ∧ Integrable (llr μ ν) μ
x : α
hx : klFun (μ.rnDeriv ν x).toReal ≤ 0
hx' : klFun (μ.rnDeriv ν x).toReal = 0
h₁ : ∀ (hx' : (μ.rnDeriv ν x).toReal = 1), μ.rnDeriv ν x = 1 x
⊢ μ.rnDeriv ν x = 1 x
have h₂ : ∀ (hx' : μ.rnDeriv ν x = 1), μ.rnDeriv ν x = 1 x
Tactic: rwa [klFun_eq_zero_iff ENNReal.toReal_nonneg, ENNReal.toReal_eq_one_iff] at hx'
Cleared hypotheses: hx'
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ Integrable (llr μ ν) μ
have hμν_ac : μ ≪ ν
Tactic: have ⟨hμν_ac, hκη_ac⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
⊢ Integrable (llr μ ν) μ
have hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
Tactic: have ⟨hμν_ac, hκη_ac⟩ := Measure.absolutelyContinuous_compProd_iff.mp h_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ
have h_int₁ : Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
Tactic: rw [← integrable_rnDeriv_mul_log_iff h_ac] at h_int
Cleared hypotheses: h_int, hμν_ac, hκη_ac
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (hypothesis)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (ε := ℝ) (fun (a : 𝓧 × 𝓨) ↦ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) a).toReal) (ν ⊗ₘ η)
hμν_ac : μ ≪ ν
hκη_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ Integrable (llr μ ν) μ
have h_int₁ : Integrable (ε := ℝ) (fun (a : 𝓧) ↦ ((∂μ/∂ν) a).toReal * log ((∂μ/∂ν) a).toReal) ν
Tactic: replace h_int := convexOn_mul_log.integrable_apply_rnDeriv_of_integrable_compProd
    continuous_mul_log.stronglyMeasurable continuous_mul_log.continuousWithinAt h_int hκη_ac
Cleared hypotheses: h_int
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ ∀ᵐ (p : 𝓧 × 𝓨) ∂ν ⊗ₘ η,
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
      ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have h : ∀ (p : 𝓧 × 𝓨) (hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p),
  ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: filter_upwards [rnDeriv_compProd h_ac ν] with p hp
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * log ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal =
    ((∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have h : ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: simp_rw [hp, ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have pos : ∀ (h_zero1 : ((∂μ/∂ν) p.1).toReal = 0),
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: by_cases h_zero1 : ((∂μ/∂ν) p.1).toReal = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
pos :
  ∀ (h_zero1 : ((∂μ/∂ν) p.1).toReal = 0),
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
      ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal *
        (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have neg : ∀ (h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0),
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: by_cases h_zero1 : ((∂μ/∂ν) p.1).toReal = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.ChainRule (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
κ η : Kernel 𝓧 𝓨
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
inst_2 : IsMarkovKernel κ
inst_3 : IsMarkovKernel η
h_ac : μ ⊗ₘ κ ≪ μ ⊗ₘ η
p : 𝓧 × 𝓨
hp : (∂μ ⊗ₘ κ/∂ν ⊗ₘ η) p = (∂μ/∂ν) p.1 * (∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p
h_zero1 : ¬((∂μ/∂ν) p.1).toReal = 0
⊢ ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
have pos : ∀ (h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0),
  ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * log (((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal) =
    ((∂μ/∂ν) p.1).toReal * ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal * (log ((∂μ/∂ν) p.1).toReal + log ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal)
Tactic: by_cases h_zero2 : ((∂μ ⊗ₘ κ/∂μ ⊗ₘ η) p).toReal = 0