awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) μ
h_indep₁ : iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i : ↥s, c (↑i : ι)) μ
have h_meas : ∀ (i : ↥s), AEMeasurable (X (↑i : ι)) μ
Tactic: apply sum_of_iIndepFun_of_forall_aemeasurable
-- 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) μ
h_indep₁ : iIndepFun (β := fun (x : ↥s) ↦ ℝ) (fun (i : ↥s) ↦ X (↑i : ι)) μ
h_meas : ∀ (i : ↥s), AEMeasurable (X (↑i : ι)) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i : ↥s, c (↑i : ι)) μ
have h_subG₁ : ∀ (i : ↥s), Membership.mem (γ := Finset ↥s) Finset.univ i → HasSubgaussianMGF (X (↑i : ι)) (c (↑i : ι)) μ
Tactic: apply sum_of_iIndepFun_of_forall_aemeasurable
-- 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
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
have this : 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
-- 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
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) μ
have this₁ : HasSubgaussianMGF (fun (ω : Ω) ↦ ∑ i : ↥s, X (↑i : ι) ω) (∑ i ∈ s, c i) μ
Tactic: rw [Finset.sum_coe_sort] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
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 / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) * (↑c : ℝ)))
have h : μ.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ε
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
⊢ μ.real {ω : Ω | X ω ≤ Y ω} =
    μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}
have e_s : ∀ (ω : Ω),
  X ω ≤ Y ω ↔
    HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
⊢ μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)} ≤
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have refine_1 : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ
Tactic: refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
refine_1 : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ
⊢ μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)} ≤
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have refine_2 : 0 ≤ HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
Tactic: refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
refine_1 : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ
refine_2 : 0 ≤ HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)
⊢ μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)} ≤
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have refine_3 : rexp (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) 2 / (2 * (↑(cX + cY) : ℝ))) =
  rexp
    (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 / (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
Tactic: refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ
have refine_1 : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ
Tactic: rw [add_comm cX]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ
have refine_1 : (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ) ⟂ᵢ[μ] fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ
Tactic: refine sub_of_indepFun hY hX ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
⊢ rexp (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) 2 / (2 * (↑(cX + cY) : ℝ))) =
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have refine_3 : -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) 2 =
  -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2
Tactic: congr 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 (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 ∂μ)
⊢ μ.real {ω : Ω | X ω ≤ Y ω} ≤
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have calc : μ.real {ω : Ω | X ω ≤ Y ω} =
  μ.real
    {ω : Ω |
      HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}
Tactic: calc μ.real {ω | X ω ≤ Y ω}
  _ = μ.real {ω | (μ[X] - μ[Y]) ≤ (Y ω - μ[Y]) - (X ω - μ[X])} := by
    congr with ω
    grind
  _ ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by
    refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
    · rw [add_comm cX]
      refine sub_of_indepFun hY hX ?_
      exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X])
        (by fun_prop) (by fun_prop)
    · grind
    · congr 2
      grind
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
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 ∂μ)
calc :
  μ.real {ω : Ω | X ω ≤ Y ω} =
    μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}
⊢ μ.real {ω : Ω | X ω ≤ Y ω} ≤
    rexp
      (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 /
        (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
have calc₁ : μ.real
    {ω : Ω |
      HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
        Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)} ≤
  rexp
    (-HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2 / (2 * ((↑cX : ℝ) + (↑cY : ℝ))))
Tactic: calc μ.real {ω | X ω ≤ Y ω}
  _ = μ.real {ω | (μ[X] - μ[Y]) ≤ (Y ω - μ[Y]) - (X ω - μ[X])} := by
    congr with ω
    grind
  _ ≤ Real.exp (- (μ[Y] - μ[X]) ^ 2 / (2 * (cX + cY))) := by
    refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_
    · rw [add_comm cX]
      refine sub_of_indepFun hY hX ?_
      exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X])
        (by fun_prop) (by fun_prop)
    · grind
    · congr 2
      grind
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
⊢ mgf X μ t ≤ rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
have hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
Tactic: have hi (u : ℝ) : Integrable (fun ω ↦ exp (u * X ω)) μ := integrable_exp_mul_of_mem_Icc hm hb
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
⊢ mgf X μ t ≤ rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
have hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
Tactic: have hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ) := by simp [hi, integrableExpSet]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
⊢ mgf X μ t ≤ rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
have obtain : ∀ (u : ℝ) (h1 : u ∈ Set.Ioo 0 t) (h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2),
  mgf X μ t ≤ rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: obtain ⟨u, h1, h2⟩ := exists_cgf_eq_iteratedDeriv_two_cgf_mul ht hc hs
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ mgf X μ t ≤ rexp (HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2)
have rw : iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2 ≤
  HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [← exp_cgf (hi t), exp_le_exp, h2]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2 ≤
    HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2
have hab : iteratedDeriv 2 (cgf X μ) u ≤ HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
have rw : Var[X; μ.tilted fun (x : Ω) ↦ u * X x] = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
Tactic: rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ Var[X; μ.tilted fun (x : Ω) ↦ u * X x] ≤ HPow.hPow (β := ℕ) ((b - a) / 2) 2
have convert_1 : IsProbabilityMeasure (μ.tilted fun (x : Ω) ↦ u * X x)
Tactic: convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
convert_1 : IsProbabilityMeasure (μ.tilted fun (x : Ω) ↦ u * X x)
⊢ Var[X; μ.tilted fun (x : Ω) ↦ u * X x] ≤ HPow.hPow (β := ℕ) ((b - a) / 2) 2
have convert_2 : AEMeasurable X (μ.tilted fun (x : Ω) ↦ u * X x)
Tactic: convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
⊢ iteratedDeriv 2 (cgf X μ) u ≤ HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
have _ : iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
Tactic: calc
  _ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
_ : iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
⊢ iteratedDeriv 2 (cgf X μ) u ≤ HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
have _₁ : Var[X; μ.tilted fun (x : Ω) ↦ u * X x] ≤ HPow.hPow (β := ℕ) ((b - a) / 2) 2
Tactic: calc
  _ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b t : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
ht : 0 < t
hi : ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
u : ℝ
h1 : u ∈ Set.Ioo 0 t
h2 : cgf X μ t = iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2
_ : iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
_₁ : Var[X; μ.tilted fun (x : Ω) ↦ u * X x] ≤ HPow.hPow (β := ℕ) ((b - a) / 2) 2
⊢ iteratedDeriv 2 (cgf X μ) u ≤ HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
have _₂ : HPow.hPow (β := ℕ) ((b - a) / 2) 2 = HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
Tactic: calc
  _ = Var[X; μ.tilted (u * X ·)] := by
    rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]
  _ ≤ ((b - a) / 2) ^ 2 := by
    convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
    · exact isProbabilityMeasure_tilted (hi u)
    · exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))
  _ = (‖b - a‖₊ / 2) ^ 2 := by simp [field]
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have inl : ∀ (ht : 0 < t), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: obtain ht | ht | ht := lt_trichotomy 0 t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
inl : ∀ (ht : 0 < t), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have inr : ∀ (ht : 0 = t), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: obtain ht | ht | ht := lt_trichotomy 0 t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
inl : ∀ (ht : 0 < t), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
inr : ∀ (ht : 0 = t), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have inr₁ : ∀ (ht : t < 0), mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: obtain ht | ht | ht := lt_trichotomy 0 t
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
⊢ mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)
have hb₁ : ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
Tactic: apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
-- Lean 4 proof step from Mathlib.Probability.Moments.SubGaussian (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
t : ℝ
ht : t < 0
hb₁ : ∀ᵐ (ω : Ω) ∂μ, -X ω ∈ Set.Icc (-b) (-a)
⊢ mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)
have hc₁ : Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
Tactic: apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)