-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet
    (hz : z.re ∈ interior (integrableExpSet X μ)) {p : ℝ} (hp : 0 ≤ p) :
    Integrable (fun ω ↦ (|X ω| ^ p : ℝ) * cexp (z * X ω)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
swap

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
exact AEMeasurable.aestronglyMeasurable (by fun_prop)

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
rw [← integrable_norm_iff]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
fun_prop

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz

Result:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun ω => ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a => ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

Tactic:
simpa [abs_rpow_of_nonneg (abs_nonneg _), Complex.norm_exp]
  using integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp

Result:
no goals