awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
h :
  ∀ (x : α) (hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal)
    (hx_pos : 0 < μ.rnDeriv ν x), rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦ (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [hμν.ae_le (exp_llr μ ν), Measure.rnDeriv_pos hμν] with x hx_eq hx_pos

Premises used: MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le, MeasureTheory.exp_llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
x : α
hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
h : (if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal) = (μ.rnDeriv ν x).toReal
h₁ h₂ : (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal

Tactic:
rw [hx_eq, if_neg hx_pos.ne']

Premises used: LT.lt.ne', if_neg
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
h :
  ∀ (x : α) (hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal)
    (hx_pos : 0 < μ.rnDeriv ν x), rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦ (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [exp_llr μ ν, Measure.rnDeriv_pos' hμν] with x hx hx_pos

Premises used: MeasureTheory.Measure.rnDeriv_pos', MeasureTheory.exp_llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
h h₁ h₂ h₃ :
  ∀ (hx : rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal) (hx_pos : 0 < μ.rnDeriv ν x),
    rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal

Tactic:
rwa [if_neg hx_pos.ne'] at hx

Premises used: LT.lt.ne', if_neg
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h : ∀ (x : α) (hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x), (-llr μ ν) x = llr ν μ x
⊢ -llr μ ν =ᶠ[ae μ] llr ν μ

Tactic:
filter_upwards [Measure.inv_rnDeriv hμν] with x hx

Premises used: MeasureTheory.Measure.inv_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
h : log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal
⊢ (-llr μ ν) x = llr ν μ x

Tactic:
rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]

Premises used: MeasureTheory.llr, ENNReal.toReal_inv, Real.log_inv, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
h :
  ∀ (x : α) (hx : (-llr μ ν) x = llr ν μ x) (hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal),
    rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (-llr μ ν x)) fun (x : α) ↦ (ν.rnDeriv μ x).toReal

Tactic:
filter_upwards [neg_llr hμν, exp_llr_of_ac' ν μ hμν] with x hx hx_exp_log

Premises used: MeasureTheory.exp_llr_of_ac', MeasureTheory.neg_llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ -llr μ ν x = llr ν μ x

Tactic:
rw [Pi.neg_apply] at hx

Premises used: Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
hx₁ : -llr μ ν x = llr ν μ x
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [Pi.neg_apply] at hx

Premises used: Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log h : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
h₁ h₂ : (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [hx, hx_exp_log]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
h :
  ∀ (x : α) (hx : (-llr ν μ) x = llr μ ν x) (hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal),
    rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (-llr μ ν x)) fun (x : α) ↦ (ν.rnDeriv μ x).toReal

Tactic:
filter_upwards [neg_llr hμν, exp_llr_of_ac ν μ hμν] with x hx hx_exp_log

Premises used: MeasureTheory.exp_llr_of_ac, MeasureTheory.neg_llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ llr ν μ x = -llr μ ν x

Tactic:
rw [Pi.neg_apply, neg_eq_iff_eq_neg] at hx

Premises used: neg_eq_iff_eq_neg, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
hx₁ : llr ν μ x = -llr μ ν x
⊢ rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [Pi.neg_apply, neg_eq_iff_eq_neg] at hx

Premises used: neg_eq_iff_eq_neg, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log h : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
h₁ h₂ : (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal

Tactic:
rw [← hx, hx_exp_log]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ Measurable (llr μ ν)

Tactic:
(Measure.measurable_rnDeriv μ ν).ennreal_toReal.log

Premises used: MeasureTheory.llr, Measurable.log, Measurable.ennreal_toReal, MeasureTheory.Measure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ StronglyMeasurable (llr μ ν)

Tactic:
(measurable_llr μ ν).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.measurable_llr
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν

Tactic:
have h := Measure.rnDeriv_smul_left_of_ne_top μ ν hc_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 ν
h₁ :
  ∀ (x : α) (hx_eq : (c • μ).rnDeriv ν 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
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((c • μ).rnDeriv ν x).toReal) fun (x : α) ↦
    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

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
h₁ : log ((c • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
⊢ log ((c • μ).rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal

Tactic:
rw [hx_eq]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
h₁ : log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal
⊢ log ((c • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
h₁ : log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
h₂ : c.toReal ≠ 0
h₃ : (μ.rnDeriv ν x).toReal ≠ 0
⊢ log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal

Tactic:
rw [log_mul]

Premises used: Real.log_mul
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
h₁ : c ≠ 0 ∧ c ≠ ∞
⊢ c.toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]

Premises used: ENNReal.toReal_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
⊢ c ≠ 0 ∧ c ≠ ∞

Tactic:
simp [hc, hc_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
h₁ : μ.rnDeriv ν x ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]

Premises used: ENNReal.toReal_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞

Tactic:
simp [hx_pos.ne', hx_ne_top.ne]

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 < ∞
⊢ log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
h :
  ∀ (x : α) (hx : llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ≥0∞).toReal),
    llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ)
⊢ llr ((↑c : ℝ≥0∞) • μ) ν =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x + log (↑c : ℝ)

Tactic:
filter_upwards [llr_smul_left hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx

Premises used: ENNReal.ofNNReal, MeasureTheory.llr_smul_left
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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
h : llr μ ν x + log (↑c : ℝ≥0∞).toReal = llr μ ν x + log (↑c : ℝ)
⊢ llr ((↑c : ℝ≥0∞) • μ) ν x = llr μ ν x + log (↑c : ℝ)

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 μ ν x + log (↑c : ℝ≥0∞).toReal = llr μ ν x + log (↑c : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν

Tactic:
have h := Measure.rnDeriv_smul_right_of_ne_top μ ν hc hc_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 ν
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
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log (μ.rnDeriv (c • ν) x).toReal) fun (x : α) ↦
    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

Premises used: MeasureTheory.Measure.rnDeriv_lt_top, MeasureTheory.Measure.rnDeriv_pos, MeasureTheory.Measure.AbsolutelyContinuous.ae_le
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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⁻¹ • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal
⊢ log (μ.rnDeriv (c • ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
rw [hx_eq]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal
⊢ log ((c⁻¹ • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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
h₃ : (μ.rnDeriv ν x).toReal ≠ 0
⊢ log (c⁻¹.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
rw [log_mul]

Premises used: Real.log_mul
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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₁ : c⁻¹ ≠ 0 ∧ c⁻¹ ≠ ∞
⊢ c⁻¹.toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]

Premises used: ENNReal.toReal_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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⁻¹ ≠ 0 ∧ c⁻¹ ≠ ∞

Tactic:
simp [hc, hc_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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₁ : μ.rnDeriv ν x ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
rw [ENNReal.toReal_ne_zero]

Premises used: ENNReal.toReal_ne_zero
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 ≠ 0 ∧ μ.rnDeriv ν x ≠ ∞

Tactic:
simp [hx_pos.ne', hx_ne_top.ne]

Premises used: LT.lt.ne', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
rw [ENNReal.toReal_inv, log_inv]

Premises used: ENNReal.toReal_inv, Real.log_inv
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0
hc : c ≠ 0
h :
  ∀ (x : α) (hx : llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ≥0∞).toReal),
    llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ)
⊢ llr μ ((↑c : ℝ≥0∞) • ν) =ᶠ[ae μ] fun (x : α) ↦ llr μ ν x - log (↑c : ℝ)

Tactic:
filter_upwards [llr_smul_right hμν (c : ℝ≥0∞) (by simpa) (by simp)] with x hx

Premises used: ENNReal.ofNNReal, MeasureTheory.llr_smul_right
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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
h : llr μ ν x - log (↑c : ℝ≥0∞).toReal = llr μ ν x - log (↑c : ℝ)
⊢ llr μ ((↑c : ℝ≥0∞) • ν) x = llr μ ν x - log (↑c : ℝ)

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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 μ ν x - log (↑c : ℝ≥0∞).toReal = llr μ ν x - log (↑c : ℝ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
simp [hc_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ c⁻¹ ≠ 0

Tactic:
have hc' : c⁻¹ ≠ 0 := by simp [hc_ne_top]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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
⊢ c⁻¹ ≠ ∞

Tactic:
simp [hc]
-- Module: Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
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
⊢ c⁻¹ ≠ ∞

Tactic:
have hc_ne_top' : c⁻¹ ≠ ∞ := by simp [hc]