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
⊢ (↑c : ℝ) *
      ((↑c⁻¹ : ℝ) * (klDiv μ ν).toReal + (1 - (↑c⁻¹ : ℝ)) * ν.real univ + (↑c⁻¹ : ℝ) * log (↑c⁻¹ : ℝ) * μ.real univ) =
    (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ
have simp : (↑c : ℝ) *
    ((↑c : ℝ)⁻¹ * (klDiv μ ν).toReal + (1 - (↑c : ℝ)⁻¹) * ν.real univ - (↑c : ℝ)⁻¹ * log (↑c : ℝ) * μ.real univ) =
  (klDiv μ ν).toReal + ((↑c : ℝ) - 1) * ν.real univ - log (↑c : ℝ) * μ.real univ
Tactic: simp only [NNReal.coe_inv, log_inv, mul_neg, neg_mul, ← sub_eq_add_neg]
-- 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 • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
have pos : ∀ (hc : c = 0), (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).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 • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
⊢ (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
have neg : ∀ (hc : ¬c = 0), (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).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 • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
have neg : c • μ ≪ ν
Tactic: rw [toReal_klDiv_smul_right_eq_smul_left, 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 ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
neg : c • μ ≪ ν
⊢ (klDiv (c • μ) (c • ν)).toReal = (↑c : ℝ) * (klDiv μ ν).toReal
have neg₁ : Integrable (llr (c • μ) ν) (c • μ)
Tactic: rw [toReal_klDiv_smul_right_eq_smul_left, 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 ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ 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
⊢ Integrable (llr (c • μ) ν) μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ
Tactic: rw [integrable_congr (llr_smul_nnreal_left 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
⊢ 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 ν
c : ℝ≥0
hc : c ≠ 0
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
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 α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
⊢ μ = c • c⁻¹ • μ
have rw : μ = (c * c⁻¹) • μ
Tactic: rw [smul_smul, mul_inv_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
rw : μ = (c * c⁻¹) • μ
⊢ μ = c • c⁻¹ • μ
have rw₁ : μ = HSMul.hSMul (α := ℝ≥0) 1 μ
Tactic: rw [smul_smul, mul_inv_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
rw : μ = (c * c⁻¹) • μ
rw₁ : μ = HSMul.hSMul (α := ℝ≥0) 1 μ
⊢ μ = c • c⁻¹ • μ
have rw₂ : μ = μ
Tactic: rw [smul_smul, mul_inv_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 : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have hμ_smul : μ = c • c⁻¹ • μ
Tactic: have hμ_smul : μ = c • (c⁻¹ • μ) := by rw [smul_smul, mul_inv_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 : μ = c • c⁻¹ • μ
⊢ ν = 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 α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
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 α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
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
hμ_smul : μ = c • c⁻¹ • μ
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have hν_smul : ν = c⁻¹ • c • ν
Tactic: have hν_smul : ν = 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have pos : ∀ (hμν : μ ≪ ν), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
pos : ∀ (hμν : μ ≪ ν), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg : ∀ (hμν : ¬μ ≪ ν), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg : ¬c⁻¹ • μ ≪ ν
Tactic: rw [klDiv_of_not_ac, 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
neg : ¬c⁻¹ • μ ≪ ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg₁ : ¬μ ≪ c • ν
Tactic: rw [klDiv_of_not_ac, 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ ¬c⁻¹ • μ ≪ ν
have neg : ∀ (h_contra : 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : c⁻¹ • μ ≪ ν
⊢ μ ≪ ν
have neg : c • c⁻¹ • μ ≪ ν
Tactic: rw [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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
⊢ ¬μ ≪ c • ν
have neg : ∀ (h_contra : μ ≪ 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : ¬μ ≪ ν
h_contra : μ ≪ c • ν
⊢ μ ≪ ν
have neg : μ ≪ c⁻¹ • c • ν
Tactic: rw [hν_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
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have hμν_right : μ ≪ (↑c : ℝ≥0∞) • ν
Tactic: have hμν_right := hμν.smul_right 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have pos : ∀ (h_int : Integrable (llr μ ν) μ), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
pos : ∀ (h_int : Integrable (llr μ ν) μ), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg : ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
Tactic: rw [klDiv_of_not_integrable, 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
neg : ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have neg₁ : ¬Integrable (llr μ (c • ν)) μ
Tactic: rw [klDiv_of_not_integrable, 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
have neg : ∀ (h_contra : Integrable (llr (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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr μ ν) μ
have neg : Integrable (llr (c • c⁻¹ • μ) ν) (c • c⁻¹ • μ)
Tactic: rw [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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c • c⁻¹ • μ)
have neg : Integrable (llr (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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (llr (c • c⁻¹ • μ) ν) (c⁻¹ • μ)
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr (c⁻¹ • μ) ν x + log (↑c : ℝ)) (c⁻¹ • μ)
Tactic: rw [integrable_congr (llr_smul_nnreal_left (hμν.smul_left _) c 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr (c⁻¹ • μ) ν x + log (↑c : ℝ)) (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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
⊢ ¬Integrable (llr μ (c • ν)) μ
have neg : ∀ (h_contra : Integrable (llr μ (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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ ν) μ
have neg : Integrable (llr μ (c⁻¹ • c • ν)) μ
Tactic: rw [hν_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
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
have this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
Tactic: have : IsFiniteMeasure ((c : ℝ≥0∞) • ν) := by
        simp only [Measure.coe_nnreal_smul]
        infer_instance
-- 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
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
have h : llr μ (c⁻¹ • (↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ((↑c : ℝ≥0∞) • ν) x - log (↑c⁻¹ : ℝ)
Tactic: have h := llr_smul_nnreal_right (hμν.smul_right hc') c⁻¹ (by simpa)
-- 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
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • (↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ((↑c : ℝ≥0∞) • ν) x - log (↑c⁻¹ : ℝ)
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
have h₁ : llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)
Tactic: simp only [Measure.coe_nnreal_smul, NNReal.coe_inv, log_inv, sub_neg_eq_add] at h
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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)
⊢ Integrable (llr μ (c⁻¹ • c • ν)) μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)) μ
Tactic: rw [integrable_congr 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 : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : ¬Integrable (llr μ ν) μ
h_contra : Integrable (llr μ (c • ν)) μ
this : IsFiniteMeasure ((↑c : ℝ≥0∞) • ν)
h : llr μ (c⁻¹ • c • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ (c • ν) x + log (↑c : ℝ)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ (c • ν) 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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
have refine : 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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (llr (c⁻¹ • μ) ν) μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c⁻¹ : ℝ)) μ
Tactic: rw [integrable_congr (llr_smul_nnreal_left 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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
⊢ Integrable (ε := ℝ) (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 ν
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 μ ν) μ
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
Tactic: have h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ) := by
    refine Integrable.smul_measure_nnreal ?_
    rw [integrable_congr (llr_smul_nnreal_left hμν c⁻¹ (by simpa))]
    fun_prop
-- 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⁻¹ • μ)
⊢ Integrable (llr μ (c • ν)) μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)) μ
Tactic: rw [integrable_congr (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 ν
c : ℝ≥0
hc : c ≠ 0
hc' : (↑c : ℝ≥0∞) ≠ 0
hμ_smul : μ = c • c⁻¹ • μ
hν_smul : ν = c⁻¹ • c • ν
hμν : μ ≪ ν
hμν_right : μ ≪ c • ν
h_int : Integrable (llr μ ν) μ
h_int_left : Integrable (llr (c⁻¹ • μ) ν) (c⁻¹ • μ)
⊢ Integrable (ε := ℝ) (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 ν
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⁻¹ • μ)
⊢ klDiv μ (c • ν) = (↑c : ℝ≥0∞) * klDiv (c⁻¹ • μ) ν
have h_int_right : Integrable (llr μ (c • ν)) μ
Tactic: have h_int_right : Integrable (llr μ (c • ν)) μ := by
    rw [integrable_congr (llr_smul_nnreal_right hμν c (by simpa))]
    fun_prop