-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma toReal_rnDeriv_tilted_right (μ ν : Measure α) [SigmaFinite μ] [SigmaFinite ν]
    (hf : Integrable (fun x ↦ exp (f x)) ν) :
    (fun x ↦ (μ.rnDeriv (ν.tilted f) x).toReal)
      =ᵐ[ν] fun x ↦ exp (- f x) * (∫ x, exp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
⊢ (fun x => (μ.rnDeriv (ν.tilted f) x).toReal) =ᶠ[ae ν] fun x =>
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
simp only [ENNReal.toReal_mul, gt_iff_lt, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν

Tactic:
positivity

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0

Tactic:
exact Or.inl (by positivity)

Result:
no goals