-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma llr_smul_right [IsFiniteMeasure μ] [Measure.HaveLebesgueDecomposition μ ν]
    (hμν : μ ≪ ν) (c : ℝ≥0∞) (hc : c ≠ 0) (hc_ne_top : c ≠ ∞) :
    llr μ (c • ν) =ᵐ[μ] fun x ↦ llr μ ν x - log c.toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ⊤
⊢ llr μ (c • ν) =ᶠ[ae μ] fun x => llr μ ν x - log c.toReal

Tactic:
simp only [llr, llr_def]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ⊤
⊢ (fun x => log (μ.rnDeriv (c • ν) x).toReal) =ᶠ[ae μ] fun x => log (μ.rnDeriv ν x).toReal - log c.toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ⊤
⊢ (fun x => log (μ.rnDeriv (c • ν) x).toReal) =ᶠ[ae μ] fun x => log (μ.rnDeriv ν x).toReal - log c.toReal

Tactic:
have h := Measure.rnDeriv_smul_right_of_ne_top μ ν hc hc_ne_top

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ⊤
h : μ.rnDeriv (c • ν) =ᶠ[ae ν] c⁻¹ • μ.rnDeriv ν
⊢ (fun x => log (μ.rnDeriv (c • ν) x).toReal) =ᶠ[ae μ] fun x => log (μ.rnDeriv ν x).toReal - log c.toReal

Proof state:
case h.hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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

Tactic:
rw [ENNReal.toReal_ne_zero]

Result:
case h.hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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 ≠ ⊤

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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

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

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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

Proof state:
case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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

Tactic:
rw [ENNReal.toReal_ne_zero]

Result:
case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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⁻¹ ≠ ⊤

Proof state:
case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝¹ : IsFiniteMeasure μ
inst✝ : μ.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]

Result:
no goals