-- Mathlib/MeasureTheory/Measure/LogLikelihoodRatio.lean
lemma llr_tilted_right [SigmaFinite μ] [SigmaFinite ν]
    (hμν : μ ≪ ν) (hf : Integrable (fun x ↦ exp (f x)) ν) :
    (llr μ (ν.tilted f)) =ᵐ[μ] fun x ↦ - f x + log (∫ z, exp (f z) ∂ν) + llr μ ν x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
⊢ μ = 0

Tactic:
ext s _

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
s : Set α
a✝ : MeasurableSet s
⊢ μ s = 0 s

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Tactic:
filter_upwards [hμν.ae_le (toReal_rnDeriv_tilted_right μ ν hf), Measure.rnDeriv_pos hμν,
  hμν.ae_le (Measure.rnDeriv_lt_top μ ν)] with x hx hx_pos hx_lt_top

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Tactic:
have hμ : μ = 0 := by ext s _; exact hμν (by simp [h])

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
hμ : μ = 0
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
s : Set α
a✝ : MeasurableSet s
⊢ ν s = 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ⊤
⊢ ∫ (x : α), rexp (f x) ∂ν ≠ 0

Tactic:
exact (integral_exp_pos hf).ne'

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
s : Set α
a✝ : MeasurableSet s
⊢ μ s = 0 s

Tactic:
exact hμν (by simp [h])

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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:
rw [llr, hx, log_mul, log_mul (exp_pos _).ne', log_exp, llr]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ⊤
⊢ ∫ (x : α), rexp (f x) ∂ν ≠ 0

case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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

case h.hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ⊤
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
hμ : μ = 0
⊢ llr μ (ν.tilted f) =ᶠ[ae μ] fun x => -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr μ ν x

Tactic:
simp only [hμ, ae_zero, Filter.EventuallyEq]

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
hμ : μ = 0
⊢ ∀ᶠ (x : α) in ⊥, llr 0 (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr 0 ν x

Proof state:
case h.hy
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
hx_lt_top : μ.rnDeriv ν x < ⊤
⊢ (μ.rnDeriv ν x).toReal ≠ 0

Tactic:
simp [ENNReal.toReal_eq_zero_iff, hx_lt_top.ne, hx_pos.ne']

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h : ν = 0
hμ : μ = 0
⊢ ∀ᶠ (x : α) in ⊥, llr 0 (ν.tilted f) x = -f x + log (∫ (z : α), rexp (f z) ∂ν) + llr 0 ν x

Tactic:
exact Filter.eventually_bot

Result:
no goals

Proof state:
case h.hx
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
hx : (μ.rnDeriv (ν.tilted f) 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

Tactic:
refine (mul_pos (exp_pos _) (integral_exp_pos hf)).ne'

Result:
no goals