awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_int : ∀ i_1 ∈ Insert.insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
insert : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ
⊢ Integrable (ε := ℝ) (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 : ℝ
inst : IsFiniteMeasure μ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ

Tactic:
IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec

Premises used: Finset.mem_insert_self, ProbabilityTheory.IndepFun.integrable_exp_mul_add
-- 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_int : ∀ i_1 ∈ Insert.insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
insert : X i ⟂ᵢ[μ] ∑ x ∈ s, X x
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * HAdd.hAdd (β := Ω → ℝ) (X i) (∑ x ∈ s, X x) ω)) μ

Tactic:
refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec

Premises used: Finset.mem_insert_self, ProbabilityTheory.IndepFun.integrable_exp_mul_add
-- 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_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ X i ⟂ᵢ[μ] ∑ x ∈ s, X x

Tactic:
(h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

Premises used: ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem, ProbabilityTheory.IndepFun.symm
-- 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_int : ∀ i_1 ∈ insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ
this : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
h_rec : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ s, X i) ω)) μ
⊢ X i ⟂ᵢ[μ] ∑ x ∈ s, X x

Tactic:
exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

Premises used: ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem, ProbabilityTheory.IndepFun.symm
-- 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)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
insert :
  ∀ (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.insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ Insert.insert i s, X i) ω)) μ
⊢ Integrable (ε := ℝ) (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 integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (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]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

Premises used: Finset.sum_apply, Insert.insert, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty, 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)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
empty :
  ∀ (h_int : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ ∅, X i) ω)) μ
insert :
  ∀ (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.insert i s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i_1 ω)) μ),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (∑ i ∈ Insert.insert i s, X i) ω)) μ
⊢ Integrable (ε := ℝ) (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 integrable_const _
  | insert i s hi_notin_s h_rec =>
    have : ∀ i : ι, i ∈ s → Integrable (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]
    refine IndepFun.integrable_exp_mul_add ?_ (h_int i (mem_insert_self _ _)) h_rec
    exact (h_indep.indepFun_finsetSum_of_notMem h_meas hi_notin_s).symm

Premises used: Finset.sum_apply, Insert.insert, MulZeroClass.mul_zero, Real.exp_zero, Finset.sum_empty, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
⊢ mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
⊢ ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ

Tactic:
have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
hi_notin_s : i ∉ s
h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t
h_int' : ∀ (i : ι), AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
insert : mgf (X i + ∑ x ∈ s, X x) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₁ : mgf (X i) μ t * mgf (∑ j ∈ s, X j) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₂ : mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
insert₃ insert₄ : mgf (X i) μ t * ∏ i ∈ s, mgf (X i) μ t = mgf (X i) μ t * ∏ x ∈ s, mgf (X x) μ t
⊢ mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t

Tactic:
rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

Premises used: Finset.prod_insert, ProbabilityTheory.iIndepFun.indepFun_finsetSum_of_notMem₀, ProbabilityTheory.aestronglyMeasurable_exp_mul_sum, ProbabilityTheory.IndepFun.mgf_add, Finset.sum_insert, ProbabilityTheory.IndepFun.symm
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
insert :
  ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s) (h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t),
    mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

Premises used: Insert.insert
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
this : IsProbabilityMeasure μ
empty : mgf (∑ i ∈ ∅, X i) μ t = ∏ i ∈ ∅, mgf (X i) μ t
insert :
  ∀ (i : ι) (s : Finset ι) (hi_notin_s : i ∉ s) (h_rec : mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t),
    mgf (∑ i ∈ Insert.insert i s, X i) μ t = ∏ i ∈ Insert.insert i s, mgf (X i) μ t
⊢ mgf (∑ i ∈ s, X i) μ t = ∏ i ∈ s, mgf (X i) μ t

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s hi_notin_s h_rec =>
    have h_int' : ∀ i : ι, AEStronglyMeasurable (fun ω : Ω => exp (t * X i ω)) μ := fun i =>
      ((h_meas i).const_mul t).exp.aestronglyMeasurable
    rw [sum_insert hi_notin_s,
      IndepFun.mgf_add (h_indep.indepFun_finsetSum_of_notMem₀ h_meas hi_notin_s).symm (h_int' i)
        (aestronglyMeasurable_exp_mul_sum fun i _ => h_int' i),
      h_rec, prod_insert hi_notin_s]

Premises used: Insert.insert
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
rw : log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
rw₁ : ∀ (j : ι) (hj : j ∈ s), mgf (X j) μ t ≠ 0
⊢ log (mgf (∑ i ∈ s, X i) μ t) = ∑ x ∈ s, log (mgf (X x) μ t)

Tactic:
rw [← log_prod fun j hj => ?_]

Premises used: Real.log_prod
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
rw rw₁ : log (∏ i ∈ s, mgf (X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)
⊢ log (mgf (∑ i ∈ s, X i) μ t) = log (∏ i ∈ s, mgf (X i) μ t)

Tactic:
rw [h_indep.mgf_sum₀ h_meas]

Premises used: ProbabilityTheory.iIndepFun.mgf_sum₀
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
(mgf_pos (h_int j hj)).ne'

Premises used: LT.lt.ne', ProbabilityTheory.mgf_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
this : IsProbabilityMeasure μ
j : ι
hj : j ∈ s
⊢ mgf (X j) μ t ≠ 0

Tactic:
exact (mgf_pos (h_int j hj)).ne'

Premises used: LT.lt.ne', ProbabilityTheory.mgf_pos
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
h_meas : ∀ (i : ι), Measurable (X i)
s : Finset ι
h_int : ∀ i ∈ s, Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X i ω)) μ
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
Ω' : Type u_3
m' : MeasurableSpace Ω'
μ' : Measure Ω'
X' : Ω' → ℝ
hident : IdentDistrib X X' μ μ'
t : ℝ
⊢ mgf X μ t = mgf X' μ' t

Tactic:
hident.comp (measurable_const_mul t).exp |>.integral_eq

Premises used: MeasurableMul.measurable_const_mul, Real.exp, ProbabilityTheory.IdentDistrib.integral_eq, ProbabilityTheory.mgf, ProbabilityTheory.IdentDistrib.comp, Measurable.exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
rw : ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s
⊢ mgf (∑ i ∈ s, X i) μ t = mgf (X j) μ t ^ #s

Tactic:
rw [h_indep.mgf_sum₀ h_meas]

Premises used: ProbabilityTheory.iIndepFun.mgf_sum₀
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s

Tactic:
Finset.prod_eq_pow_card fun i hi =>
    mgf_congr_of_identDistrib (X i) (X j) (hident i hi j hj) t

Premises used: Finset.prod_eq_pow_card, ProbabilityTheory.mgf_congr_of_identDistrib
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∏ i ∈ s, mgf (X i) μ t = mgf (X j) μ t ^ #s

Tactic:
exact Finset.prod_eq_pow_card fun i hi =>
    mgf_congr_of_identDistrib (X i) (X j) (hident i hi j hj) t

Premises used: Finset.prod_eq_pow_card, ProbabilityTheory.mgf_congr_of_identDistrib
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ι → Ω → ℝ
s : Finset ι
j : ι
h_meas : ∀ (i : ι), Measurable (X i)
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
hident : ∀ i ∈ s, ∀ j ∈ s, IdentDistrib (X i) (X j) μ μ
hj : j ∈ s
t : ℝ
⊢ ∀ (i : ι), AEMeasurable (X i) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
inl : ∀ (ht_zero_eq : 0 = t), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
inr : ∀ (ht_pos : 0 < t), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rcases ht.eq_or_lt with ht_zero_eq | ht_pos

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
inl : μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-0 * ε) * mgf X μ 0
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-t * ε) * mgf X μ t

Tactic:
rw [ht_zero_eq.symm]

Premises used: Eq.symm
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
inl : μ.real {ω : Ω | ε ≤ X ω} ≤ μ.real Set.univ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-0 * ε) * mgf X μ 0

Tactic:
simp only [neg_zero, zero_mul, exp_zero, mgf_zero', one_mul]

Premises used: MulZeroClass.zero_mul, ProbabilityTheory.mgf_zero', Real.exp_zero, neg_zero, one_mul
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
inl : autoParam (Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)) measureReal_mono._auto_1
inl₁ : Subset.{u_1} (α := Set Ω) {ω : Ω | ε ≤ X ω} Set.univ
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ μ.real Set.univ

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ autoParam (Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)) measureReal_mono._auto_1

Tactic:
measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ Subset.{u_1} (α := Set Ω) {ω : Ω | ε ≤ X ω} Set.univ

Tactic:
Set.subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_zero_eq : 0 = t
⊢ autoParam (Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)) measureReal_mono._auto_1

Tactic:
exacts [measure_ne_top _ _, Set.subset_univ _]

Premises used: Set.subset_univ, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
e_s :
  ∀ (ω : Ω),
    Membership.mem (γ := Set Ω) {ω : Ω | ε ≤ X ω} ω ↔
      Membership.mem (γ := Set Ω) {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ω
⊢ μ.real {ω : Ω | ε ≤ X ω} = μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)}

Tactic:
congr 1 with ω
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
e_s : ε ≤ X ω ↔ t * ε ≤ t * X ω
⊢ Membership.mem (γ := Set Ω) {ω : Ω | ε ≤ X ω} ω ↔
    Membership.mem (γ := Set Ω) {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ω

Tactic:
simp only [Set.mem_setOf_eq, exp_le_exp]

Premises used: Set.mem_setOf_eq, Real.exp_le_exp
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ε ≤ X ω ↔ t * ε ≤ t * X ω

Tactic:
⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩

Premises used: LT.lt.le, le_of_mul_le_mul_left, Iff.intro, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
ω : Ω
⊢ ε ≤ X ω ↔ t * ε ≤ t * X ω

Tactic:
exact ⟨fun h => mul_le_mul_of_nonneg_left h ht_pos.le,
        fun h => le_of_mul_le_mul_left h ht_pos⟩
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
⊢ rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ

Tactic:
have : exp (t * ε) * μ.real {ω | exp (t * ε) ≤ exp (t * X ω)} ≤
          μ[fun ω => exp (t * X ω)] :=
        mul_meas_ge_le_integral_of_nonneg (ae_of_all _ fun x => (exp_pos _).le) h_int _
-- Module: Mathlib.Probability.Moments.Basic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst : IsFiniteMeasure μ
ε : ℝ
ht : 0 ≤ t
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) μ
ht_pos : 0 < t
this : rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
rwa :
  μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) * (rexp (t * ε))⁻¹
rwa₁ : μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ) / rexp (t * ε)
rwa₂ rwa₃ rwa₄ rwa₅ :
  rexp (t * ε) * μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ
⊢ μ.real {ω : Ω | rexp (t * ε) ≤ rexp (t * X ω)} ≤ (rexp (t * ε))⁻¹ * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (t * X ω)) x ∂μ

Tactic:
rwa [mul_comm (exp (t * ε))⁻¹, ← div_eq_mul_inv, le_div_iff₀' (exp_pos _)]

Premises used: le_div_iff₀', HMul.hMul, Real.exp, div_eq_mul_inv, Inv.inv, mul_comm, Real.exp_pos