awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∂μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
hasDerivAt_integral_pow_mul_exp hz (n + 1)

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, HAdd.hAdd, OfNat.ofNat
-- 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 ∂μ
⊢ HasDerivAt (F := ℂ) (fun (z : ℂ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ)
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

Premises used: ProbabilityTheory.hasDerivAt_integral_pow_mul_exp, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
zero :
  ∀ {z : ℂ} (hz : z.re ∈ interior (integrableExpSet X μ)),
    HasDerivAt (iteratedDeriv 0 (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ HAdd.hAdd (α := ℕ) 0 1 * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
succ :
  ∀ (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 μ)),
    HasDerivAt (iteratedDeriv (n + 1) (complexMGF X μ))
      (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1 + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z
⊢ HasDerivAt (iteratedDeriv n (complexMGF X μ))
    (∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ) z

Tactic:
induction n generalizing z with
  | zero => simp [hasDerivAt_complexMGF hz]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    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)
    rw [EventuallyEq.hasDerivAt_iff this]
    exact hasDerivAt_integral_pow_mul_exp hz (n + 1)

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

Tactic:
simp [complexMGF]

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

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 μ)),
    iteratedDeriv n (complexMGF X μ) z = ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ n * cexp (z * (↑(X ω) : ℂ))) x ∂μ
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (complexMGF X μ)) z =
    ∫ (x : Ω), (fun (ω : Ω) ↦ (↑(X ω) : ℂ) ^ (n + 1) * cexp (z * (↑(X ω) : ℂ))) x ∂μ

Tactic:
(hasDerivAt_iteratedDeriv_complexMGF hz n).deriv

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

Tactic:
exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv

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

Tactic:
induction n generalizing z with
  | zero => simp [complexMGF]
  | succ n hn =>
    rw [iteratedDeriv_succ]
    exact (hasDerivAt_iteratedDeriv_complexMGF hz n).deriv

Premises used: iteratedDeriv_succ, HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF, ProbabilityTheory.complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ t ∈ integrableExpSet Y μ'
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
ext t
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
pos :
  ∀ (hμ : μ = 0),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
neg :
  ∀ (hμ : ¬μ = 0),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'

Tactic:
simp [hμ, hμμ'.mp hμ]

Premises used: Iff.mp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
⊢ NeZero μ

Tactic:
have : NeZero μ := ⟨hμ⟩
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this : NeZero μ
⊢ NeZero μ'

Tactic:
have : NeZero μ' := ⟨(not_iff_not.mpr hμμ').mp hμ⟩
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
hμ : ¬μ = 0
this_1 : NeZero μ
this : NeZero μ'
neg : 0 < mgf X μ t ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'
neg₁ : 0 < mgf X μ t ↔ 0 < mgf Y μ' t
neg₂ neg₃ : 0 < mgf Y μ' t ↔ 0 < mgf Y μ' t
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ ↔ Integrable (ε := ℝ) (fun (ω : Ω') ↦ rexp (t * Y ω)) μ'

Tactic:
rw [← mgf_pos_iff, ← mgf_pos_iff, hXY]

Premises used: ProbabilityTheory.mgf_pos_iff
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
integrableExpSet_eq_of_mgf' hXY ?_

Premises used: ProbabilityTheory.integrableExpSet_eq_of_mgf'
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
refine : μ = 0 ↔ μ' = 0
⊢ integrableExpSet X μ = integrableExpSet Y μ'

Tactic:
refine integrableExpSet_eq_of_mgf' hXY ?_

Premises used: ProbabilityTheory.integrableExpSet_eq_of_mgf'
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
simp : ¬μ' = 0
⊢ μ = 0 ↔ μ' = 0

Tactic:
simp only [IsProbabilityMeasure.ne_zero, false_iff]

Premises used: false_iff, MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
this : mgf Y μ' 0 ≠ 0
h_contra : μ' = 0
⊢ False

Tactic:
simp [h_contra] at this
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
suffices : mgf Y μ' 0 ≠ 0
⊢ ¬μ' = 0

Tactic:
suffices mgf Y μ' 0 ≠ 0 by
    intro h_contra
    simp [h_contra] at this
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
rw : mgf X μ 0 ≠ 0
⊢ mgf Y μ' 0 ≠ 0

Tactic:
rw [← hXY]
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (0 * X ω)) μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsProbabilityMeasure μ
hXY : mgf X μ = mgf Y μ'
⊢ mgf X μ 0 ≠ 0

Tactic:
exact (mgf_pos (by simp)).ne'

Premises used: LT.lt.ne', ProbabilityTheory.mgf_pos
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
pos :
  ∀ (h_empty : interior (integrableExpSet X μ) = ∅),
    Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
neg :
  ∀ (h_empty : ¬interior (integrableExpSet X μ) = ∅),
    Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
by_cases h_empty : interior (integrableExpSet X μ) = ∅

Premises used: ProbabilityTheory.integrableExpSet, interior
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : interior (integrableExpSet X μ) = ∅
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
simp [h_empty]
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : ¬interior (integrableExpSet X μ) = ∅
⊢ (interior (integrableExpSet X μ)).Nonempty

Tactic:
rw [← ne_eq, ← Set.nonempty_iff_ne_empty] at h_empty

Premises used: ne_eq, Set.nonempty_iff_ne_empty
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
h_empty : (interior (integrableExpSet X μ)).Nonempty
neg :
  ∀ (t : ℝ) (ht : t ∈ interior (integrableExpSet X μ)),
    Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
obtain ⟨t, ht⟩ := h_empty
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
have hX : AnalyticOnNhd ℂ (complexMGF X μ) {z | z.re ∈ interior (integrableExpSet X μ)} :=
    analyticOnNhd_complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
⊢ AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}

Tactic:
have hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z | z.re ∈ interior (integrableExpSet Y μ')} :=
    analyticOnNhd_complexMGF
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
neg :
  ∀ (ht : t ∈ interior (integrableExpSet Y μ'))
    (hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')})
    (hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}),
    Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
rw [integrableExpSet_eq_of_mgf' hXY hμμ'] at hX ht ⊢

Premises used: ProbabilityTheory.integrableExpSet_eq_of_mgf'
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')} (↑t : ℂ)

Tactic:
simp [ht]
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
neg : ∃ᶠ (z : ℂ) in 𝓝[≠] (↑t : ℂ), complexMGF X μ z = complexMGF Y μ' z
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}

Tactic:
refine AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq hX hY
    (convex_integrableExpSet.interior.linear_preimage reLm).isPreconnected
    (z₀ := (t : ℂ)) (by simp [ht]) ?_

Premises used: Complex.reLm, AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq, Convex.interior, ProbabilityTheory.convex_integrableExpSet, Convex.isPreconnected, Convex.linear_preimage
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)

Tactic:
.of_forall fun y ↦ ?_

Premises used: Filter.Frequently.of_forall
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
refine : ∀ (y : ℝ), complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)

Tactic:
refine .of_forall fun y ↦ ?_
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
y : ℝ
rw : (↑(mgf X μ y) : ℂ) = complexMGF Y μ' (↑y : ℂ)
rw₁ : (↑(mgf X μ y) : ℂ) = (↑(mgf Y μ' y) : ℂ)
rw₂ rw₃ : (↑(mgf Y μ' y) : ℂ) = (↑(mgf Y μ' y) : ℂ)
⊢ complexMGF X μ (↑y : ℂ) = complexMGF Y μ' (↑y : ℂ)

Tactic:
rw [complexMGF_ofReal, complexMGF_ofReal, hXY]

Premises used: ProbabilityTheory.complexMGF_ofReal
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
⊢ ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)

Tactic:
have h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ x = complexMGF Y μ' x := by
    refine .of_forall fun y ↦ ?_
    rw [complexMGF_ofReal, complexMGF_ofReal, hXY]
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
h_real : ∃ᶠ (x : ℝ) in 𝓝[≠] t, complexMGF X μ (↑x : ℂ) = complexMGF Y μ' (↑x : ℂ)
neg :
  ∀
    (h_real :
      ∃ (ns : ℕ → ℝ),
        Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ (↑(ns n) : ℂ) = complexMGF Y μ' (↑(ns n) : ℂ)),
    ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] (↑t : ℂ), complexMGF X μ z = complexMGF Y μ' z

Tactic:
rw [frequently_iff_seq_forall] at h_real ⊢

Premises used: Filter.frequently_iff_seq_forall
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
h_real :
  ∃ (ns : ℕ → ℝ), Tendsto ns atTop (𝓝[≠] t) ∧ ∀ (n : ℕ), complexMGF X μ (↑(ns n) : ℂ) = complexMGF Y μ' (↑(ns n) : ℂ)
neg :
  ∀ (xs : ℕ → ℝ) (hx_tendsto : Tendsto xs atTop (𝓝[≠] t))
    (hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)),
    ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)
⊢ ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)

Tactic:
obtain ⟨xs, hx_tendsto, hx_eq⟩ := h_real
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
hXY : mgf X μ = mgf Y μ'
hμμ' : μ = 0 ↔ μ' = 0
t : ℝ
ht : t ∈ interior (integrableExpSet Y μ')
hX : AnalyticOnNhd ℂ (complexMGF X μ) {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
hY : AnalyticOnNhd ℂ (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet Y μ')}
xs : ℕ → ℝ
hx_tendsto : Tendsto xs atTop (𝓝[≠] t)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)

Tactic:
⟨fun n ↦ xs n, ?_, fun n ↦ ?_⟩

Premises used: Complex.ofReal, And.intro, Exists.intro