-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma setIntegral_tilted [SFinite μ] (f : α → ℝ) (g : α → E) (s : Set α) :
    ∫ x in s, g x ∂(μ.tilted f) = ∫ x in s, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) (μ.restrict s)

Tactic:
rw [← aemeasurable_coe_nnreal_real_iff]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) (μ.restrict s)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) (μ.restrict s)

Tactic:
refine AEMeasurable.restrict ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) μ

Tactic:
simpa only [NNReal.coe_mk]

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, ⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩ • g x ∂μ =
    ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
congr

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
  integral_zero_measure]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ 0 = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ 0 = ∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀']

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, ⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩ • g x ∂μ =
    ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x => ⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) (μ.restrict s)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (fun x => rexp (f x)) μ

Tactic:
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Result:
no goals

Proof state:
case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

Tactic:
exact (measurable_exp.comp_aemeasurable hf).div_const _

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
by_cases hf : AEMeasurable f μ

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Proof state:
case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x => ⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) (μ.restrict s)

Tactic:
suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ by
  rw [← aemeasurable_coe_nnreal_real_iff]
  refine AEMeasurable.restrict ?_
  simpa only [NNReal.coe_mk]

Result:
case pos.hf
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ

Tactic:
have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
  exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ ∫ (x : α) in s, g x ∂μ.tilted f = ∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ