awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ 0 < mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t

Tactic:
mgf_pos' h0 (h_int t)

Premises used: ProbabilityTheory.mgf_pos'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ 0 < mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t

Tactic:
exact mgf_pos' h0 (h_int t)

Premises used: ProbabilityTheory.mgf_pos'
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
h t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h0 : ¬Eq.{u_1 + 1} (α := Measure Ω) ((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) (0 : Measure Ω)
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact h t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
rw rw₁ : (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
rw [log_exp]

Premises used: Real.log_exp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
calc : log (mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t) ≤ log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2))
calc₁ : log (rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ cgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ (↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
calc cgf X (κ ω') t
  _ = log (mgf X (κ ω') t) := rfl
  _ ≤ log (exp (c * t ^ 2 / 2)) := by
    by_cases h0 : κ ω' = 0
    · simpa [h0] using by positivity
    gcongr
    · exact mgf_pos' h0 (h_int t)
    · exact h t
  _ ≤ c * t ^ 2 / 2 := by rw [log_exp]

Premises used: HMul.hMul, ProbabilityTheory.cgf, HDiv.hDiv, Real.exp, Real.log, HPow.hPow, ProbabilityTheory.mgf, OfNat.ofNat, DFunLike.coe, NNReal.toReal, rfl
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h₁ :
  ∀ (ω' : Ω') (h : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (0 * X y)) ((κ : (a : Ω') → Measure Ω) ω'))
    (h_mgf :
      ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
    IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
filter_upwards [h.ae_integrable_exp_mul 0, h.mgf_le] with ω' h h_mgf

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le, OfNat.ofNat, ProbabilityTheory.Kernel.HasSubgaussianMGF.ae_integrable_exp_mul
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : @Integrable ℝ _ _ _ mΩ (fun (y : Ω) ↦ rexp (0 * X y)) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
simpa [integrable_const_iff] using h

Premises used: MeasureTheory.integrable_const_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
h₁ :
  ∀ (ω' : Ω') (h : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω'))
    (h_mgf :
      ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)),
    LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
filter_upwards [h.isFiniteMeasure, h.mgf_le] with ω' h h_mgf

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.isFiniteMeasure, ProbabilityTheory.Kernel.HasSubgaussianMGF.mgf_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
this : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1
rwa : (((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ ≤ ENNReal.ofReal 1
rwa₁ rwa₂ rwa₃ rwa₄ : ENNReal.toReal ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ) ≤ 1
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) zero_le_one]

Premises used: MeasureTheory.measure_ne_top, ENNReal.ofReal_one, zero_le_one, ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
h₁ : Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1
⊢ LE.le (α := ℝ≥0∞) ((((κ : (a : Ω') → Measure Ω) ω' : Measure Ω) : (a : Set Ω) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
suffices (κ ω').real Set.univ ≤ 1 by
    rwa [← ENNReal.ofReal_one, ENNReal.le_ofReal_iff_toReal_le (measure_ne_top _ _) zero_le_one]
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_1 : HasSubgaussianMGF X c κ ν
ω' : Ω'
h : IsFiniteMeasure.{u_1} (α := Ω) (m0 := mΩ) ((κ : (a : Ω') → Measure Ω) ω')
h_mgf : ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ Measure.real.{u_1} (α := Ω) (m := mΩ) ((κ : (a : Ω') → Measure Ω) ω') Set.univ ≤ 1

Tactic:
simpa [mgf] using h_mgf 0

Premises used: ProbabilityTheory.mgf, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ (q : ℚ),
    ∀ᵐ (ω' : Ω') ∂ν,
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑q : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑q : ℝ) 2 / 2)
⊢ ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)

Tactic:
rw [← ae_all_iff] at h_mgf

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
⊢ ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) x)

Tactic:
have h_int' (n : ℤ) := Measure.ae_integrable_of_integrable_comp (h_int n)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ (n : ℤ), ∀ᵐ (x : Ω') ∂ν, @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑n : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) x)
⊢ ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)

Tactic:
rw [← ae_all_iff] at h_int'

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
h :
  ∀ (ω' : Ω')
    (h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω'))
    (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
filter_upwards [h_int'] with ω' h_int t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
ω' : Ω'
h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)

Premises used: Int.le_ceil, ProbabilityTheory.integrable_exp_mul_of_le_of_le, Int.floor_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int' :
  ∀ᵐ (a : Ω') ∂ν, ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) a)
ω' : Ω'
h_int : ∀ (i : ℤ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp ((↑i : ℝ) * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)

Premises used: Int.le_ceil, ProbabilityTheory.integrable_exp_mul_of_le_of_le, Int.floor_le
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')

Tactic:
have h_int : ∀ᵐ ω' ∂ν, ∀ t, Integrable (fun ω ↦ exp (t * X ω)) (κ ω') := by
      have h_int' (n : ℤ) := Measure.ae_integrable_of_integrable_comp (h_int n)
      rw [← ae_all_iff] at h_int'
      filter_upwards [h_int'] with ω' h_int t
      exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
h :
  ∀ (ω' : Ω')
    (h_mgf :
      ∀ (i : ℚ),
        mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
          rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2))
    (h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')) (t : ℝ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
filter_upwards [h_mgf, h_int] with ω' h_mgf h_int t
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf_1 :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int_2 :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
ω' : Ω'
h_mgf :
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
Rat.denseRange_cast.induction_on t ?_ h_mgf

Premises used: Rat.denseRange_cast, DenseRange.induction_on
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf_1 :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int_2 :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
ω' : Ω'
h_mgf :
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
h :
  IsClosed (X := ℝ)
    {b : ℝ | mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') b ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) b 2 / 2)}
⊢ mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
refine Rat.denseRange_cast.induction_on t ?_ h_mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf_1 :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int_2 :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
ω' : Ω'
h_mgf :
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ Continuous (Y := ℝ) fun (b : ℝ) ↦ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) b 2 / 2)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h_int_1 : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)
h_mgf_1 :
  ∀ᵐ (a : Ω') ∂ν,
    ∀ (i : ℚ),
      mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) a) (↑i : ℝ) ≤
        rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int_2 :
  ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
ω' : Ω'
h_mgf :
  ∀ (i : ℚ),
    mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') (↑i : ℝ) ≤
      rexp ((↑c : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) (↑i : ℝ) 2 / 2)
h_int : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((κ : (a : Ω') → Measure Ω) ω')
t : ℝ
⊢ IsClosed (X := ℝ)
    {b : ℝ | mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') b ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) b 2 / 2)}

Tactic:
exact isClosed_le (continuous_mgf h_int) (by fun_prop)

Premises used: isClosed_le, ProbabilityTheory.continuous_mgf
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
inst : IsFiniteMeasure ν
inst_1 : IsZeroOrMarkovKernel κ
⊢ ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * 0)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
inst : IsFiniteMeasure ν
inst_1 : IsZeroOrMarkovKernel κ
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) (fun (x : Ω) ↦ 0) ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑0 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simpa using ae_of_all _ fun _ ↦ measureReal_le_one

Premises used: MeasureTheory.ae_of_all, MeasureTheory.measureReal_le_one
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
inst : IsFiniteMeasure ν
inst_1 : IsZeroOrMarkovKernel κ
⊢ HasSubgaussianMGF 0 0 κ ν

Tactic:
fun_zero

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.fun_zero
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
integrable_exp_mul : ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑0 : (a : Ω') → Measure Ω) ∘ₘ ν)
mgf_le :
  ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) X (((0 : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ HasSubgaussianMGF (mΩ := mΩ) X c 0 ν

Tactic:
constructor
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ), @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω)) ((⇑0 : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ),
      mgf (m := mΩ) X (((0 : Kernel Ω' Ω) : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simp [exp_nonneg]

Premises used: Real.exp_nonneg
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ),
    @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * X ω))
      (Measure.bind.{u_2, u_1} (α := Ω') (mα := mΩ') 0 (⇑κ : (a : Ω') → Measure Ω))

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂0,
    ∀ (t : ℝ), mgf (m := mΩ) X ((κ : (a : Ω') → Measure Ω) ω') t ≤ rexp ((↑c : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.SubGaussian
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ @Integrable ℝ _ _ _ mΩ (fun (ω : Ω) ↦ rexp (t * (-X) ω)) ((⇑κ : (a : Ω') → Measure Ω) ∘ₘ ν)

Tactic:
simpa using h.integrable_exp_mul (-t)

Premises used: ProbabilityTheory.Kernel.HasSubgaussianMGF.integrable_exp_mul, Neg.neg