awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_5 : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ
refine_5₁ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ
refine_5₂ : 0 ≤ t / 2
refine_5₃ : t / 2 < |t|
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ |X ω| ^ (n + 1) * rexp (z.re * X ω + t / 2 * |X ω|)) μ

Tactic:
refine 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
-- 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 (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ

Tactic:
h_subset (add_half_inf_sub_mem_Ioo hlu)

Premises used: Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.integrableExpSet, ProbabilityTheory.add_half_inf_sub_mem_Ioo
-- 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 (ω : Ω) ↦ rexp ((z.re + t) * X ω)) μ

Tactic:
exact h_subset (add_half_inf_sub_mem_Ioo hlu)

Premises used: ProbabilityTheory.add_half_inf_sub_mem_Ioo
-- 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 (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ

Tactic:
h_subset (sub_half_inf_sub_mem_Ioo hlu)

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo, Set.Mem, setOf, MeasureTheory.Integrable, ProbabilityTheory.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 (ω : Ω) ↦ rexp ((z.re - t) * X ω)) μ

Tactic:
exact h_subset (sub_half_inf_sub_mem_Ioo hlu)

Premises used: ProbabilityTheory.sub_half_inf_sub_mem_Ioo
-- 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
⊢ 0 ≤ t / 2

Tactic:
positivity
-- 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
⊢ t / 2 < t

Tactic:
simp [ht]
-- 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
⊢ t / 2 < |t|

Tactic:
exact lt_of_lt_of_le (by simp [ht]) (le_abs_self _)

Premises used: le_abs_self, lt_of_lt_of_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
⊢ ∀ᵐ (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

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_6 :
  ∀ (ω : Ω) (ε : ℂ) (hε : ε ∈ Metric.ball z (t / 2)),
    HasDerivAt (F := ℂ) (fun (x : ℂ) ↦ (fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ω)
      ((fun (z : ℂ) (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) ε ω) ε
⊢ ∀ᵐ (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

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_6 :
  HasDerivAt (fun (x : ℂ) ↦ (↑(X ω) : ℂ) ^ n * cexp (x * (↑(X ω) : ℂ)))
    ((↑(X ω) : ℂ) ^ n * ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ)))) ε
⊢ HasDerivAt (fun (x : ℂ) ↦ (↑(X ω) : ℂ) ^ n * cexp (x * (↑(X ω) : ℂ)))
    ((↑(X ω) : ℂ) ^ (n + 1) * cexp (ε * (↑(X ω) : ℂ))) ε

Tactic:
simp_rw [pow_succ, mul_assoc]

Premises used: pow_succ, mul_assoc
-- 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)
⊢ HasDerivAt (fun (x : ℂ) ↦ (↑(X ω) : ℂ) ^ n * cexp (x * (↑(X ω) : ℂ)))
    ((↑(X ω) : ℂ) ^ n * ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ)))) ε

Tactic:
HasDerivAt.const_mul _ ?_

Premises used: HasDerivAt.const_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)
refine_6 : HasDerivAt (fun (x : ℂ) ↦ cexp (x * (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ))) ε
⊢ HasDerivAt (fun (x : ℂ) ↦ (↑(X ω) : ℂ) ^ n * cexp (x * (↑(X ω) : ℂ)))
    ((↑(X ω) : ℂ) ^ n * ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ)))) ε

Tactic:
refine HasDerivAt.const_mul _ ?_

Premises used: HasDerivAt.const_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)
refine_6 :
  HasDerivAt (fun (x : ℂ) ↦ NormedSpace.exp (x • (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ))) ε
⊢ HasDerivAt (fun (x : ℂ) ↦ cexp (x * (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) * cexp (ε * (↑(X ω) : ℂ))) ε

Tactic:
simp_rw [← smul_eq_mul, Complex.exp_eq_exp_ℂ]

Premises used: Complex.exp_eq_exp_ℂ, smul_eq_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)
⊢ HasDerivAt (fun (u : ℂ) ↦ NormedSpace.exp (u • (↑(X ω) : ℂ))) (NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)) ε

Tactic:
hasDerivAt_exp_smul_const (X ω : ℂ) ε

Premises used: hasDerivAt_exp_smul_const, Complex.ofReal
-- 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)
h : (↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
⊢ HasDerivAt (fun (x : ℂ) ↦ NormedSpace.exp (x • (↑(X ω) : ℂ))) ((↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ))) ε

Tactic:
convert! hasDerivAt_exp_smul_const (X ω : ℂ) ε using 1

Premises used: hasDerivAt_exp_smul_const, Complex.ofReal
-- 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)
h : (↑(X ω) : ℂ) * NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
h₁ h₂ : NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)
⊢ (↑(X ω) : ℂ) • NormedSpace.exp (ε • (↑(X ω) : ℂ)) = NormedSpace.exp (ε • (↑(X ω) : ℂ)) * (↑(X ω) : ℂ)

Tactic:
rw [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (F := ℂ)
    (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1 * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
hasDerivAt_integral_pow_mul_exp hz 0

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h :
  ∀ (x : ℂ),
    complexMGF X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (x * (↑(X ω) : ℂ))) x_1 ∂μ
h₁ : ∀ (x x : Ω), (↑(X x) : ℂ) = (↑(X x) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
convert! hasDerivAt_integral_pow_mul_exp hz 0

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x : ℂ
⊢ complexMGF X μ x = ∫ (x_1 : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (↑(X ω) : ℂ) 0 * cexp (x * (↑(X ω) : ℂ))) x_1 ∂μ

Tactic:
simp [complexMGF]

Premises used: ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
x x_1 : Ω
⊢ (↑(X x_1) : ℂ) = (↑(X x_1) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1

Tactic:
simp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
⊢ HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
have h := hasDerivAt_complexMGF hz
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
h : HasDerivAt (complexMGF X μ) (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasFDerivAt (complexMGF X μ)
    (ContinuousLinearMap.toSpanSingleton ℂ (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)) z

Tactic:
rw [hasDerivAt_iff_hasFDerivAt] at h

Premises used: hasDerivAt_iff_hasFDerivAt
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
h :
  HasFDerivAt (complexMGF X μ)
    (ContinuousLinearMap.toSpanSingleton ℂ (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
h.hasFDerivWithinAt.differentiableWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z
h :
  HasFDerivAt (complexMGF X μ)
    (ContinuousLinearMap.toSpanSingleton ℂ (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)) z
⊢ DifferentiableWithinAt ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)} z

Tactic:
exact h.hasFDerivWithinAt.differentiableWithinAt

Premises used: HasFDerivAt.hasFDerivWithinAt, HasFDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
differentiableOn_complexMGF.analyticOnNhd (isOpen_interior.preimage Complex.continuous_re)

Premises used: isOpen_interior, Complex.continuous_re, ProbabilityTheory.differentiableOn_complexMGF, DifferentiableOn.analyticOnNhd, IsOpen.preimage
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ AnalyticOn ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
analyticOnNhd_complexMGF.analyticOn

Premises used: AnalyticOnNhd.analyticOn, ProbabilityTheory.analyticOnNhd_complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ AnalyticAt ℂ (complexMGF X μ) z

Tactic:
analyticOnNhd_complexMGF z hz

Premises used: ProbabilityTheory.analyticOnNhd_complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv 0 (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1 * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
simp [hasDerivAt_complexMGF hz]

Premises used: ProbabilityTheory.hasDerivAt_complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
succ :
  HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
rw [iteratedDeriv_succ]

Premises used: iteratedDeriv_succ
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)

Tactic:
IsOpen.eventually_mem ?_ hz

Premises used: Set.Mem, IsOpen.eventually_mem
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
refine : IsOpen (X := ℂ) fun (y : ℂ) ↦ interior (integrableExpSet X μ) y.re
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)

Tactic:
refine IsOpen.eventually_mem ?_ hz

Premises used: IsOpen.eventually_mem
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ interior (integrableExpSet X μ) y.re

Tactic:
isOpen_interior.preimage Complex.continuous_re

Premises used: Set.Mem, isOpen_interior, Complex.continuous_re, setOf, Set.sUnion, Set.preimage, interior, IsOpen.preimage
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ IsOpen (X := ℂ) fun (y : ℂ) ↦ interior (integrableExpSet X μ) y.re

Tactic:
exact isOpen_interior.preimage Complex.continuous_re

Premises used: isOpen_interior, Complex.continuous_re, IsOpen.preimage
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)

Tactic:
have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
y : ℂ
hy : y.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) y = ∫ (x : Ω), (↑(X x) : ℂ) ^ (n + 1) * cexp (y * (↑(X x) : ℂ)) ∂μ

Tactic:
HasDerivAt.deriv (hn hy)

Premises used: HasDerivAt.deriv
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
h_mem : ∀ᶠ (y : ℂ) in 𝓝 z, y.re ∈ interior (integrableExpSet X μ)
h :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (y : ℂ) ↦ y.re ∈ interior (integrableExpSet X μ)) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ |
              (fun (x : ℂ) ↦
                  deriv (iteratedDeriv n (complexMGF X μ)) x =
                    (fun (z : ℂ) ↦
                        (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ : ℂ))
                      x)
                x}
            x}
      a
h₁ h₂ :
  ∀ (y : ℂ) (hy : y.re ∈ interior (integrableExpSet X μ)),
    deriv (iteratedDeriv n (complexMGF X μ)) y = ∫ (x : Ω), (↑(X x) : ℂ) ^ (n + 1) * cexp (y * (↑(X x) : ℂ)) ∂μ
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ

Tactic:
filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ

Tactic:
have : deriv (iteratedDeriv n (complexMGF X μ))
        =ᶠ[𝓝 z] fun z ↦ μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] := by
      have h_mem : ∀ᶠ y in 𝓝 z, y.re ∈ interior (integrableExpSet X μ) := by
        refine IsOpen.eventually_mem ?_ hz
        exact isOpen_interior.preimage Complex.continuous_re
      filter_upwards [h_mem] with y hy using HasDerivAt.deriv (hn hy)
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv n (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
this :
  deriv (iteratedDeriv n (complexMGF X μ)) =ᶠ[𝓝 z] fun (z : ℂ) ↦
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ
succ :
  HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasDerivAt (deriv (iteratedDeriv n (complexMGF X μ)))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
rw [EventuallyEq.hasDerivAt_iff this]

Premises used: Filter.EventuallyEq.hasDerivAt_iff