-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma setIntegral_tilted' (f : α → ℝ) (g : α → E) {s : Set α} (hs : MeasurableSet s) :
    ∫ 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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
⊢ ∫ (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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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 neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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 ∂μ

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

Tactic:
rw [integral_undef hf']

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

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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₀ _ _ hs]

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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 ∂μ

α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) μ