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

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

Tactic:
congr

Result:
case inr.refine_4.h.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

Proof state:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]

Result:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν

Proof state:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ ⊤

Tactic:
simp

Result:
no goals

Proof state:
case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x => (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᶠ[ae ν] fun x =>
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
filter_upwards with x

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

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

Tactic:
simp_rw [h, ae_zero, Filter.EventuallyEq]

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

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

Tactic:
exact Filter.eventually_bot

Result:
no goals

Proof state:
case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ⊤

Tactic:
refine ae_of_all _ (by simp)

Result:
no goals

Proof state:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

Tactic:
exact (hf.1.aemeasurable.div_const _).ennreal_ofReal

Result:
no goals

Proof state:
case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Tactic:
filter_upwards

Result:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Proof state:
case inr.refine_2.h
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Result:
no goals

Proof state:
case inr.refine_4.h.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
exact div_pos (exp_pos _) (integral_exp_pos hf)

Result:
no goals

Proof state:
case inr.refine_4.h.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

Tactic:
rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]

Result:
case inr.refine_4.h.e_a
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

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

Tactic:
refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_

Result:
case inr.refine_1
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (fun x => ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

case inr.refine_2
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

case inr.refine_3
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ⊤

case inr.refine_4
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst✝¹ : SigmaFinite μ
inst✝ : SigmaFinite ν
hf : Integrable (fun x => rexp (f x)) ν
h0 : NeZero ν
⊢ (fun x => (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) =ᶠ[ae ν] fun x =>
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x