awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
pos : (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) fun (ω : Ω) ↦ rexp (t * X ω)
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
refine integral_mono_ae htY htX ?_

Premises used: MeasureTheory.integral_mono_ae
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
ω : Ω
hω : X ω ≤ Y ω
⊢ rexp (t * Y ω) ≤ rexp (t * X ω)

Tactic:
exp_monotone <| mul_le_mul_of_nonpos_left hω ht

Premises used: mul_le_mul_of_nonpos_left, Real.exp_monotone
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x ≤ Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦ LE.le (α := ℝ) ((fun (ω : Ω) ↦ rexp (t * Y ω)) x) ((fun (ω : Ω) ↦ rexp (t * X ω)) x)) x}
            x}
      a
h₁ h₂ : ∀ (ω : Ω) (hω : X ω ≤ Y ω), rexp (t * Y ω) ≤ rexp (t * X ω)
⊢ (ae μ).EventuallyLE (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) fun (ω : Ω) ↦ rexp (t * X ω)

Tactic:
filter_upwards [hXY] with ω hω using exp_monotone <| mul_le_mul_of_nonpos_left hω ht

Premises used: Real.exp_monotone
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
neg : 0 ≤ mgf X μ t
⊢ mgf Y μ t ≤ mgf X μ t

Tactic:
rw [mgf_undef htY]

Premises used: ProbabilityTheory.mgf_undef
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t

Tactic:
mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
Y : Ω → ℝ
hXY : X ≤ᶠ[ae μ] Y
ht : t ≤ 0
htX : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
htY : ¬Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ 0 ≤ mgf X μ t

Tactic:
exact mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
⊢ ∀ (t : ℝ), Measurable (β := ℝ) fun (x : ℝ) ↦ rexp (t * x)

Tactic:
have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable (β := ℝ) fun (x : ℝ) ↦ rexp (t * x)
⊢ ((fun (x : ℝ) ↦ rexp (s * x)) ∘ X) ⟂ᵢ[μ] (fun (x : ℝ) ↦ rexp (t * x)) ∘ Y

Tactic:
IndepFun.comp h_indep (h_meas s) (h_meas t)

Premises used: ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable (β := ℝ) fun (x : ℝ) ↦ rexp (t * x)
⊢ ((fun (x : ℝ) ↦ rexp (s * x)) ∘ X) ⟂ᵢ[μ] (fun (x : ℝ) ↦ rexp (t * x)) ∘ Y

Tactic:
exact IndepFun.comp h_indep (h_meas s) (h_meas t)

Premises used: ProbabilityTheory.IndepFun.comp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
simp_rw :
  ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ =
    HMul.hMul (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * Y x) ∂μ)
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
simp_rw [mgf, Pi.add_apply, mul_add, exp_add]

Premises used: Pi.add_apply, mul_add, ProbabilityTheory.mgf, Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ =
    HMul.hMul (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * Y x) ∂μ)

Tactic:
(h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY

Premises used: ProbabilityTheory.IndepFun.exp_mul, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
hY : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ ∫ (x : Ω), rexp (t * X x) * rexp (t * Y x) ∂μ =
    HMul.hMul (α := ℝ) (∫ (x : Ω), rexp (t * X x) ∂μ) (∫ (x : Ω), rexp (t * Y x) ∂μ)

Tactic:
exact (h_indep.exp_mul t t).integral_mul_eq_mul_integral hX hY

Premises used: ProbabilityTheory.IndepFun.exp_mul, ProbabilityTheory.IndepFun.integral_mul_eq_mul_integral
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)

Tactic:
have A : Continuous fun x : ℝ => exp (t * x) := by fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ

Tactic:
have h'X : AEStronglyMeasurable (fun ω => exp (t * X ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hX.aemeasurable
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
h'X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ

Tactic:
have h'Y : AEStronglyMeasurable (fun ω => exp (t * Y ω)) μ :=
    A.aestronglyMeasurable.comp_aemeasurable hY.aemeasurable
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
h'X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h'Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
h_indep.mgf_add h'X h'Y

Premises used: ProbabilityTheory.IndepFun.mgf_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
hX : AEStronglyMeasurable X μ
hY : AEStronglyMeasurable Y μ
A : Continuous (Y := ℝ) fun (x : ℝ) ↦ rexp (t * x)
h'X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h'Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ mgf (X + Y) μ t = mgf X μ t * mgf Y μ t

Tactic:
exact h_indep.mgf_add h'X h'Y

Premises used: ProbabilityTheory.IndepFun.mgf_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
pos : ∀ (hμ : μ = 0), cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
neg : ∀ (hμ : ¬μ = 0), cgf (X + Y) μ t = cgf X μ t + cgf Y μ t
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
hμ : μ = 0
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
neg : log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)
⊢ cgf (X + Y) μ t = cgf X μ t + cgf Y μ t

Tactic:
simp only [cgf, h_indep.mgf_add h_int_X.aestronglyMeasurable h_int_Y.aestronglyMeasurable]

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, ProbabilityTheory.cgf, ProbabilityTheory.IndepFun.mgf_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)

Tactic:
log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne'

Premises used: ProbabilityTheory.mgf_pos', LT.lt.ne', Real.log_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
hμ : ¬μ = 0
⊢ log (mgf X μ t * mgf Y μ t) = log (mgf X μ t) + log (mgf Y μ t)

Tactic:
exact log_mul (mgf_pos' hμ h_int_X).ne' (mgf_pos' hμ h_int_Y).ne'

Premises used: ProbabilityTheory.mgf_pos', LT.lt.ne', Real.log_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
simp_rw : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Premises used: Pi.add_apply, mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
AEStronglyMeasurable.mul h_int_X h_int_Y

Premises used: MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_int_X : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
exact AEStronglyMeasurable.mul h_int_X h_int_Y

Premises used: MeasureTheory.AEStronglyMeasurable.mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ 1) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
simp only [sum_apply, sum_empty, mul_zero, exp_zero]

Premises used: Finset.sum_apply, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ 1) μ

Tactic:
aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ 1) μ

Tactic:
exact aestronglyMeasurable_const

Premises used: MeasureTheory.aestronglyMeasurable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
⊢ ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ

Tactic:
have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ

Tactic:
specialize h_rec this
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ Insert.insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
insert : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ Insert.insert i s, X i) ω)) μ

Tactic:
rw [sum_insert hi_notin_s]

Premises used: Finset.sum_insert
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ

Tactic:
apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec

Premises used: Finset.mem_insert_self, ProbabilityTheory.aestronglyMeasurable_exp_mul_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀
    (h_int :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
insert :
  ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
    (h_rec :
      ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
        AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
    (h_int : ∀ i_1 ∈ Insert.insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ Insert.insert i s, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ

Tactic:
induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec

Premises used: MeasureTheory.aestronglyMeasurable_const, Finset.sum_apply, Insert.insert, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
s : Finset ι
h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀
    (h_int :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
insert :
  ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s)
    (h_rec :
      ∀ (h_int : ∀ i ∈ s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
        AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ)
    (h_int : ∀ i_1 ∈ Insert.insert i s, AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
    AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ Insert.insert i s, X i) ω)) μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty =>
    simp only [sum_apply, sum_empty, mul_zero, exp_zero]
    exact aestronglyMeasurable_const
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
    specialize h_rec this
    rw [sum_insert hi_notin_s]
    apply aestronglyMeasurable_exp_mul_add (h_int i (mem_insert_self _ _)) h_rec

Premises used: MeasureTheory.aestronglyMeasurable_const, Finset.sum_apply, Insert.insert, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (X + Y) ω)) μ

Tactic:
simp_rw [Pi.add_apply, mul_add, exp_add]

Premises used: Pi.add_apply, mul_add, Real.exp_add
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
(h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

Premises used: ProbabilityTheory.IndepFun.integrable_mul, ProbabilityTheory.IndepFun.exp_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
h_int_X : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
h_int_Y : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * Y ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ

Tactic:
exact (h_indep.exp_mul t t).integrable_mul h_int_X h_int_Y

Premises used: ProbabilityTheory.IndepFun.integrable_mul, ProbabilityTheory.IndepFun.exp_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 1) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ

Tactic:
simp only [sum_apply, sum_empty, mul_zero, exp_zero]

Premises used: Finset.sum_apply, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 1) μ

Tactic:
integrable_const _

Premises used: MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 1) μ

Tactic:
exact integrable_const _

Premises used: MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
⊢ ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ

Tactic:
have : ∀ i : ι, i ∈ s → Integrable (fun ω : Ω => exp (t * X i ω)) μ := fun i hi =>
      h_int i (mem_insert_of_mem hi)
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec :
  ∀ (h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ

Tactic:
specialize h_rec this