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

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_sub hf (integrable_const _)]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a ∂μ - ∫ (a : α), log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
exact hf.sub (integrable_const _)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

Tactic:
swap

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)) μ

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ =
    ∫ (x : α), llr μ ν x ∂μ + ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
abel

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a ∂μ - ∫ (a : α), log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
simp only [integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (x : α), f x - log (∫ (x : α), rexp (f x) ∂μ) + llr μ ν x ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

Tactic:
rw [integral_add ?_ h_int]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ ∫ (a : α), f a - log (∫ (x : α), rexp (f x) ∂μ) ∂μ + ∫ (a : α), llr μ ν a ∂μ =
    ∫ (x : α), f x ∂μ - log (∫ (x : α), rexp (f x) ∂μ) + ∫ (x : α), llr μ ν x ∂μ

α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : α → ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : SigmaFinite ν
hμν : μ ≪ ν
hf : Integrable f μ
h_int : Integrable (llr μ ν) μ
hfμ : Integrable (fun x => rexp (f x)) μ
hfν : AEMeasurable f ν
⊢ Integrable (fun x => f x - log (∫ (x : α), rexp (f x) ∂μ)) μ