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

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∫ (x : α), rexp (f x) ∂μ ≠ 0

Tactic:
exact (integral_exp_pos hf).ne'

Result:
no goals

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

Tactic:
have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
⊢ (fun x => log ((μ.tilted f).rnDeriv μ x).toReal) =ᶠ[ae μ] fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)

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

Tactic:
positivity

Result:
no goals

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

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

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

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

Tactic:
filter_upwards [rnDeriv_tilted_left_self hf'] with x hx

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

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

Tactic:
rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : SigmaFinite μ
hf : Integrable (fun x => rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ∫ (x : α), rexp (f x) ∂μ ≠ 0

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

Tactic:
cases eq_zero_or_neZero μ with
| inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
| inr h0 =>
  have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
  filter_upwards [rnDeriv_tilted_left_self hf'] with x hx
  rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
  exact (integral_exp_pos hf).ne'

Result:
no goals

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

Tactic:
exact Filter.eventually_bot

Result:
no goals