awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: rw [klDiv_of_not_integrable h_int]
-- 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_int₁ : ¬(Integrable (llr μ ν) μ ∧ Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ))
Tactic: rw [integrable_llr_compProd_iff h_ac] at h_int
Cleared hypotheses: h_int
-- 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 (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ))
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_int₁ : ¬Integrable (llr μ ν) μ ∨ ¬Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: simp only [not_and_or] at h_int
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr μ ν) μ ∨ ¬Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg : ∀ (h : ¬Integrable (llr μ ν) μ), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: cases h_int with
    | inl h => simp [h]
    | inr h => simp [h]
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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : ¬Integrable (llr μ ν) μ ∨ ¬Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
neg : ∀ (h : ¬Integrable (llr μ ν) μ), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
⊢ ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have neg₁ : ∀ (h : ¬Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)), ∞ = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
Tactic: cases h_int with
    | inl h => simp [h]
    | inr h => simp [h]
Cleared hypotheses: h_int
-- 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 (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
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_μν : μ ≪ ν
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
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_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_int_μν : Integrable (llr μ ν) μ
Tactic: have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp h_int
-- 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_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
Tactic: have ⟨h_int_μν, h_int_κη⟩ := (integrable_llr_compProd_iff h_ac).mp 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ klDiv (μ ⊗ₘ κ) (ν ⊗ₘ η) = klDiv μ ν + klDiv (μ ⊗ₘ κ) (μ ⊗ₘ η)
have pos : ENNReal.ofReal
    (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
      ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
  ENNReal.ofReal
    (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
      ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
Tactic: simp_rw [klDiv_of_ac_of_integrable h_ac h_int, klDiv_of_ac_of_integrable h_ac_μν h_int_μν,
    klDiv_of_ac_of_integrable h_ac_κη h_int_κη,
    ← ENNReal.ofReal_add (integral_llr_add_sub_measure_univ_nonneg h_ac_μν h_int_μν)
    (integral_llr_add_sub_measure_univ_nonneg h_ac_κη h_int_κη), measureReal_def,
    Measure.compProd_apply_univ, add_sub_cancel_right]
-- 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
this :
  ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
    HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
⊢ ENNReal.ofReal
      (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
have rw : ENNReal.ofReal
    (HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ) +
        ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
      ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
  ENNReal.ofReal
    (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
      ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
Tactic: rw [this]
-- 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 : μ ⊗ₘ κ ≪ ν ⊗ₘ η
h_int : Integrable (llr (μ ⊗ₘ κ) (ν ⊗ₘ η)) (μ ⊗ₘ κ)
h_ac_μν : μ ≪ ν
h_ac_κη : μ ⊗ₘ κ ≪ μ ⊗ₘ η
h_int_μν : Integrable (llr μ ν) μ
h_int_κη : Integrable (llr (μ ⊗ₘ κ) (μ ⊗ₘ η)) (μ ⊗ₘ κ)
⊢ ENNReal.ofReal
      (∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) x ∂μ ⊗ₘ κ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
        ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ)) =
    ENNReal.ofReal
      (∫ (x : 𝓧), llr μ ν x ∂μ + ENNReal.toReal ((ν : (a : Set 𝓧) → ℝ≥0∞) univ) -
          ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) univ) +
        ∫ (x : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) x ∂μ ⊗ₘ κ)
have pos : ∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
  HAdd.hAdd (α := ℝ) (∫ (a : 𝓧), llr μ ν a ∂μ) (∫ (p : 𝓧 × 𝓨), llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂μ ⊗ₘ κ)
Tactic: suffices ∫ p, llr (μ ⊗ₘ κ) (ν ⊗ₘ η) p ∂μ ⊗ₘ κ =
      ∫ a, llr μ ν a ∂μ + ∫ p, llr (μ ⊗ₘ κ) (μ ⊗ₘ η) p ∂(μ ⊗ₘ κ) by rw [this]; ring_nf
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ x * log x + 1 - x
have funProp : ∀ (x : ℝ), x ≠ 0
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt klFun (log x) x
have h : log x = log x + 1 + 0 - 1
Tactic: convert! ((hasDerivAt_mul_log hx).add (hasDerivAt_const x 1)).sub (hasDerivAt_id x) using 1
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ deriv klFun = log
have h : ∀ (x : ℝ), deriv klFun x = log x
Tactic: ext x
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
⊢ deriv klFun x = log x
have pos : ∀ (h0 : x = 0), deriv klFun x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), deriv klFun x = log x
⊢ deriv klFun x = log x
have neg : ∀ (h0 : ¬x = 0), deriv klFun x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
h0 : x = 0
⊢ deriv klFun x = log x
have pos : deriv klFun 0 = 0
Tactic: simp only [h0, log_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ ¬DifferentiableWithinAt ℝ klFun (Ioi 0) 0
have refine : Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot
Tactic: refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi _ ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Ioi 0)) atBot
have rw : Tendsto log (nhdsWithin 0 (Ioi 0)) atBot
Tactic: rw [deriv_klFun]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ ¬DifferentiableWithinAt ℝ klFun (Iio 0) 0
have refine : Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot
Tactic: refine not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio _ ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ Tendsto (deriv klFun) (nhdsWithin 0 (Iio 0)) atBot
have rw : Tendsto log (nhdsWithin 0 (Iio 0)) atBot
Tactic: rw [deriv_klFun]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
⊢ derivWithin klFun (Ioi x) x = log x
have pos : ∀ (h0 : x = 0), derivWithin klFun (Ioi x) x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), derivWithin klFun (Ioi x) x = log x
⊢ derivWithin klFun (Ioi x) x = log x
have neg : ∀ (h0 : ¬x = 0), derivWithin klFun (Ioi x) x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Ioi x) x = log x
have pos : derivWithin klFun (Ioi 0) 0 = 0
Tactic: simp only [h0, log_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
⊢ derivWithin klFun (Iio x) x = log x
have pos : ∀ (h0 : x = 0), derivWithin klFun (Iio x) x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
pos : ∀ (h0 : x = 0), derivWithin klFun (Iio x) x = log x
⊢ derivWithin klFun (Iio x) x = log x
have neg : ∀ (h0 : ¬x = 0), derivWithin klFun (Iio x) x = log x
Tactic: by_cases h0 : x = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
h0 : x = 0
⊢ derivWithin klFun (Iio x) x = log x
have pos : derivWithin klFun (Iio 0) 0 = 0
Tactic: simp only [h0, log_zero]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ derivWithin klFun (Ioi x) x) atTop atTop
have simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x) atTop atTop
Tactic: simp only [rightDeriv_klFun]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ klFun x = 0 ↔ x = 1
have refine : ∀ (h : klFun x = 0), x = 1
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [klFun_apply, h]⟩
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
⊢ Eq (α := (x : ℝ) → ℝ) (fun (x : ℝ) ↦ x * log x + 1 - x) fun (x : ℝ) ↦ x * (log x - 1) + 1
have h : ∀ (x : ℝ), x * log x + 1 - x = x * (log x - 1) + 1
Tactic: ext
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (hypothesis)
Goal:
⊢ Tendsto klFun atTop atTop
have this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
Tactic: have : klFun = (fun x ↦ x * (log x - 1) + 1) := by unfold klFun; ext; ring
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto klFun atTop atTop
have rw : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1) + 1) atTop atTop
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1) + 1) atTop atTop
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1)) atTop atTop
Tactic: refine Tendsto.atTop_add ?_ tendsto_const_nhds
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
this : klFun = fun (x : ℝ) ↦ x * (log x - 1) + 1
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x * (log x - 1)) atTop atTop
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ log x - 1) atTop atTop
Tactic: refine tendsto_id.atTop_mul_atTop₀ ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ
have h : ∀ (x : α),
  klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
Tactic: convert! this using 3 with x
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
x : α
⊢ klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
have h : (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal =
  (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
Tactic: rw [klFun, add_sub_assoc]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
this :
  Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
x : α
h :
  (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal =
    (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
⊢ klFun (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
have h₁ : (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal) =
  (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal)
Tactic: rw [klFun, add_sub_assoc]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν ↔ Integrable (llr μ ν) μ
have suffices : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
    ν ↔
  Integrable (llr μ ν) μ
Tactic: suffices Integrable (fun x ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal
      + (1 - (μ.rnDeriv ν x).toReal)) ν ↔ Integrable (llr μ ν) μ by
    convert! this using 3 with x
    rw [klFun, add_sub_assoc]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + (1 - (μ.rnDeriv ν x).toReal))
      ν ↔
    Integrable (llr μ ν) μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ 1 - (μ.rnDeriv ν x).toReal) ν
Tactic: rw [integrable_add_iff_integrable_left', integrable_rnDeriv_mul_log_iff hμν]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ 1 - (μ.rnDeriv ν x).toReal) ν
have funProp : enorm (E := ℝ) 1 ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have rw : ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
  ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
Tactic: rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw :
  ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have hf : Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν
Tactic: rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw :
  ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have hg : Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν
Tactic: rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw :
  ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν
hg : Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have hf₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν
Tactic: rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
rw :
  ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
hf : Integrable (ε := ℝ) (fun (a : α) ↦ (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal) ν
hg : Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν
hf₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν
⊢ ∫ (x : α), (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1 - (μ.rnDeriv ν x).toReal ∂ν =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have hg₁ : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal) ν
Tactic: rw [integral_sub, integral_add, integral_const, Measure.integral_toReal_rnDeriv hμν, smul_eq_mul,
    mul_one]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ ∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν + ν.real univ - μ.real univ =
    ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
have e_a : Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (x : α), llr μ ν x ∂μ)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ 1) ν
have funProp : enorm (E := ℝ) 1 ≠ ⊤
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.KLFun (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal + 1) ν
have hf : Integrable (ε := ℝ) (fun (x : α) ↦ (μ.rnDeriv ν x).toReal * log (μ.rnDeriv ν x).toReal) ν
Tactic: refine Integrable.add ?_ (integrable_const _)