awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
⊢ mgf (X ∘ Y) μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : mgf (X ∘ Y) μ t = mgf (m := mΩ) X (Measure.map Y μ) t
Tactic: convert! h.mgf_le t using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF (mΩ := mΩ) X c (Measure.map Y μ)
t : ℝ
⊢ mgf (X ∘ Y) μ t = mgf (m := mΩ) X (Measure.map Y μ) t
have h₁ : mgf (X ∘ Y) μ t = mgf (X ∘ Y) μ t
Tactic: rw [mgf_map hY (h.integrable_exp_mul t).1]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ
have refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)), HasSubgaussianMGF X c μ
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, fun t ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)), HasSubgaussianMGF X c μ
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ
have refine_2 : ∀ (h : HasSubgaussianMGF X c μ) (t : ℝ),
  @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, fun t ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
refine_1 : ∀ (h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)), HasSubgaussianMGF X c μ
refine_2 :
  ∀ (h : HasSubgaussianMGF X c μ) (t : ℝ),
    @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
⊢ HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ) ↔ HasSubgaussianMGF X c μ
have refine_3 : ∀ (h : HasSubgaussianMGF X c μ) (t : ℝ),
  mgf (m := measurableSpace) id (Measure.map X μ) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ⟨fun t ↦ ?_, fun t ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
⊢ HasSubgaussianMGF X c μ
have refine_1 : HasSubgaussianMGF (id ∘ X) c μ
Tactic: rw [← Function.id_comp X]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (ω : ℝ) ↦ rexp (t * id ω)) (Measure.map X μ)
have refine_2 : Integrable (ε := ℝ) ((fun (ω : ℝ) ↦ rexp (t * id ω)) ∘ X) μ
Tactic: rw [integrable_map_measure (by fun_prop) hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf (m := measurableSpace) id (Measure.map X μ) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have refine_3 : mgf X μ t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [mgf_id_map hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF X c μ
hXY : IdentDistrib X Y μ μ'
⊢ HasSubgaussianMGF Y c μ'
have hX₁ : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
Tactic: rw [← id_map_iff hXY.aemeasurable_fst] at hX
Cleared hypotheses: hX, hXY
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ' : Measure Ω'
Y : Ω' → ℝ
hX : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map X μ)
hXY : IdentDistrib X Y μ μ'
⊢ HasSubgaussianMGF Y c μ'
have rwa : HasSubgaussianMGF (mΩ := measurableSpace) id c (Measure.map Y μ')
Tactic: rwa [← id_map_iff hXY.aemeasurable_snd, ← hXY.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω)) (μ.trim hm)
have refine : StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)
Tactic: refine (hX.integrable_exp_mul t).trim hm ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
⊢ mgf X (μ.trim hm) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have rw : ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [mgf, ← integral_trim]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hm : m ≤ mΩ
hXm : Measurable X
hX : HasSubgaussianMGF X c μ
t : ℝ
rw : ∫ (x : Ω), rexp (t * X x) ∂μ ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X (μ.trim hm) t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have hf : StronglyMeasurable (β := ℝ) fun (ω : Ω) ↦ rexp (t * X ω)
Tactic: rw [mgf, ← integral_trim]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
r : ℝ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ r * X ω) (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) ⋯ * c) μ
have rw : ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ()))
  (r : ℝ),
  Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ r * X ω)
    (Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) (HPow.hPow (β := ℕ) r 2) sorry * c) (Kernel.const Unit μ) (Measure.dirac ())
Tactic: rw [HasSubgaussianMGF_iff_kernel] at h ⊢
Cleared hypotheses: h, r
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : HasSubgaussianMGF X c μ
⊢ integrableExpSet X μ = Set.univ
have h : ∀ (t : ℝ), t ∈ integrableExpSet X μ ↔ Membership.mem (γ := Set ℝ) Set.univ t
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
ε : ℝ
hε : 0 ≤ ε
⊢ μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
have rw : ∀ (h : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) X c (Kernel.const Unit μ) (Measure.dirac ())) {ε : ℝ}
  (hε : 0 ≤ ε), μ.real {ω : Ω | ε ≤ X ω} ≤ rexp (-HPow.hPow (β := ℕ) ε 2 / (2 * (↑c : ℝ)))
Tactic: rw [HasSubgaussianMGF_iff_kernel] at h
Cleared hypotheses: h, ε, hε
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X ω + Y ω)
    (HPow.hPow (β := ℕ)
      (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
        ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
      2)
    μ
have this : Kernel.HasSubgaussianMGF (mΩ' := PUnit.instMeasurableSpace) (fun (ω : Ω) ↦ X ω + Y ω)
  (HPow.hPow (β := ℕ)
    (HAdd.hAdd (α := ℝ≥0) (β := ℝ≥0) ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cX : ℝ≥0)
      ((NNReal.sqrt : (a : ℝ≥0) → ℝ≥0) cY : ℝ≥0))
    2)
  (Kernel.const Unit μ) (Measure.dirac ())
Tactic: have := (HasSubgaussianMGF_iff_kernel.1 hX).add (HasSubgaussianMGF_iff_kernel.1 hY)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * (X ω + Y ω))) μ
have simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
Tactic: simp_rw [mul_add, exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (t * X ω) * rexp (t * Y ω)) μ
have convert! : (↑2 : ℝ≥0∞).HolderTriple (↑2 : ℝ≥0∞) 1
Tactic: convert! MemLp.integrable_mul (hX.memLp_exp_mul t 2) (hY.memLp_exp_mul t 2)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have c0 : 0 ≤ mgf Y μ t
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
c0 : 0 ≤ mgf Y μ t
⊢ mgf X μ t * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₁ : mgf X μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
c0 : 0 ≤ mgf Y μ t
h₁ : mgf X μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X μ t * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h₂ : mgf Y μ t ≤ rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)
have rw : rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
  rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [← exp_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX μ
hY : HasSubgaussianMGF Y cY μ
hindep : X ⟂ᵢ[μ] Y
t : ℝ
⊢ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
    rexp (((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2)
have e_x : (↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 + (↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 =
  ((↑cX : ℝ) + (↑cY : ℝ)) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 (fun (ω : Ω) ↦ X ω + Y ω) μ t ≤ rexp ((↑(cX + cY) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have calc : mgf X μ t * mgf Y μ t ≤ rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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)
⊢ mgf (fun (ω : Ω) ↦ X ω + Y ω) μ t ≤ rexp ((↑(cX + cY) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have calc₁ : rexp ((↑cX : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * rexp ((↑cY : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) =
  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
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have this : IsProbabilityMeasure μ
Tactic: have : IsProbabilityMeasure μ := h_indep.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ insert i s, X i ω) (∑ i ∈ insert i s, c i) μ
have insert : HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ
Tactic: simp_rw [← Finset.sum_apply, Finset.sum_insert his, Pi.add_apply, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ
have h_indep' : X i ⟂ᵢ[μ] ∑ j ∈ s, X j
Tactic: have h_indep' := (h_indep.indepFun_finsetSum_of_notMem₀ h_meas his).symm
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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) μ
have insert : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
Tactic: refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ X i ω + ∑ c ∈ s, X c ω) (c i + ∑ i ∈ s, c i) μ
have insert₁ : X i ⟂ᵢ[μ] fun (ω : Ω) ↦ ∑ c ∈ s, X c ω
Tactic: refine add_of_indepFun (h_subG _ (Finset.mem_insert_self _ _)) (h ?_) ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ⟂ᵢ[μ] fun (ω : Ω) ↦ ∑ c ∈ s, X c ω
have h₁ : ∀ (x : Ω), Eq (α := ℝ) (∑ c ∈ s, X c x) ((∑ j ∈ s, X j) x)
Tactic: convert! h_indep'
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 : Ω
⊢ Eq (α := ℝ) (∑ c ∈ s, X c x) ((∑ j ∈ s, X j) x)
have h₁ : Eq (α := ℝ) (∑ c ∈ s, X c x) (∑ c ∈ s, X c x)
Tactic: rw [Finset.sum_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have empty : ∀ (h_subG : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasSubgaussianMGF (X i) (c i) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, 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]
Cleared hypotheses: s, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have 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 i s, HasSubgaussianMGF (X i_1) (c i_1) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ insert i s, X i ω) (∑ i ∈ insert 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]
Cleared hypotheses: s, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have empty : ∀ (h_subG : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → HasSubgaussianMGF (X i) (c i) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, 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]
Cleared hypotheses: s, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have 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 i s, HasSubgaussianMGF (X i_1) (c i_1) μ),
  HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ insert i s, X i ω) (∑ i ∈ insert 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]
Cleared hypotheses: s, h_subG
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 : ι)) μ
have h_indep₁ : iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ
Tactic: apply sum_of_iIndepFun_of_forall_aemeasurable