awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
have h₁ : μ.rnDeriv ν x ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞
Tactic: rw [ENNReal.toReal_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ llr ((↑c : ℝ≥0∞) • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)
have h : ∀ (x : α) (hx : llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ≥0∞).toReal),
  llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ)
Tactic: filter_upwards [llr_smul_left hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
x : α
hx : llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ≥0∞).toReal
⊢ llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ)
have h : llr μ ν x + log (↑c : ℝ≥0∞).toReal = llr μ ν x + log (↑c : ℝ)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (μ.rnDeriv (c • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal - log c.toReal
have h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
Tactic: have h := Measure.rnDeriv_smul_right_of_ne_top μ ν hc hc_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (μ.rnDeriv (c • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal - log c.toReal
have h₁ : ∀ (x : α) (hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x) (hx_pos : 0 < μ.rnDeriv ν x)
  (hx_ne_top : μ.rnDeriv ν x < ∞), log (μ.rnDeriv (c • ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Tactic: filter_upwards [hμν.ae_le h, Measure.rnDeriv_pos hμν, hμν.ae_le (Measure.rnDeriv_lt_top μ ν)]
    with x hx_eq hx_pos hx_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log (μ.rnDeriv (c • ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₁ : log ((c⁻¹ • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Tactic: rw [hx_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log ((c⁻¹ • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₁ : log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
Tactic: simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₁ : log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
h₁ : log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
⊢ log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₂ : c⁻¹.toReal ≠ 0
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
h₁ : log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
h₂ : c⁻¹.toReal ≠ 0
⊢ log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₃ : (μ.rnDeriv ν x).toReal ≠ 0
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ c⁻¹.toReal ≠ 0
have h₁ : c⁻¹ ≠ 0 ∧ c⁻¹ ≠ ∞
Tactic: rw [ENNReal.toReal_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0
have h₁ : μ.rnDeriv ν x ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞
Tactic: rw [ENNReal.toReal_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
x : α
hx_eq : μ.rnDeriv (c • ν) x = (c⁻¹ • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log c⁻¹.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
have h₁ : -log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
Tactic: rw [ENNReal.toReal_inv, log_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ llr μ ((↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)
have h : ∀ (x : α) (hx : llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ≥0∞).toReal),
  llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ)
Tactic: filter_upwards [llr_smul_right hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
x : α
hx : llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ≥0∞).toReal
⊢ llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ)
have h : llr μ ν x - log (↑c : ℝ≥0∞).toReal = llr μ ν x - log (↑c : ℝ)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)
have hc' : c⁻¹ ≠ 0
Tactic: have hc' : c⁻¹ ≠ 0 := by simp [hc_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)
have hc_ne_top' : c⁻¹ ≠ ∞
Tactic: have hc_ne_top' : c⁻¹ ≠ ∞ := by simp [hc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
⊢ llr (c⁻¹ • μ) ν =ᶠ[ae μ] llr μ (c • ν)
have h : ∀ (x : α) (hx_left : llr (c⁻¹ • μ) ν x = llr μ ν x + log c⁻¹.toReal)
  (hx_right : llr μ (c • ν) x = llr μ ν x - log c.toReal), llr (c⁻¹ • μ) ν x = llr μ (c • ν) x
Tactic: filter_upwards [llr_smul_left hμν c⁻¹ hc' hc_ne_top', llr_smul_right hμν c hc hc_ne_top] with
    x hx_left hx_right
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
hc' : c⁻¹ ≠ 0
hc_ne_top' : c⁻¹ ≠ ∞
x : α
hx_left : llr (c⁻¹ • μ) ν x = llr μ ν x + log c⁻¹.toReal
hx_right : llr μ (c • ν) x = llr μ ν x - log c.toReal
⊢ llr (c⁻¹ • μ) ν x = llr μ (c • ν) x
have h : llr μ ν x + log c⁻¹.toReal = llr μ ν x - log c.toReal
Tactic: rw [hx_left, hx_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((c • μ).rnDeriv (c • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal
have lift : ∀ (c : ℝ≥0) (hc : (↑c : ℝ≥0∞) ≠ 0),
  (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal
Tactic: lift c to ℝ≥0 using hc_ne_top
Cleared hypotheses: c, hc, hc_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : (↑c : ℝ≥0∞) ≠ 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal
have hc₁ : ¬c = 0
Tactic: norm_cast at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : ¬c = 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Eq (α := ℝ) ((fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) x)
                  ((fun (x : α) ↦ log (μ.rnDeriv ν x).toReal) x))
              x}
          x}
    a
Tactic: filter_upwards [hμν.ae_le (Measure.rnDeriv_smul_same μ ν hc)] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : ¬c = 0
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ (c • μ).rnDeriv (c • ν) x = μ.rnDeriv ν x) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ) ((fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) x)
                    ((fun (x : α) ↦ log (μ.rnDeriv ν x).toReal) x))
                x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal
have h₁ : ∀ (a : α),
  (c • μ).rnDeriv (c • ν) a = μ.rnDeriv ν a →
    log (((↑c : ℝ≥0∞) • μ).rnDeriv ((↑c : ℝ≥0∞) • ν) a).toReal = log (μ.rnDeriv ν a).toReal
Tactic: filter_upwards [hμν.ae_le (Measure.rnDeriv_smul_same μ ν hc)] with x hx using by simp [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] llr μ ν
have h : ∀ (x : α) (hx : llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x),
  llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x
Tactic: filter_upwards [llr_smul_same hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
x : α
hx : llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x
⊢ llr ((↑c : ℝ≥0∞) • μ) ((↑c : ℝ≥0∞) • ν) x = llr μ ν x
have h : llr μ ν x = llr μ ν x
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)
have simp_rw : Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal • log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)
Tactic: simp_rw [← smul_eq_mul, integral_rnDeriv_smul hμν, llr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
simp_rw : Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal • log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)
⊢ Eq (α := ℝ) (∫ (a : α), (μ.rnDeriv ν a).toReal * log (μ.rnDeriv ν a).toReal ∂ν) (∫ (a : α), llr μ ν a ∂μ)
have simp_rw₁ : Eq (α := ℝ) (∫ (x : α), log (μ.rnDeriv ν x).toReal ∂μ) (∫ (a : α), llr μ ν a ∂μ)
Tactic: simp_rw [← smul_eq_mul, integral_rnDeriv_smul hμν, llr]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
⊢ llr (μ.tilted f) ν =ᶠ[ae μ] fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
have h : ∀ (x : α) (hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal)
  (hx_pos : 0 < μ.rnDeriv ν x) (hx_lt_top : μ.rnDeriv ν x < ∞),
  llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
Tactic: filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ hfν), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
have h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0
Tactic: rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0
⊢ llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
have h₁ : rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0
Tactic: rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0
h₁ : rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0
⊢ llr (μ.tilted f) ν x = f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
have h₂ : (μ.rnDeriv ν x).toReal ≠ 0
Tactic: rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ 0
have h : ¬Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
Tactic: simp only [ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ≠ 0
have h : ¬(rexp (f x) = 0 ∨ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0)
Tactic: simp only [ne_eq, div_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
h0 : NeZero μ
x : α
hx : ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ∞
⊢ ¬(rexp (f x) = 0 ∨ Eq (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0)
have h : rexp (f x) ≠ 0 ∧ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ llr (μ.tilted f) ν =ᶠ[ae μ] fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl hμ =>
    simp only [hμ, ae_zero, Filter.EventuallyEq, Filter.eventually_bot]
  | inr h0 =>
    filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_left μ hfν), Measure.rnDeriv_pos hμν,
      hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top
    rw [llr, hx, log_mul, div_eq_mul_inv, log_mul (exp_pos _).ne', log_exp, log_inv, llr,
      ← sub_eq_add_neg]
    · simp only [ne_eq, inv_eq_zero]
      exact (integral_exp_pos hf).ne'
    · simp only [ne_eq, div_eq_zero_iff]
      push Not
      exact ⟨(exp_pos _).ne', (integral_exp_pos hf).ne'⟩
    · simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (llr (μ.tilted f) ν) μ
have rw : Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (z : α), rexp (f z) ∂μ) + llr μ ν x) μ
Tactic: rw [integrable_congr (llr_tilted_left hμν hfμ hfν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
have rw : HAdd.hAdd (α := ℝ) (∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
  ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
Tactic: rw [integral_add ?_ h_int]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst : IsProbabilityMeasure μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
hfν : AEMeasurable f ν
rw :
  HAdd.hAdd (α := ℝ) (∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ) (∫ (a : α), llr μ ν a ∂μ) =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ
have rw₁ : Integrable (ε := ℝ) (fun (x : α) ↦ f x - log (∫ (x : α), rexp (f x) ∂μ)) μ
Tactic: rw [integral_add ?_ h_int]