awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ 0 ≤ mgf Y μ t

Tactic:
mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ 0 ≤ mgf Y μ t

Tactic:
exact mgf_nonneg

Premises used: ProbabilityTheory.mgf_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf X μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
hX.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf X μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact hX.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf Y μ t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
hY.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ mgf Y μ t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact hY.mgf_le t

Premises used: ProbabilityTheory.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
rw :
  rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [← exp_add]

Premises used: Real.exp_add
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
e_x :
  (↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 =
    ((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ (↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 =
    ((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
ring
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
calc :
  mgf X μ t * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
calc₁ :
  rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (fun (ω : Ω) ↦ X ω + Y ω) μ t ≤ rexp ((↑(cX + cY) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
calc mgf (X + Y) μ t
    _ = mgf X μ t * mgf Y μ t :=
      hindep.mgf_add (hX.integrable_exp_mul t).1 (hY.integrable_exp_mul t).1
    _ ≤ exp (cX * t ^ 2 / 2) * exp (cY * t ^ 2 / 2) := by
      gcongr
      · exact mgf_nonneg
      · exact hX.mgf_le t
      · exact hY.mgf_le t
    _ = exp ((cX + cY) * t ^ 2 / 2) := by rw [← exp_add]; congr; ring

Premises used: ProbabilityTheory.HasSubgaussianMGF.integrable_exp_mul, HMul.hMul, HDiv.hDiv, Real.exp, HPow.hPow, And.left, HAdd.hAdd, ProbabilityTheory.mgf, ProbabilityTheory.IndepFun.mgf_add, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + -Y ω) (cX + cY) μ

Tactic:
hX.add_of_indepFun hY.neg hindep.neg_right

Premises used: ProbabilityTheory.HasSubgaussianMGF.neg, ProbabilityTheory.IndepFun.neg_right, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + -Y ω) (cX + cY) μ

Tactic:
exact hX.add_of_indepFun hY.neg hindep.neg_right

Premises used: ProbabilityTheory.HasSubgaussianMGF.neg, ProbabilityTheory.IndepFun.neg_right, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ IsProbabilityMeasure μ

Tactic:
have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
h_subG : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, c i) μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ Insert.insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
insert : HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Insert.insert i s, X i ω) (∑ i ∈ Insert.insert i s, c i) μ

Tactic:
simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]

Premises used: Finset.sum_apply, Pi.add_apply, Finset.sum_insert
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
⊢ X i ⟂ᵢ[μ] ∑ j ∈ s, X j

Tactic:
have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ

Tactic:
add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_

Premises used: Finset.mem_insert_self, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ Insert.insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
insert : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
insert₁ : X i ⟂ᵢ[μ] fun (ω : Ω) ↦ ∑ c ∈ s, X c ω
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ

Tactic:
refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_

Premises used: Finset.mem_insert_self, ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ

Tactic:
fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ

Tactic:
exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)

Premises used: Finset.mem_insert_of_mem
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
⊢ X i ⟂ᵢ[μ] ∑ j ∈ s, X j

Tactic:
h_indep'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
h₁ : ∀ (x : Ω), Eq (α := ℝ) (∑ c ∈ s, X c x) ((∑ j ∈ s, X j) x)
⊢ X i ⟂ᵢ[μ] fun (ω : Ω) ↦ ∑ c ∈ s, X c ω

Tactic:
convert! h_indep'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
i : ι
s : Finset ι
his : i ∉ s
h :
  ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
h_subG : ∀ i_1 ∈ insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ
h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
x : Ω
h₁ h₂ : Eq (α := ℝ) (∑ c ∈ s, X c x) (∑ c ∈ s, X c x)
⊢ Eq (α := ℝ) (∑ c ∈ s, X c x) ((∑ j ∈ s, X j) x)

Tactic:
rw [Finset.sum_apply]

Premises used: Finset.sum_apply
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : IsProbabilityMeasure μ
empty :
  ∀ (h_subG : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, c i) μ
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (h :
      ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ)
    (h_subG : ∀ i_1 ∈ Insert.insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Insert.insert i s, X i ω) (∑ i ∈ Insert.insert i s, c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h =>
    simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
    have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
    refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
    · exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)
    · convert! h_indep'
      rw [Finset.sum_apply]

Premises used: Finset.sum_apply, Insert.insert, Pi.add_apply
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : IsProbabilityMeasure μ
empty :
  ∀ (h_subG : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasSubgaussianMGF (X i) (c i) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, c i) μ
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (h :
      ∀ (h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ),
        HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ)
    (h_subG : ∀ i_1 ∈ Insert.insert i s, HasSubgaussianMGF (X i_1) (c i_1) μ),
    HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ Insert.insert i s, X i ω) (∑ i ∈ Insert.insert i s, c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h =>
    simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
    have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
    refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
    · exact fun i hi ↦ h_subG _ (Finset.mem_insert_of_mem hi)
    · convert! h_indep'
      rw [Finset.sum_apply]

Premises used: Finset.sum_apply, Insert.insert, Pi.add_apply
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
h_indep₁ : iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ
h_meas : ∀ (i : ↥s), AEMeasurable (X (↑i : ι)) μ
h_subG₁ : ∀ (i : ↥s), Membership.mem (γ := Finset ↥s) Finset.univ i → HasSubgaussianMGF (X (↑i : ι)) (c (↑i : ι)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i : ↥s, c (↑i : ι)) μ

Tactic:
apply sum_of_iIndepFun_of_forall_aemeasurable

Premises used: _private.0.ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun_of_forall_aemeasurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ

Tactic:
h_indep.precomp Subtype.val_injective

Premises used: Subtype.val_injective, ProbabilityTheory.iIndepFun.precomp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ

Tactic:
exact h_indep.precomp Subtype.val_injective

Premises used: Subtype.val_injective, ProbabilityTheory.iIndepFun.precomp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ (i : ↥s), AEMeasurable (X (↑i : ι)) μ

Tactic:
fun i ↦ (h_subG i i.2).aemeasurable

Premises used: ProbabilityTheory.HasSubgaussianMGF.aemeasurable, Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ (i : ↥s), AEMeasurable (X (↑i : ι)) μ

Tactic:
exact fun i ↦ (h_subG i i.2).aemeasurable
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ (i : ↥s), Membership.mem (γ := Finset ↥s) Finset.univ i → HasSubgaussianMGF (X (↑i : ι)) (c (↑i : ι)) μ

Tactic:
fun i _ ↦ h_subG i i.2

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ (i : ↥s), Membership.mem (γ := Finset ↥s) Finset.univ i → HasSubgaussianMGF (X (↑i : ι)) (c (↑i : ι)) μ

Tactic:
exact fun i _ ↦ h_subG i i.2
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i : ↥s, c (↑i : ι)) μ

Tactic:
have : HasSubgaussianMGF (fun ω ↦ ∑ (i : s), X i ω) (∑ (i : s), c i) μ := by
    apply sum_of_iIndepFun_of_forall_aemeasurable
    · exact h_indep.precomp Subtype.val_injective
    · exact fun i ↦ (h_subG i i.2).aemeasurable
    · exact fun i _ ↦ h_subG i i.2
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i : ↥s, c (↑i : ι)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i ∈ s, c i) μ

Tactic:
rw [Finset.sum_coe_sort] at this

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i ∈ s, c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
this.congr (ae_of_all _ fun ω ↦ Finset.sum_attach s (fun i ↦ X i ω))

Premises used: Finset.sum_attach, MeasureTheory.ae_of_all, ProbabilityTheory.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
this : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i ∈ s, c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ

Tactic:
exact this.congr (ae_of_all _ fun ω ↦ Finset.sum_attach s (fun i ↦ X i ω))

Premises used: Finset.sum_attach, MeasureTheory.ae_of_all, ProbabilityTheory.HasSubgaussianMGF.congr
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ι) ↦ ℝ) X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω : Ω | ε ≤ ∑ i ∈ s, X i ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑(∑ i ∈ s, c i) : ℝ)))

Tactic:
(sum_of_iIndepFun h_indep h_subG).measure_ge_le hε

Premises used: ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
⊢ ∀ i ∈ Finset.range n, HasSubgaussianMGF (X i) ((fun (x : ℕ) ↦ c) i) μ

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑(∑ i ∈ Finset.range n, c) : ℝ)))

Tactic:
have h := (sum_of_iIndepFun h_indep (c := fun _ ↦ c)
    (s := Finset.range n) (by simpa)).measure_ge_le hε
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
h_indep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X μ
c : ℝ≥0
n : ℕ
h_subG : ∀ i < n, HasSubgaussianMGF (X i) c μ
ε : ℝ
hε : 0 ≤ ε
h :
  μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑(∑ i ∈ Finset.range n, c) : ℝ)))
⊢ μ.real {ω : Ω | ε ≤ ∑ i ∈ Finset.range n, X i ω} ≤
    rexp (-HPow.hPow (β := ℕ) ε 2 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (↑c : ℝ)))

Tactic:
simpa [← mul_assoc] using h

Premises used: mul_assoc
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) cX μ
hY : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ) cY μ
hindep : X ⟂ᵢ[μ] Y
h_le : LE.le (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)
e_s :
  ∀ (ω : Ω),
    X ω ≤ Y ω ↔
      HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)
⊢ μ.real {ω : Ω | X ω ≤ Y ω} =
    μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}

Tactic:
congr with ω