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 (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 ∂μ)
ω : Ω
⊢ X ω ≤ Y ω ↔
    HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)

Tactic:
grind
-- 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 ∂μ)
⊢ μ.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:
(measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
-- 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 ∂μ)
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 ∂μ)
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 : ℝ))))
⊢ μ.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:
refine (measure_ge_le (X := fun ω ↦ (Y ω - μ[Y]) - (X ω - μ[X])) (c := cX + cY) ?_ ?_).trans_eq
      ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
-- 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 ∂μ)
refine_1 : HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cX + cY) μ

Tactic:
rw [add_comm cX]

Premises used: add_comm
-- 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 ∂μ)
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ

Tactic:
sub_of_indepFun hY hX ?_

Premises used: ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun
-- 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 ∂μ)
refine_1 : (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ) ⟂ᵢ[μ] fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ
⊢ HasSubgaussianMGF (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)) (cY + cX) μ

Tactic:
refine sub_of_indepFun hY hX ?_

Premises used: ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun
-- 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 ∂μ)
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ x - ∫ (x : Ω), Y x ∂μ

Tactic:
fun_prop
-- 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 ∂μ)
⊢ Measurable (β := ℝ) fun (x : ℝ) ↦ x - ∫ (x : Ω), X x ∂μ

Tactic:
fun_prop
-- 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 ∂μ)
⊢ (fun (ω : Ω) ↦ Y ω - ∫ (x : Ω), Y x ∂μ) ⟂ᵢ[μ] fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ

Tactic:
exact hindep.symm.comp (φ := fun x ↦ x - μ[Y]) (ψ := fun x ↦ x - μ[X])
        (by fun_prop) (by fun_prop)

Premises used: ProbabilityTheory.IndepFun.comp, ProbabilityTheory.IndepFun.symm
-- 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 ∂μ)
⊢ 0 ≤ HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)

Tactic:
grind
-- 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 ∂μ)
refine_3 :
  -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) 2 =
    -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2
⊢ 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:
congr 2
-- 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 ∂μ)
⊢ -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ)) 2 =
    -HPow.hPow (β := ℕ) (HSub.hSub (α := ℝ) (∫ (x : Ω), Y x ∂μ) (∫ (x : Ω), X x ∂μ)) 2

Tactic:
grind
-- 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 ∂μ)
calc :
  μ.real {ω : Ω | X ω ≤ Y ω} =
    μ.real
      {ω : Ω |
        HSub.hSub (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), Y x ∂μ) ≤
          Y ω - ∫ (x : Ω), Y x ∂μ - (X ω - ∫ (x : Ω), X x ∂μ)}
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 : ℝ))))
⊢ μ.real {ω : Ω | X ω ≤ Y ω} ≤
    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

Premises used: HMul.hMul, setOf, MeasureTheory.Measure.real, HSub.hSub, HDiv.hDiv, LE.le, Real.exp, HPow.hPow, HAdd.hAdd, MeasureTheory.integral, OfNat.ofNat, NNReal.toReal, Neg.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ ∀ (u : ℝ), Integrable (ε := ℝ) (fun (ω : Ω) ↦ rexp (u * X ω)) μ

Tactic:
have hi (u : ℝ) : Integrable (fun ω ↦ exp (u * X ω)) μ := integrable_exp_mul_of_mem_Icc hm hb
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)) μ
⊢ Set.Icc 0 t ⊆ interior (integrableExpSet X μ)

Tactic:
simp [hi, integrableExpSet]

Premises used: ProbabilityTheory.integrableExpSet
-- Module: Mathlib.Probability.Moments.SubGaussian
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 ω)) μ
⊢ Set.Icc 0 t ⊆ interior (integrableExpSet X μ)

Tactic:
have hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ) := by simp [hi, integrableExpSet]
-- Module: Mathlib.Probability.Moments.SubGaussian
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 μ)
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)
⊢ 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

Premises used: ProbabilityTheory.exists_cgf_eq_iteratedDeriv_two_cgf_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
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
rw :
  iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2 ≤
    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)

Tactic:
rw [← exp_cgf (hi t), exp_le_exp, h2]

Premises used: ProbabilityTheory.exp_cgf, Real.exp_le_exp
-- Module: Mathlib.Probability.Moments.SubGaussian
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
hab : iteratedDeriv 2 (cgf X μ) u ≤ HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
⊢ iteratedDeriv 2 (cgf X μ) u * HPow.hPow (β := ℕ) t 2 / 2 ≤
    HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
gcongr
-- Module: Mathlib.Probability.Moments.SubGaussian
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
rw rw₁ : Var[X; μ.tilted fun (x : Ω) ↦ u * X x] = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]
⊢ iteratedDeriv 2 (cgf X μ) u = Var[X; μ.tilted fun (x : Ω) ↦ u * X x]

Tactic:
rw [← variance_tilted_mul (hs (Set.mem_Icc_of_Ioo h1))]

Premises used: Set.mem_Icc_of_Ioo, ProbabilityTheory.variance_tilted_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
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

Tactic:
variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _

Premises used: HMul.hMul, ProbabilityTheory.variance_le_sq_of_bounded, MeasureTheory.tilted_absolutelyContinuous
-- Module: Mathlib.Probability.Moments.SubGaussian
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)
convert_2 : AEMeasurable X (μ.tilted fun (x : Ω) ↦ u * X x)
⊢ Var[X; μ.tilted fun (x : Ω) ↦ u * X x] ≤ HPow.hPow (β := ℕ) ((b - a) / 2) 2

Tactic:
convert! variance_le_sq_of_bounded ((tilted_absolutelyContinuous μ (u * X ·)) hb) _
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ IsProbabilityMeasure (μ.tilted fun (x : Ω) ↦ u * X x)

Tactic:
isProbabilityMeasure_tilted (hi u)

Premises used: MeasureTheory.isProbabilityMeasure_tilted
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ IsProbabilityMeasure (μ.tilted fun (x : Ω) ↦ u * X x)

Tactic:
exact isProbabilityMeasure_tilted (hi u)

Premises used: MeasureTheory.isProbabilityMeasure_tilted
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ AEMeasurable X (μ.tilted fun (x : Ω) ↦ u * X x)

Tactic:
hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))

Premises used: HMul.hMul, AEMeasurable.mono_ac, MeasureTheory.tilted_absolutelyContinuous
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ AEMeasurable X (μ.tilted fun (x : Ω) ↦ u * X x)

Tactic:
exact hm.mono_ac (tilted_absolutelyContinuous μ (u * X ·))

Premises used: HMul.hMul, AEMeasurable.mono_ac, MeasureTheory.tilted_absolutelyContinuous
-- Module: Mathlib.Probability.Moments.SubGaussian
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
⊢ HPow.hPow (β := ℕ) ((b - a) / 2) 2 = HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2

Tactic:
simp [field]
-- Module: Mathlib.Probability.Moments.SubGaussian
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
_₂ : HPow.hPow (β := ℕ) ((b - a) / 2) 2 = HPow.hPow (β := ℕ) ((↑‖b - a‖₊ : ℝ) / 2) 2
⊢ iteratedDeriv 2 (cgf X μ) u ≤ 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]

Premises used: HMul.hMul, NNNorm.nnnorm, HSub.hSub, HDiv.hDiv, MeasureTheory.Measure.tilted, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
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)
inr₁ : ∀ (ht : t < 0), 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)

Tactic:
obtain ht | ht | ht := lt_trichotomy 0 t

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : 0 < t
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero hm hb hc ht

Premises used: ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero, NNReal.toReal
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : 0 < t
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero hm hb hc ht

Premises used: ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
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 : 0 = t
⊢ mgf X μ t ≤ rexp ((↑(HPow.hPow (β := ℕ) (‖b - a‖₊ / 2) 2) : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simp [← ht]
-- Module: Mathlib.Probability.Moments.SubGaussian
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 = mgf (-X) μ (-t)

Tactic:
simp [mgf]

Premises used: ProbabilityTheory.mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
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)
hc₁ : Eq (α := ℝ) (∫ (x : Ω), -X x ∂μ) 0
ht₁ : 0 < -t
⊢ mgf (-X) μ (-t) ≤ rexp (HPow.hPow (β := ℕ) ((↑‖-a - -b‖₊ : ℝ) / 2) 2 * HPow.hPow (β := ℕ) (-t) 2 / 2)

Tactic:
apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)

Premises used: ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero, AEMeasurable.neg
-- Module: Mathlib.Probability.Moments.SubGaussian
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
ω : Ω
h : ∀ (hl : a ≤ X ω) (hr : X ω ≤ b), -X ω ∈ Set.Icc (-b) (-a)
⊢ X ω ∈ Set.Icc a b → -X ω ∈ Set.Icc (-b) (-a)

Tactic:
⟨hl, hr⟩
-- Module: Mathlib.Probability.Moments.SubGaussian
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
ω : Ω
hl : a ≤ X ω
hr : X ω ≤ b
⊢ -X ω ∈ Set.Icc (-b) (-a)

Tactic:
⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.Icc, And.intro, neg_le_neg_iff