awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
h_subset (sub_half_inf_sub_mem_Ioo hvlu)

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo, Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ

Tactic:
exact h_subset (sub_half_inf_sub_mem_Ioo hvlu)

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
h : ∀ (ω : Ω), |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hv
      (by positivity : 0 ≤ (n : ℝ)) with
    ω

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ |X ω| ^ n = HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
rw :
  ∀ (hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ) {p : ℝ} (hp : 0 ≤ p),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hv

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : ∃ (l : ℝ) (u : ℝ), v ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
p : ℝ
hp : 0 ≤ p
obtain :
  ∀ (l u : ℝ) (hvlu : v ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
obtain ⟨l, u, hvlu, h_subset⟩ := hv
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
integrable_rpow_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v p : ℝ
hp : 0 ≤ p
l u : ℝ
hvlu : v ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
h_pos : 0 < min (v - l) (u - v)
refine_1 : min (v - l) (u - v) / 2 ≠ 0
refine_2 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v + min (v - l) (u - v) / 2) * X ω)) μ
refine_3 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((v - min (v - l) (u - v) / 2) * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (v * X ω)) μ

Tactic:
refine integrable_rpow_mul_exp_of_integrable_exp_mul
    (t := min (v - l) (u - v) / 2) ?_ ?_ ?_ hp

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
h : ∀ (ω : Ω), X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n * rexp (v * X ω)) μ

Tactic:
convert!
    integrable_rpow_mul_exp_of_mem_interior_integrableExpSet hv (by positivity : 0 ≤ (n : ℝ)) with ω

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ X ω ^ n = HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)) μ

Tactic:
integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet h hp

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
h₁ : Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) μ

Tactic:
convert! integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet h hp using 1

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ |X ω| ^ p) fun (ω : Ω) ↦ |X ω| ^ p * rexp (0 * X ω)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n * rexp (0 * X ω)) μ

Tactic:
integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet h n

Premises used: ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
h₁ : ∀ (x : Ω), |X x| ^ n = |X x| ^ n * rexp (0 * X x)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ n) μ

Tactic:
convert! integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet h n

Premises used: ProbabilityTheory.integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x : Ω
⊢ |X x| ^ n = |X x| ^ n * rexp (0 * X x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)) μ

Tactic:
integrable_rpow_mul_exp_of_mem_interior_integrableExpSet h hp

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
h₁ : Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω ^ p) fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ p) μ

Tactic:
convert! integrable_rpow_mul_exp_of_mem_interior_integrableExpSet h hp using 1

Premises used: ProbabilityTheory.integrable_rpow_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ Eq.{u_1 + 1} (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω ^ p) fun (ω : Ω) ↦ X ω ^ p * rexp (0 * X ω)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n * rexp (0 * X ω)) μ

Tactic:
integrable_pow_mul_exp_of_mem_interior_integrableExpSet h n

Premises used: ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
h₁ : ∀ (x : Ω), X x ^ n = X x ^ n * rexp (0 * X x)
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω ^ n) μ

Tactic:
convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h n

Premises used: ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x : Ω
⊢ X x ^ n = X x ^ n * rexp (0 * X x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
⊢ AEMeasurable X μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet h
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
pos : ∀ (hp_zero : p = 0), MemLp X (↑p : ℝ≥0∞) μ
neg : ∀ (hp_zero : ¬p = 0), MemLp X (↑p : ℝ≥0∞) μ
⊢ MemLp X (↑p : ℝ≥0∞) μ

Tactic:
by_cases hp_zero : p = 0
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
pos : AEStronglyMeasurable X μ
⊢ MemLp X (↑p : ℝ≥0∞) μ

Tactic:
simp only [hp_zero, ENNReal.coe_zero, memLp_zero_iff_aestronglyMeasurable]

Premises used: ENNReal.coe_zero, MeasureTheory.memLp_zero_iff_aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ

Tactic:
hX.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : p = 0
⊢ AEStronglyMeasurable X μ

Tactic:
exact hX.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ (↑p : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖X x‖ ^ (↑p : ℝ≥0∞).toReal) μ
⊢ MemLp X (↑p : ℝ≥0∞) μ

Tactic:
rw [← integrable_norm_rpow_iff hX.aestronglyMeasurable (mod_cast hp_zero) (by simp)]

Premises used: AEMeasurable.aestronglyMeasurable, MeasureTheory.integrable_norm_rpow_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ)) μ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ ‖X x‖ ^ (↑p : ℝ≥0∞).toReal) μ

Tactic:
simp only [norm_eq_abs, ENNReal.coe_toReal]

Premises used: ENNReal.coe_toReal, Real.norm_eq_abs
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ)) μ

Tactic:
integrable_rpow_abs_of_mem_interior_integrableExpSet h p.2

Premises used: ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet, Subtype.property
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp_zero : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ)) μ

Tactic:
exact integrable_rpow_abs_of_mem_interior_integrableExpSet h p.2

Premises used: ProbabilityTheory.integrable_rpow_abs_of_mem_interior_integrableExpSet, Subtype.property
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
⊢ Integrable X μ

Tactic:
simpa using integrable_pow_of_mem_interior_integrableExpSet h 1

Premises used: ProbabilityTheory.integrable_pow_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ
rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
rw [← integrable_norm_iff]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖cexp (z * (↑(X a) : ℂ))‖) μ

Tactic:
simpa [Complex.norm_exp] using hz

Premises used: Complex.norm_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hX : AEMeasurable X μ
hz : z.re ∈ integrableExpSet X μ
⊢ AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
integrable_cexp_mul_of_re_mem_integrableExpSet
    (aemeasurable_of_mem_interior_integrableExpSet hz) (interior_subset hz)

Premises used: ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet, ProbabilityTheory.aemeasurable_of_mem_interior_integrableExpSet, interior_subset
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
⊢ AEMeasurable X μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(|X a| ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ
rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
rw [← integrable_norm_iff]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(|X ω| ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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

Premises used: ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet, Real.abs_rpow_of_nonneg, Complex.norm_exp, abs_nonneg
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(HPow.hPow (β := ℝ) |X ω| (↑n : ℝ)) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Premises used: Nat.cast_nonneg, ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
h : ∀ (x : Ω), (↑|X x| : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) |X x| (↑n : ℝ)) : ℂ)
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑|X ω| : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
convert! integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Premises used: Nat.cast_nonneg, ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x : Ω
⊢ (↑|X x| : ℂ) ^ n = (↑(HPow.hPow (β := ℝ) |X x| (↑n : ℝ)) : ℂ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
rw : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(X a ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ
rw₁ : AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
rw [← integrable_norm_iff]

Premises used: MeasureTheory.integrable_norm_iff
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℂ) (fun (ω : Ω) ↦ (↑(X ω ^ p) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
simp : Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖(↑(X a ^ p) : ℂ) * cexp (z * (↑(X a) : ℂ))‖) μ

Tactic:
simp only [norm_mul, norm_real, Complex.norm_exp, mul_re, ofReal_re,
    ofReal_im, mul_zero, sub_zero]

Premises used: Complex.mul_re, sub_zero, norm_mul, Complex.norm_real, MulZeroClass.mul_zero, Complex.norm_exp, Complex.ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : 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‖ * rexp (z.re * X a)) μ

Tactic:
(integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_

Premises used: MeasureTheory.Integrable.mono, ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ
refine_2 : ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ

Tactic:
refine (integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet hz hp).mono ?_ ?_

Premises used: MeasureTheory.Integrable.mono, ProbabilityTheory.integrable_rpow_abs_mul_exp_of_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
funProp : 0 ≤ p
⊢ AEStronglyMeasurable (β := ℝ) (fun (a : Ω) ↦ ‖X a ^ p‖ * rexp (z.re * X a)) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖

Tactic:
ae_of_all _ fun ω ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
refine_2 : ∀ (ω : Ω), ‖‖X ω ^ p‖ * rexp (z.re * X ω)‖ ≤ ‖|X ω| ^ p * rexp (z.re * X ω)‖
⊢ ∀ᵐ (a : Ω) ∂μ, ‖‖X a ^ p‖ * rexp (z.re * X a)‖ ≤ ‖|X a| ^ p * rexp (z.re * X a)‖

Tactic:
refine ae_of_all _ fun ω ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
refine_2 : |(|X ω ^ p|)| * rexp (z.re * X ω) ≤ ||X ω| ^ p| * rexp (z.re * X ω)
⊢ ‖‖X ω ^ p‖ * rexp (z.re * X ω)‖ ≤ ‖|X ω| ^ p * rexp (z.re * X ω)‖

Tactic:
simp only [norm_mul, Real.norm_eq_abs, Real.abs_exp]

Premises used: norm_mul, Real.norm_eq_abs, Real.abs_exp
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
refine_2 : |X ω ^ p| ≤ |X ω| ^ p
⊢ |(|X ω ^ p|)| * rexp (z.re * X ω) ≤ ||X ω| ^ p| * rexp (z.re * X ω)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

Tactic:
abs_rpow_le_abs_rpow _ _

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
ω : Ω
⊢ |X ω ^ p| ≤ |X ω| ^ p

Tactic:
exact abs_rpow_le_abs_rpow _ _

Premises used: Real.abs_rpow_le_abs_rpow
-- Module: Mathlib.Probability.Moments.IntegrableExpMul
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (ε := ℂ) (fun (ω : Ω) ↦ (↑(HPow.hPow (β := ℝ) (X ω) (↑n : ℝ)) : ℂ) * cexp (z * (↑(X ω) : ℂ))) μ

Tactic:
integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Premises used: ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet, Nat.cast_nonneg