awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
mp : klDiv μ ν = ∞ → μ ≪ ν → ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞ ↔ μ ≪ ν → ¬Integrable (llr μ ν) μ
have mpr : (μ ≪ ν → ¬Integrable (llr μ ν) μ) → klDiv μ ν = ∞
Tactic: constructor
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : klDiv μ ν = ∞
⊢ μ ≪ ν → ¬Integrable (llr μ ν) μ
have mp : ∀ (h : μ ≪ ν ∧ Integrable (llr μ ν) μ), klDiv μ ν ≠ ∞
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ∞
have mpr : ∀ (h : ¬Integrable (llr μ ν) μ), klDiv μ ν = ∞
Tactic: rcases or_not_of_imp h with (h | h)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : μ ≪ ν → ¬Integrable (llr μ ν) μ
mpr : ∀ (h : ¬Integrable (llr μ ν) μ), klDiv μ ν = ∞
⊢ klDiv μ ν = ∞
have mpr₁ : ∀ (h : ¬μ ≪ ν), klDiv μ ν = ∞
Tactic: rcases or_not_of_imp h with (h | h)
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞
have rw : (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) else ∞) =
  if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞
Tactic: rw [klDiv_def]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν ∧ Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
    ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
have rw : ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ) =
  ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ)
Tactic: rw [integral_klFun_rnDeriv h.1 h.2]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ klDiv μ ν = if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have rw : (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
  if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
Tactic: rw [klDiv_eq_integral_klFun]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos : ∀ (hμν : μ ≪ ν),
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
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μν : μ ≪ ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have neg : ∀ (hμν : ¬μ ≪ ν),
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
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μν : μ ≪ ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos : ∀
  (h_int_iff :
    ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
      Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν),
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
Tactic: have h_int_iff := lintegral_ofReal_ne_top_iff_integrable
    (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
-- 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_iff :
      ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
        Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
Tactic: have h_int_iff := lintegral_ofReal_ne_top_iff_integrable
    (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
-- 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_iff :
      ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
        Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
pos₁ : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos₂ : (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal
Tactic: have h_int_iff := lintegral_ofReal_ne_top_iff_integrable
    (f := fun x ↦ klFun (μ.rnDeriv ν x).toReal) (μ := ν) ?_ ?_
-- 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos : ∀ (h_int : Integrable (llr μ ν) μ),
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
pos :
  ∀ (h_int : Integrable (llr μ ν) μ),
    (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
      if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ),
  (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have pos : ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
  ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν
Tactic: simp only [hμν, h_int, and_self, ↓reduceIte]
-- 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
⊢ ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν
have pos : Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
Tactic: rw [ofReal_integral_eq_lintegral_ofReal]
-- 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : Integrable (llr μ ν) μ
pos : Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
⊢ ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) =
    ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν
have pos₁ : (ae ν).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal
Tactic: rw [ofReal_integral_eq_lintegral_ofReal]
-- 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν ≠ ∞ ↔
    Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have h_int_iff₁ : ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
  ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
Tactic: rw [← not_iff_not, ne_eq, Decidable.not_not] at h_int_iff
Cleared hypotheses: h_int_iff, 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_iff :
  ∫⁻ (a : α), ENNReal.ofReal (klFun (μ.rnDeriv ν a).toReal) ∂ν = ∞ ↔
    ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
h_int : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞) =
    if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞
have neg : (if μ ≪ ν then ∫⁻ (x : α), ENNReal.ofReal (klFun (μ.rnDeriv ν x).toReal) ∂ν else ∞) =
  if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν) else ∞
Tactic: symm
-- 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 - μ.real univ
have rw : LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
Tactic: rw [← integral_klFun_rnDeriv 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 μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ
have rw : 0 ≤ ∫ (x : α), llr μ ν x ∂μ + ν.real univ - μ.real univ
Tactic: rw [klDiv_of_ac_of_integrable h h_int, ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
have pos : ∀ (h_int : Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
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_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
pos : ∀ (h_int : Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
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_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h_int : ¬Integrable (llr μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
have neg : ENNReal.toReal ∞ = ∫ (a : α), llr μ ν a ∂μ
Tactic: rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h_int : ¬Integrable (llr μ ν) μ
neg : ENNReal.toReal ∞ = ∫ (a : α), llr μ ν a ∂μ
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
have neg₁ : ENNReal.toReal ∞ = 0
Tactic: rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
h_eq : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
h_int : ¬Integrable (llr μ ν) μ
neg : ENNReal.toReal ∞ = ∫ (a : α), llr μ ν a ∂μ
neg₁ : ENNReal.toReal ∞ = 0
⊢ (klDiv μ ν).toReal = ∫ (a : α), llr μ ν a ∂μ
have neg₂ : Eq (α := ℝ) 0 0
Tactic: rw [klDiv_of_not_integrable h_int, integral_undef h_int, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ ≪ ν
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have pos : ∀ (h_int : Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
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 μ ν) μ), (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have neg : ∀ (h_int : ¬Integrable (llr μ ν) μ), (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
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 μ ν) μ
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have pos : LE.le (α := ℝ) 0 (∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν)
Tactic: rw [klDiv_eq_integral_klFun, if_pos ⟨h, h_int⟩, ENNReal.toReal_ofReal]
-- 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 μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have neg : (klDiv μ ν).toReal = 0
Tactic: rw [integral_undef]
-- 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 μ ν) μ
neg : (klDiv μ ν).toReal = 0
⊢ (klDiv μ ν).toReal = ∫ (x : α), klFun (μ.rnDeriv ν x).toReal ∂ν
have neg₁ : ¬Integrable (ε := ℝ) (fun (x : α) ↦ klFun (μ.rnDeriv ν x).toReal) ν
Tactic: rw [integral_undef]
-- 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 μ ν).toReal = 0
have neg : ENNReal.toReal ∞ = 0
Tactic: rw [klDiv_of_not_integrable h_int, ENNReal.toReal_top]
-- 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 μ ν) μ
neg : ENNReal.toReal ∞ = 0
⊢ (klDiv μ ν).toReal = 0
have neg₁ : Eq (α := ℝ) 0 0
Tactic: rw [klDiv_of_not_integrable h_int, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
have pos : ∀ (hc : c = 0),
  (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
Tactic: by_cases hc : c = 0
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
pos :
  ∀ (hc : c = 0),
    (klDiv (c • μ) ν).toReal =
      (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
have neg : ∀ (hc : ¬c = 0),
  (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
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 ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
have h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
Tactic: have h_llr := 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
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
have neg : ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
  (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
    (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
Tactic: rw [toReal_klDiv hμν h_int, toReal_klDiv (hμν.smul_left c)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
neg :
  ∫ (a : α), llr (c • μ) ν a ∂c • μ + ν.real univ - (c • μ).real univ =
    (↑c : ℝ) * (∫ (a : α), llr μ ν a ∂μ + ν.real univ - μ.real univ) + (1 - (↑c : ℝ)) * ν.real univ +
      (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
⊢ (klDiv (c • μ) ν).toReal =
    (↑c : ℝ) * (klDiv μ ν).toReal + (1 - (↑c : ℝ)) * ν.real univ + (↑c : ℝ) * log (↑c : ℝ) * μ.real univ
have neg₁ : Integrable (llr (c • μ) ν) (c • μ)
Tactic: rw [toReal_klDiv hμν h_int, toReal_klDiv (hμν.smul_left c)]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ Integrable (llr (c • μ) ν) (c • μ)
have neg : Integrable (llr (c • μ) ν) μ
Tactic: refine Integrable.smul_measure_nnreal ?_
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ Integrable (llr (c • μ) ν) μ
have neg : Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ
Tactic: rw [integrable_congr h_llr]
-- Lean 4 proof step from Mathlib.InformationTheory.KullbackLeibler.Basic (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
hμν : μ ≪ ν
h_int : Integrable (llr μ ν) μ
c : ℝ≥0
hc : ¬c = 0
h_llr : llr (c • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)) μ
have funProp : ‖log (↑c : ℝ)‖ₑ ≠ ∞
Tactic: fun_prop