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 ν
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 • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have pos : ENNReal.ofReal ((↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal) = (↑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]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν)) μ
⊢ ENNReal.ofReal ((↑c : ℝ) * (klDiv (c⁻¹ • μ) ν).toReal) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have pos : (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv (c⁻¹ • μ) ν).toReal = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
Tactic: simp only [NNReal.zero_le_coe, ENNReal.ofReal_mul, ENNReal.ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν)) μ
⊢ (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv (c⁻¹ • μ) ν).toReal = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have pos : klDiv (c⁻¹ • μ) ν ≠ ∞
Tactic: rw [ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have pos : ∀ (hc : c = 0), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
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 ν
c : ℝ≥0
pos : ∀ (hc : c = 0), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have neg : ∀ (hc : ¬c = 0), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have hc' : (↑c : ℝ≥0∞) ≠ 0
Tactic: have hc' : (c : ℝ≥0∞) ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ_1 ν : Measure α
inst : IsFiniteMeasure μ_1
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
μ : Measure α
⊢ μ = c⁻¹ • c • μ
have rw : μ = (c⁻¹ * c) • μ
Tactic: rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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) • μ
⊢ μ = c⁻¹ • c • μ
have rw₁ : μ = HSMul.hSMul (α := ℝ≥0) 1 μ
Tactic: rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 μ
⊢ μ = c⁻¹ • c • μ
have rw₂ : μ = μ
Tactic: rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
Tactic: have hμ_smul (μ : Measure α) : μ = c⁻¹ • (c • μ) := by
    rw [smul_smul, inv_mul_cancel₀ hc, one_smul]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • μ
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have pos : ∀ (hμν : μ ≪ ν), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * 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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
pos : ∀ (hμν : μ ≪ ν), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have neg : ∀ (hμν : ¬μ ≪ ν), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * 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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : ¬μ ≪ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have neg : ¬c • μ ≪ c • ν
Tactic: rw [klDiv_of_not_ac hμν, klDiv_of_not_ac, ENNReal.mul_top hc']
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν
have neg : ∀ (h_contra : c • μ ≪ c • ν), μ ≪ ν
Tactic: refine fun h_contra ↦ hμν ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • ν
⊢ μ ≪ ν
have neg : c⁻¹ • c • μ ≪ c⁻¹ • c • ν
Tactic: rw [hμ_smul μ, hμ_smul ν]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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μν : μ ≪ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have pos : ∀ (h_int : Integrable (llr μ ν) μ), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * 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 ν
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 μ ν
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * 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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have neg : ¬Integrable (llr (c • μ) (c • ν)) (c • μ)
Tactic: rw [klDiv_of_not_integrable h_int, klDiv_of_not_integrable, ENNReal.mul_top hc']
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • μ)
have neg : ∀ (h_contra : Integrable (llr (c • μ) (c • ν)) (c • μ)), Integrable (llr μ ν) μ
Tactic: refine fun h_contra ↦ h_int ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 μ ν) μ
have neg : Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (c⁻¹ • c • μ)
Tactic: rw [hμ_smul μ, hμ_smul ν]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
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 • μ)
have neg : Integrable (llr (c⁻¹ • c • μ) (c⁻¹ • c • ν)) (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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have pos : ENNReal.ofReal (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ≥0∞) * ENNReal.ofReal (klDiv μ ν).toReal
Tactic: rw [← ENNReal.ofReal_toReal (klDiv_ne_top (hμν.smul c) _),
    ← ENNReal.ofReal_toReal (klDiv_ne_top 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 ν
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
⊢ klDiv (c • μ) (c • ν) = (↑c : ℝ≥0∞) * klDiv μ ν
have rw : Integrable (llr (c • μ) (c • ν)) (c • μ)
Tactic: rw [← ENNReal.ofReal_toReal (klDiv_ne_top (hμν.smul c) _),
    ← ENNReal.ofReal_toReal (klDiv_ne_top 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 ν
c : ℝ≥0
hc : ¬c = 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : ∀ (μ : Measure α), μ = c⁻¹ • c • μ
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (c • μ) (c • ν)) (c • μ)
have refine : Integrable (llr (c • μ) (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 μ ν) μ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have pos : ∀ (hμ : μ = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Tactic: by_cases hμ : μ = 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 μ ν) μ
pos : ∀ (hμ : μ = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have neg : ∀ (hμ : ¬μ = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Tactic: by_cases hμ : μ = 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 μ ν) μ
hμ : ¬μ = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have pos : ∀ (hν : ν = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Tactic: by_cases hν : ν = 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 μ ν) μ
hμ : ¬μ = 0
pos : ∀ (hν : ν = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have neg : ∀ (hν : ¬ν = 0), 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Tactic: by_cases hν : ν = 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 μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have pos : μ = 0
Tactic: refine absurd ?_ 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 μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ = 0
have hμν₁ : μ ≪ 0
Tactic: rw [hν] at hμν
Cleared hypotheses: hμν, h_int, hμ, 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have this : NeZero ν
Tactic: have : NeZero ν := ⟨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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have hμν' : μ ≪ ν'
Tactic: have hμν' : μ ≪ ν' := hμν.trans (Measure.absolutelyContinuous_smul (by simp))
-- 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 : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have neg : ∀ (h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ),
  0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
Tactic: have h := integral_llr_add_sub_measure_univ_nonneg hμν' ?_
-- 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 : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
neg :
  ∀ (h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ),
    0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have neg₁ : Integrable (llr μ ν') μ
Tactic: have h := integral_llr_add_sub_measure_univ_nonneg hμν' ?_
-- 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 : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
⊢ Integrable (llr μ ν') μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹)) μ
Tactic: rw [integrable_congr (llr_smul_right hμν (ν univ)⁻¹ (by simp) (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μν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
this : NeZero ν
ν' : Measure α := HSMul.hSMul (α := ℝ≥0∞) (((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) ν
hμν' : μ ≪ ν'
h : 0 ≤ ∫ (x : α), llr μ ν' x ∂μ + ν'.real univ - μ.real univ
⊢ 0 ≤ ∫ (x : α), llr μ ν x ∂μ + μ.real univ * log (ν.real univ) + 1 - μ.real univ
have h₁ : 0 ≤
  ∫ (a : α), llr μ ν a ∂μ - μ.real univ * log (ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) univ)⁻¹) + ν'.real univ -
    μ.real univ
Tactic: rw [integral_congr_ae (llr_smul_right hμν (ν univ)⁻¹ (by simp) (by simp [hν])),
    integral_sub h_int (integrable_const _), integral_const, smul_eq_mul] at h
Cleared hypotheses: h
-- 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 μ ν) μ
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have refine : Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
Tactic: refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν
-- 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 μ ν) μ
⊢ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal
have rw : Eq (α := ℝ) (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
Tactic: rw [toReal_klDiv_eq_integral_klFun hμν]
-- 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 μ ν) μ
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ (klDiv μ ν).toReal
have calc : ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
Tactic: calc ν.real univ * klFun (μ.real univ / ν.real univ)
  _ ≤ ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν := by
    refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν
    rwa [integrable_klFun_rnDeriv_iff hμν]
  _ = (klDiv μ ν).toReal := by rw [toReal_klDiv_eq_integral_klFun hμν]
-- 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 μ ν) μ
calc : ν.real univ * klFun (μ.real univ / ν.real univ) ≤ ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
⊢ ν.real univ * klFun (μ.real univ / ν.real univ) ≤ (klDiv μ ν).toReal
have calc₁ : ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν = (klDiv μ ν).toReal
Tactic: calc ν.real univ * klFun (μ.real univ / ν.real univ)
  _ ≤ ∫ x, klFun (μ.rnDeriv ν x).toReal ∂ν := by
    refine mul_le_integral_rnDeriv_of_ac convexOn_klFun continuous_klFun.continuousWithinAt ?_ hμν
    rwa [integrable_klFun_rnDeriv_iff hμν]
  _ = (klDiv μ ν).toReal := by rw [toReal_klDiv_eq_integral_klFun hμν]
-- 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 μ ν) μ
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have pos : ∀ (hμ : μ = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
Tactic: by_cases hμ : μ = 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 μ ν) μ
pos : ∀ (hμ : μ = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have neg : ∀ (hμ : ¬μ = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
Tactic: by_cases hμ : μ = 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 μ ν) μ
hμ : ¬μ = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have pos : ∀ (hν : ν = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
Tactic: by_cases hν : ν = 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 μ ν) μ
hμ : ¬μ = 0
pos : ∀ (hν : ν = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have neg : ∀ (hν : ¬ν = 0), μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
Tactic: by_cases hν : ν = 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 μ ν) μ
hμ : ¬μ = 0
hν : ν = 0
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have pos : μ = 0
Tactic: refine absurd ?_ hμ
-- 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
⊢ μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ ≤ (klDiv μ ν).toReal
have neg : μ.real univ * log (μ.real univ / ν.real univ) + ν.real univ - μ.real univ =
  ν.real univ * klFun (μ.real univ / ν.real univ)
Tactic: refine (le_of_eq ?_).trans (mul_klFun_le_toReal_klDiv 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 μ ν) μ
hμ : ¬μ = 0
hν : ¬ν = 0
⊢ ν.real univ * (μ.real univ / ν.real univ) = μ.real univ
have hb : ν.real univ ≠ 0
Tactic: rw [mul_div_cancel₀]