awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) : ℂ)
neg : Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝[≠] (↑t : ℂ))
neg₁ : ∀ (n : ℕ), complexMGF X μ ((fun (n : ℕ) ↦ (↑(xs n) : ℂ)) n) = complexMGF Y μ' ((fun (n : ℕ) ↦ (↑(xs n) : ℂ)) n)
⊢ ∃ (ns : ℕ → ℂ), Tendsto ns atTop (𝓝[≠] (↑t : ℂ)) ∧ ∀ (n : ℕ), complexMGF X μ (ns n) = complexMGF Y μ' (ns n)

Tactic:
refine ⟨fun n ↦ xs n, ?_, fun n ↦ ?_⟩
-- 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) : ℂ)
neg :
  ∀ (hx_tendsto : Tendsto xs atTop (𝓝 t) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n))
    (hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)),
    Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ)) ∧
      ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝[≠] (↑t : ℂ))

Tactic:
rw [tendsto_nhdsWithin_iff] at hx_tendsto ⊢

Premises used: tendsto_nhdsWithin_iff
-- 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) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
neg : Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ))
neg₁ : ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ)) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)

Tactic:
constructor
-- 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) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
neg : Tendsto xs atTop (𝓝 t)
⊢ Tendsto (fun (n : ℕ) ↦ (↑(xs n) : ℂ)) atTop (𝓝 (↑t : ℂ))

Tactic:
rw [tendsto_ofReal_iff]

Premises used: Filter.tendsto_ofReal_iff
-- 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) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ Tendsto xs atTop (𝓝 t)

Tactic:
hx_tendsto.1

Premises used: And.left
-- 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) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ Tendsto xs atTop (𝓝 t)

Tactic:
exact hx_tendsto.1

Premises used: And.left
-- 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) ∧ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) {t}ᶜ (xs n)
hx_eq : ∀ (n : ℕ), complexMGF X μ (↑(xs n) : ℂ) = complexMGF Y μ' (↑(xs n) : ℂ)
⊢ ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℂ) {(↑t : ℂ)}ᶜ (↑(xs n) : ℂ)

Tactic:
simpa using hx_tendsto.2

Premises used: And.right
-- 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) : ℂ)
n : ℕ
⊢ complexMGF X μ ((fun (n : ℕ) ↦ (↑(xs n) : ℂ)) n) = complexMGF Y μ' ((fun (n : ℕ) ↦ (↑(xs n) : ℂ)) n)

Tactic:
simp [hx_eq]
-- 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 μ'
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
eqOn_complexMGF_of_mgf' hXY ?_

Premises used: ProbabilityTheory.eqOn_complexMGF_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
⊢ Set.EqOn (complexMGF X μ) (complexMGF Y μ') {z : ℂ | z.re ∈ interior (integrableExpSet X μ)}

Tactic:
refine eqOn_complexMGF_of_mgf' hXY ?_

Premises used: ProbabilityTheory.eqOn_complexMGF_of_mgf'
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
⊢ ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)

Tactic:
have inner_ne_zero (x : ℝ) (h : x ≠ 0) : innerₗ ℝ x ≠ 0 :=
    DFunLike.ne_iff.mpr ⟨x, inner_self_ne_zero.mpr h⟩
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
apply :
  ∀ (w : ℝ),
    Eq (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
        (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
      (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
        (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
⊢ Eq (α := Measure ℝ) (Measure.map X μ) (Measure.map Y μ')

Tactic:
apply MeasureTheory.ext_of_integral_char_eq continuous_probChar probChar_ne_one inner_ne_zero
    continuous_inner (fun w ↦ ?_)

Premises used: Real.continuous_probChar, MeasureTheory.ext_of_integral_char_eq, continuous_inner, Real.probChar_ne_one
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
rw :
  ∀ (h : ∀ (x : ℂ), complexMGF X μ x = complexMGF Y μ' x)
    (inner_ne_zero :
      ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ))
    (w : ℝ),
    Eq (α := ℂ)
      (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
        (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
      (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
        (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)

Tactic:
rw [funext_iff] at h

Premises used: funext_iff
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : ∀ (x : ℂ), complexMGF X μ x = complexMGF Y μ' x
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
⊢ complexMGF X μ ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I) =
    complexMGF Y μ' ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I)

Tactic:
specialize h (Multiplicative.toAdd w * I)

Premises used: HMul.hMul, Complex.ofReal, Multiplicative.toAdd, DFunLike.coe, Complex.I
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  complexMGF X μ ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I) =
    complexMGF Y μ' ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * I)
⊢ Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')

Tactic:
simp_rw [complexMGF, mul_assoc, mul_comm I, ← mul_assoc] at h

Premises used: mul_assoc, mul_comm, ProbabilityTheory.complexMGF, Complex.I
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
simp :
  Eq (α := ℂ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦
      (BoundedContinuousFunction.char (L := innerₗ ℝ) continuous_probChar ⋯ w : (a : ℝ) → ℂ) v)

Tactic:
simp only [BoundedContinuousFunction.char_apply, innerₗ_apply_apply,
    RCLike.inner_apply, conj_trivial, probChar_apply, ofReal_mul]

Premises used: conj_trivial, RCLike.inner_apply, innerₗ_apply_apply, Real.probChar_apply, Complex.ofReal_mul, BoundedContinuousFunction.char_apply
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (Measure.map X μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
⊢ AEStronglyMeasurable (β := ℂ) (m₀ := Real.measurableSpace) (fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (Measure.map Y μ')

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero :
  ∀ (x : ℝ) (h : x ≠ 0), Ne (α := ℝ →ₗ[ℝ] ℝ) ((innerₗ ℝ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) x : ℝ →ₗ[ℝ] ℝ) (0 : ℝ →ₗ[ℝ] ℝ)
w : ℝ
h :
  Eq (α := ℂ) (∫ (ω : Ω), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(X ω) : ℂ) * I) ∂μ)
    (∫ (ω : Ω'), cexp ((↑((Multiplicative.toAdd : (a : Multiplicative ℝ) → ℝ) w) : ℂ) * (↑(Y ω) : ℂ) * I) ∂μ')
rwa :
  Eq (α := ℂ) (∫ (x : Ω), cexp ((↑w : ℂ) * (↑(X x) : ℂ) * I) ∂μ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
rwa₁ rwa₂ rwa₃ rwa₄ :
  Eq (α := ℂ) (∫ (x : Ω), cexp ((↑w : ℂ) * (↑(X x) : ℂ) * I) ∂μ) (∫ (x : Ω'), cexp ((↑w : ℂ) * (↑(Y x) : ℂ) * I) ∂μ')
⊢ Eq (α := ℂ) (@integral _ _ _ _ Real.measurableSpace (Measure.map X μ) fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))
    (@integral _ _ _ _ Real.measurableSpace (Measure.map Y μ') fun (v : ℝ) ↦ cexp ((↑w : ℂ) * (↑v : ℂ) * I))

Tactic:
rwa [integral_map hX (by fun_prop), integral_map hY (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Moments.ComplexMGF
Goal:
μ μ' : Measure ℝ
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure μ'
h : complexMGF id μ = complexMGF id μ'
⊢ μ = μ'

Tactic:
simpa using Measure.ext_of_complexMGF_eq aemeasurable_id aemeasurable_id h

Premises used: MeasureTheory.Measure.ext_of_complexMGF_eq, aemeasurable_id
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
simp_rw :
  ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ cov[X, Y; μ] = ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
simp_rw [covariance, sub_mul, mul_sub]

Premises used: mul_sub, sub_mul, ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
hg :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
rw [integral_sub]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a - X a * ∫ (x : Ω), Y x ∂μ ∂μ)
      (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
rw [integral_sub]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      ∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
rw [integral_sub]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
repeat :
  HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
hf : Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ
hg : Integrable (ε := ℝ) (fun (a : Ω) ↦ HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
hf₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * Y a) μ
hg₁ : Integrable (ε := ℝ) (fun (a : Ω) ↦ X a * ∫ (x : Ω), Y x ∂μ) μ
hf₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ) μ
hg₂ :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) μ
⊢ ∫ (ω : Ω),
      X ω * Y ω - X ω * ∫ (x : Ω), Y x ∂μ -
        ((∫ (x : Ω), X x ∂μ) * Y ω - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) ∂μ =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
repeat rw [integral_sub]

Premises used: MeasureTheory.integral_sub
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
simp_rw :
  ∫ (a : Ω), X a * Y a ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
      (HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
        HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ HSub.hSub (α := ℝ) (∫ (a : Ω), X a * Y a ∂μ) (∫ (a : Ω), X a * ∫ (x : Ω), Y x ∂μ ∂μ) -
      HSub.hSub (α := ℝ) (∫ (a : Ω), (∫ (x : Ω), X x ∂μ) * Y a ∂μ)
        (∫ (a : Ω), HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ∂μ) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
simp_rw [integral_mul_const, integral_const_mul, integral_const, probReal_univ,
       one_smul]

Premises used: MeasureTheory.integral_const_mul, one_smul, MeasureTheory.integral_const, MeasureTheory.probReal_univ, MeasureTheory.integral_mul_const
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ ∫ (a : Ω), X a * Y a ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
      (HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ) -
        HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)) =
    ∫ (x : Ω), (X * Y) x ∂μ - HMul.hMul (α := ℝ) (∫ (a : Ω), X a ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ LE.le (α := ENNReal) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Covariance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ (∫ (x : Ω), X x ∂μ) * Y a) μ

Tactic:
exact hY.const_mul _ |>.integrable (by simp)

Premises used: MeasureTheory.MemLp.const_mul, MeasureTheory.MemLp.integrable