awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
⊢ Eq (α := ℝ) (∫ (ω : Ω), ‖cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ))‖ ∂μ)
    (∫ (ω : Ω), rexp (z.re * X ω) ∂μ)

Tactic:
simp [Complex.norm_exp]

Premises used: Complex.norm_exp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
calc :
  Eq (α := ℝ) (∫ (ω : Ω), ‖cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ))‖ ∂μ)
    (∫ (ω : Ω), rexp (z.re * X ω) ∂μ)
⊢ Norm.norm (E := ℂ) (∫ (ω : Ω), cexp ((↑z.re : ℂ) * (↑(X ω) : ℂ)) * cexp ((↑z.im : ℂ) * I * (↑(X ω) : ℂ)) ∂μ) ≤
    mgf X μ z.re

Tactic:
calc ‖∫ ω, cexp (z.re * X ω) * cexp (z.im * I * X ω) ∂μ‖
  _ ≤ ∫ ω, ‖cexp (z.re * X ω) * cexp (z.im * I * X ω)‖ ∂μ := norm_integral_le_integral_norm _
  _ = ∫ ω, rexp (z.re * X ω) ∂μ := by simp [Complex.norm_exp]

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  Eq (α := ℝ) (∫ (x_1 : Ω), rexp (x * X x_1) ∂μ) (∫ (x_1 : Ω), (fun (x_2 : Ω) ↦ rexp (x * X x_2)) x_1 ∂μ)
⊢ ∫ (ω : Ω), cexp ((↑x : ℂ) * (↑(X ω) : ℂ)) ∂μ = (↑(∫ (x_1 : Ω), (fun (ω : Ω) ↦ rexp (x * X ω)) x_1 ∂μ) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ (↑x : ℂ)).re = mgf X μ x

Tactic:
simp [complexMGF_ofReal]

Premises used: ProbabilityTheory.complexMGF_ofReal
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (x : ℝ), (complexMGF X μ (↑x : ℂ)).re = mgf X μ x
⊢ (fun (x : ℝ) ↦ (complexMGF X μ (↑x : ℂ)).re) = mgf X μ

Tactic:
ext x
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ (↑x : ℂ)).re = mgf X μ x

Tactic:
re_complexMGF_ofReal x

Premises used: ProbabilityTheory.re_complexMGF_ofReal
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : ℝ
⊢ (complexMGF X μ (↑x : ℂ)).re = mgf X μ x

Tactic:
exact re_complexMGF_ofReal x

Premises used: ProbabilityTheory.re_complexMGF_ofReal
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
μ : Measure ℝ
t : ℝ
simp : Eq (α := ℂ) (∫ (ω : ℝ), cexp ((↑t : ℂ) * I * (↑ω : ℂ)) ∂μ) (∫ (x : ℝ), cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ)
⊢ complexMGF id μ ((↑t : ℂ) * I) = charFun μ t

Tactic:
simp only [complexMGF, id_eq, charFun, RCLike.inner_apply, conj_trivial, ofReal_mul]

Premises used: MeasureTheory.charFun, conj_trivial, RCLike.inner_apply, ProbabilityTheory.complexMGF, Complex.ofReal_mul, id_eq
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
μ : Measure ℝ
t : ℝ
e_f : ∀ (x : ℝ), cexp ((↑t : ℂ) * I * (↑x : ℂ)) = cexp ((↑t : ℂ) * (↑x : ℂ) * I)
⊢ Eq (α := ℂ) (∫ (ω : ℝ), cexp ((↑t : ℂ) * I * (↑ω : ℂ)) ∂μ) (∫ (x : ℝ), cexp ((↑t : ℂ) * (↑x : ℂ) * I) ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
μ : Measure ℝ
t x : ℝ
⊢ cexp ((↑t : ℂ) * I * (↑x : ℂ)) = cexp ((↑t : ℂ) * (↑x : ℂ) * I)

Tactic:
ring_nf
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
t : ℝ
rw :
  complexMGF (m := Real.measurableSpace) id (Measure.map X μ) ((↑t : ℂ) * I) =
    charFun (mE := Real.measurableSpace) (Measure.map X μ) t
rw₁ rw₂ :
  charFun (mE := Real.measurableSpace) (Measure.map X μ) t = charFun (mE := Real.measurableSpace) (Measure.map X μ) t
⊢ complexMGF X μ ((↑t : ℂ) * I) = charFun (mE := Real.measurableSpace) (Measure.map X μ) t

Tactic:
rw [← complexMGF_id_map hX, complexMGF_id_mul_I]

Premises used: ProbabilityTheory.complexMGF_id_mul_I, ProbabilityTheory.complexMGF_id_map
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ AEMeasurable X μ

Tactic:
have hX : AEMeasurable X μ := aemeasurable_of_mem_interior_integrableExpSet hz
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
⊢ z.re ∈ interior (integrableExpSet X μ)

Tactic:
have hz' := hz
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
hz' : z.re ∈ interior (integrableExpSet X μ)
⊢ ∃ (l : ℝ) (u : ℝ), z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ

Tactic:
rw [mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset] at hz'

Premises used: mem_interior_iff_mem_nhds, mem_nhds_iff_exists_Ioo_subset
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
hz' : ∃ (l : ℝ) (u : ℝ), z.re ∈ Set.Ioo l u ∧ Set.Ioo l u ⊆ integrableExpSet X μ
obtain :
  ∀ (l u : ℝ) (hlu : z.re ∈ Set.Ioo l u) (h_subset : Set.Ioo l u ⊆ integrableExpSet X μ),
    HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
obtain ⟨l, u, hlu, h_subset⟩ := hz'
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
⊢ 0 < min (z.re - l) (u - z.re)

Tactic:
simp [hlu.1, hlu.2]

Premises used: And.right, And.left
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
⊢ 0 < min (z.re - l) (u - z.re)

Tactic:
have h_pos : 0 < (z.re - l) ⊓ (u - z.re) := by simp [hlu.1, hlu.2]
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
⊢ 0 < t

Tactic:
have ht : 0 < t := half_pos h_pos
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
(hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2

Premises used: half_pos, hasDerivAt_integral_of_dominated_loc_of_deriv_le, Metric.ball_mem_nhds, And.right
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
refine_1 :
  ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ
refine_2 : Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_3 : AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ
refine_4 :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a
refine_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ
refine_6 :
  ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ (fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x a)
        ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) x
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
refine (hasDerivAt_integral_of_dominated_loc_of_deriv_le
    (bound := fun ω ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|))
    (F := fun z ω ↦ X ω ^ n * cexp (z * X ω))
    (F' := fun z ω ↦ X ω ^ (n + 1) * cexp (z * X ω)) (Metric.ball_mem_nhds _ (half_pos ht))
    ?_ ?_ ?_ ?_ ?_ ?_).2

Premises used: half_pos, hasDerivAt_integral_of_dominated_loc_of_deriv_le, Metric.ball_mem_nhds, And.right
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z_1 : ℂ
hz : z_1.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z_1.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z_1.re - l) (u - z_1.re) / 2
h_pos : 0 < min (z_1.re - l) (u - z_1.re)
ht : 0 < t
z : ℂ
⊢ AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᶠ (x : ℂ) in 𝓝 z,
    AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x) μ

Tactic:
exact .of_forall fun z ↦ by fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ

Tactic:
integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet hz n

Premises used: ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (ε := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) z) μ

Tactic:
exact integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet hz n

Premises used: ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ AEStronglyMeasurable (β := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) z) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a

Tactic:
ae_of_all _ fun ω ε hε ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
refine_4 :
  ∀ (ω : Ω) (ε : ℂ) (hε : ε ∈ Metric.ball z (t / 2)),
    Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ≤
      (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) ω
⊢ ∀ᵐ (a : Ω) ∂μ,
    ∀ x ∈ Metric.ball z (t / 2),
      Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x a) ≤
        (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) a

Tactic:
refine ae_of_all _ fun ω ε hε ↦ ?_

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
refine_4 : |X ω| ^ (n + 1) * ‖cexp (ε * (↑(X ω) : ℂ))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
⊢ Norm.norm (E := ℂ) ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ≤
    (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) ω

Tactic:
simp only [norm_mul, norm_pow, norm_real, Real.norm_eq_abs]

Premises used: norm_pow, norm_mul, Complex.norm_real, Real.norm_eq_abs
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
refine_4 : |X ω| ^ (n + 1) * rexp (ε * (↑(X ω) : ℂ)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
⊢ |X ω| ^ (n + 1) * ‖cexp (ε * (↑(X ω) : ℂ))‖ ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
rw [Complex.norm_exp]

Premises used: Complex.norm_exp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
refine_4 : |X ω| ^ (n + 1) * rexp (ε.re * X ω) ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)
⊢ |X ω| ^ (n + 1) * rexp (ε * (↑(X ω) : ℂ)).re ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
simp only [mul_re, ofReal_re, ofReal_im, mul_zero, sub_zero]

Premises used: Complex.mul_re, sub_zero, MulZeroClass.mul_zero, Complex.ofReal_re, Complex.ofReal_im
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
refine_4 : ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|
⊢ |X ω| ^ (n + 1) * rexp (ε.re * X ω) ≤ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ε = z + (ε - z)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
⊢ ε = z + (ε - z)

Tactic:
have : ε = z + (ε - z) := by simp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
refine_4 : z.re * X ω + (ε - z).re * X ω ≤ z.re * X ω + t / 2 * |X ω|
⊢ ε.re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Tactic:
rw [this, add_re, add_mul]

Premises used: add_mul, Complex.add_re
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
refine_4 : (ε - z).re * X ω ≤ t / 2 * |X ω|
⊢ z.re * X ω + (ε - z).re * X ω ≤ z.re * X ω + t / 2 * |X ω|

Tactic:
gcongr _ + ?_
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ (ε - z).re * X ω ≤ t / 2 * |X ω|

Tactic:
(le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
refine_4 : |(ε - z).re * X ω| ≤ t / 2 * |X ω|
⊢ (ε - z).re * X ω ≤ t / 2 * |X ω|

Tactic:
refine (le_abs_self _).trans ?_

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
refine_4 : |(ε - z).re| * |X ω| ≤ t / 2 * |X ω|
⊢ |(ε - z).re * X ω| ≤ t / 2 * |X ω|

Tactic:
rw [abs_mul]

Premises used: abs_mul
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
refine_4 : |(ε - z).re| ≤ t / 2
⊢ |(ε - z).re| * |X ω| ≤ t / 2 * |X ω|

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ |(ε - z).re| ≤ t / 2

Tactic:
(abs_re_le_norm _).trans ?_

Premises used: Complex.abs_re_le_norm, LE.le.trans
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
hε : ε ∈ Metric.ball z (t / 2)
this : ε = z + (ε - z)
⊢ ‖ε - z‖ < t / 2

Tactic:
simp only [Metric.mem_ball, dist_eq_norm] at hε

Premises used: dist_eq_norm, Metric.mem_ball
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
this : ε = z + (ε - z)
hε : ‖ε - z‖ < t / 2
⊢ ‖ε - z‖ ≤ t / 2

Tactic:
hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
ω : Ω
ε : ℂ
this : ε = z + (ε - z)
hε : ‖ε - z‖ < t / 2
⊢ ‖ε - z‖ ≤ t / 2

Tactic:
exact hε.le

Premises used: LT.lt.le
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
hX : AEMeasurable X μ
l u : ℝ
hlu : z.re ∈ Set.Ioo l u
h_subset : Set.Ioo l u ⊆ integrableExpSet X μ
t : ℝ := min (z.re - l) (u - z.re) / 2
h_pos : 0 < min (z.re - l) (u - z.re)
ht : 0 < t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

Tactic:
integrable_pow_abs_mul_exp_add_of_integrable_exp_mul ?_ ?_ ?_ ?_ (t := t) (n + 1)

Premises used: HAdd.hAdd, ProbabilityTheory.integrable_pow_abs_mul_exp_add_of_integrable_exp_mul, OfNat.ofNat