Sub-exponential random variables

A real random variable X has a sub-exponential moment generating function (mgf) with parameters (V, b) if for every t with b * |t| ≤ 1, exp (t * X) is integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2). The range of t is written as b * |t| ≤ 1 (rather than |t| ≤ 1 / b) so that b = 0 imposes no restriction on t: the case b = 0 is exactly HasSubgaussianMGF (see Mathlib/Probability/Moments/SubGaussian.lean, whose structure this file follows).

As for sub-Gaussian variables, the notion is first defined with respect to a kernel and a measure (Kernel.HasSubexponentialMGF), then specialized to conditionally sub-exponential variables (HasCondSubexponentialMGF, the kernel being the conditional expectation kernel of a sub-σ-algebra) and to sub-exponential variables with respect to a measure (HasSubexponentialMGF, a constant kernel).

Main definitions

• Kernel.HasSubexponentialMGF X V b κ ν: for every t with b * |t| ≤ 1, exp (t * X) is integrable with respect to κ ∘ₘ ν and, for ν-almost every ω', mgf X (κ ω') t ≤ exp (V * t ^ 2 / 2).
• HasCondSubexponentialMGF m hm X V b μ: Kernel.HasSubexponentialMGF with respect to the conditional expectation kernel condExpKernel μ m and the measure μ.trim hm.
• HasSubexponentialMGF X V b μ: for every t with b * |t| ≤ 1, exp (t * X) is μ-integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2). This is equivalent to Kernel.HasSubexponentialMGF with a constant kernel (hasSubexponentialMGF_iff_kernel).

Main results

• HasSubexponentialMGF.integral_eq_zero: a sub-exponential variable is integrable and centered.
• HasSubexponentialMGF.const_mul, neg, mono, add, add_of_indepFun, sum_of_iIndepFun: stability under scaling, sums, and independent sums.
• HasSubexponentialMGF.measure_ge_le, measure_le_le, measure_abs_ge_le: Bernstein-type tail bounds exp (-min (t ^ 2 / (2 * V)) (t / (2 * b))).
• HasSubexponentialMGF.measure_sum_ge_le_of_iIndepFun, measure_abs_average_ge_le: Bernstein's inequality for sums and averages of independent sub-exponential variables.
• hasSubexponentialMGF_of_abs_le_of_integral_eq_zero: a centered variable bounded by M with second moment at most v has parameters (3 * v / 2, M).
• HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF and measure_sum_ge_le_of_hasCondSubexponentialMGF: a sum of conditionally sub-exponential martingale differences is sub-exponential, and the corresponding Azuma–Bernstein inequality.

Implementation notes

The parameters V and b are real numbers rather than ℝ≥0, which avoids coercions in the arithmetic of the applications. The Bernstein-type tail bounds do not assume 0 < V or 0 < b: when V ≤ 0 or b ≤ 0, the right-hand side exp (-min (t ^ 2 / (2 * V)) (t / (2 * b))) is at least 1 (with the convention x / 0 = 0) and the bound holds trivially. As in Kernel.HasSubgaussianMGF, the integrability condition of the kernel version is integrability with respect to κ ∘ₘ ν, not almost-everywhere integrability with respect to κ ω'.

Sub-exponential with respect to a kernel and a measure

structure ProbabilityTheory.Kernel.HasSubexponentialMGF {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} (X : Ω → ℝ) (V b : ℝ) (κ : Kernel Ω' Ω) (ν : MeasureTheory.Measure Ω' := by volume_tac) : Prop

A random variable X has a sub-exponential moment-generating function with parameters (V, b) with respect to a kernel κ and a measure ν if for every t with b * |t| ≤ 1, exp (t * X) is integrable with respect to κ ∘ₘ ν and, for ν-almost all ω', the moment-generating function of X with respect to κ ω' is bounded by exp (V * t ^ 2 / 2). For b = 0 this is Kernel.HasSubgaussianMGF X V κ ν.

• integrable_exp_mul (t : ℝ) : b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (ν.bind ⇑κ)
• mgf_le : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), b * |t| ≤ 1 → mgf X (κ ω') t ≤ Real.exp (V * t ^ 2 / 2)

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.aestronglyMeasurable {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : MeasureTheory.AEStronglyMeasurable X (ν.bind ⇑κ)

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_integrable_exp_mul {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (ht : b * |t| ≤ 1) : ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.Integrable (fun (y : Ω) => Real.exp (t * X y)) (κ ω')

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_aestronglyMeasurable {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.AEStronglyMeasurable X (κ ω')

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_forall_integrable_exp_mul_of_forall {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {b : ℝ} (h_int : ∀ (t : ℝ), b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (ν.bind ⇑κ)) : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (κ ω')

Auxiliary lemma: almost-everywhere integrability of exp (t * X) with respect to κ ω', simultaneously for all admissible t, from the integrability with respect to κ ∘ₘ ν.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_forall_integrable_exp_mul {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (κ ω')

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_forall_memLp_exp_mul {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (p : NNReal) : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), b * |↑p * t| ≤ 1 → MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω)) (↑p) (κ ω')

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.memLp_exp_mul {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (p : NNReal) (ht : b * |↑p * t| ≤ 1) : MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω)) (↑p) (ν.bind ⇑κ)

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.cgf_le {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (hV : 0 ≤ V) : ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), b * |t| ≤ 1 → cgf X (κ ω') t ≤ V * t ^ 2 / 2

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.isFiniteMeasure {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, MeasureTheory.IsFiniteMeasure (κ ω')

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_univ_le_one {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω') Set.univ ≤ 1

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_le_one {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (s : Set Ω) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω') s ≤ 1

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measureReal_le_one {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (s : Set Ω) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real s ≤ 1

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.of_ae_mgf_le {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h_int : ∀ (t : ℝ), b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) (ν.bind ⇑κ)) (h_mgf : ∀ (t : ℝ), b * |t| ≤ 1 → ∀ᵐ (ω' : Ω') ∂ν, mgf X (κ ω') t ≤ Real.exp (V * t ^ 2 / 2)) : HasSubexponentialMGF X V b κ ν

To prove that X is sub-exponential with respect to κ and ν, it suffices to check the bound on the mgf for each admissible t separately, almost everywhere.

@[simp]

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.fun_zero {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {b : ℝ} [MeasureTheory.IsFiniteMeasure ν] [IsZeroOrMarkovKernel κ] : HasSubexponentialMGF (fun (x : Ω) => 0) 0 b κ ν

@[simp]

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.zero {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {b : ℝ} [MeasureTheory.IsFiniteMeasure ν] [IsZeroOrMarkovKernel κ] : HasSubexponentialMGF 0 0 b κ ν

@[simp]

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.zero_kernel {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {X : Ω → ℝ} {V b : ℝ} : HasSubexponentialMGF X V b 0 ν

@[simp]

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.zero_measure {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} : HasSubexponentialMGF X V b κ 0

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.neg {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : HasSubexponentialMGF (-X) V b κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.fun_neg {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) : HasSubexponentialMGF (fun (i : Ω) => -X i) V b κ ν

Eta-expanded form of ProbabilityTheory.Kernel.HasSubexponentialMGF.neg

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.mono {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {V' b' : ℝ} (hV : V ≤ V') (hb : b ≤ b') : HasSubexponentialMGF X V' b' κ ν

theorem ProbabilityTheory.Kernel.HasSubgaussianMGF.hasSubexponentialMGF {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} (h : HasSubgaussianMGF X c κ ν) (b : ℝ) : HasSubexponentialMGF X (↑c) b κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.hasSubgaussianMGF {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V : ℝ} (h : HasSubexponentialMGF X V 0 κ ν) (hV : 0 ≤ V) : HasSubgaussianMGF X ⟨V, hV⟩ κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.congr {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} {Y : Ω → ℝ} (h : HasSubexponentialMGF X V b κ ν) (h' : X =ᵐ[ν.bind ⇑κ] Y) : HasSubexponentialMGF Y V b κ ν

theorem ProbabilityTheory.Kernel.hasSubexponentialMGF_congr {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} {Y : Ω → ℝ} (h : X =ᵐ[ν.bind ⇑κ] Y) : HasSubexponentialMGF X V b κ ν ↔ HasSubexponentialMGF Y V b κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.of_map {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {V b : ℝ} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {κ : Kernel Ω' Ω''} {Y : Ω'' → Ω} {X : Ω → ℝ} (hY : Measurable Y) (h : HasSubexponentialMGF X V b (κ.map Y) ν) : HasSubexponentialMGF (X ∘ Y) V b κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.id_map_iff {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (hX : Measurable X) : HasSubexponentialMGF id V b (κ.map X) ν ↔ HasSubexponentialMGF X V b κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.const_mul {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (r : ℝ) : HasSubexponentialMGF (fun (ω : Ω) => r * X ω) (r ^ 2 * V) (|r| * b) κ ν

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_ge_le_exp_add {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (t : ℝ) : ∀ᵐ (ω' : Ω') ∂ν, ∀ (s : ℝ), 0 ≤ s → b * |s| ≤ 1 → (κ ω').real {ω : Ω | t ≤ X ω} ≤ Real.exp (-s * t + V * s ^ 2 / 2)

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_ge_le_exp_neg_sq {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (ht : 0 ≤ t) (htb : t * b ≤ V) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω : Ω | t ≤ X ω} ≤ Real.exp (-(t ^ 2 / (2 * V)))

Chernoff bound in the Gaussian regime t * b ≤ V.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_ge_le_exp_neg_div {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) (hb : 0 < b) {t : ℝ} (htb : V ≤ t * b) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω : Ω | t ≤ X ω} ≤ Real.exp (-(t / (2 * b)))

Chernoff bound in the exponential regime V ≤ t * b.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_ge_le {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (ht : 0 ≤ t) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω : Ω | t ≤ X ω} ≤ Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound for the upper tail of a sub-exponential random variable. When V ≤ 0 or b ≤ 0, the right-hand side is at least 1 and the bound is trivial.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_le_le {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (ht : 0 ≤ t) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω : Ω | X ω ≤ -t} ≤ Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound for the lower tail of a sub-exponential random variable.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.measure_abs_ge_le {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b κ ν) {t : ℝ} (ht : 0 ≤ t) : ∀ᵐ (ω' : Ω') ∂ν, (κ ω').real {ω : Ω | t ≤ |X ω|} ≤ 2 * Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound, two-sided.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.add_of_holderConjugate {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X Y : Ω → ℝ} {VX VY bX bY p q : ℝ} (hpq : p.HolderConjugate q) (hX : HasSubexponentialMGF X VX bX κ ν) (hY : HasSubexponentialMGF Y VY bY κ ν) : HasSubexponentialMGF (fun (ω : Ω) => X ω + Y ω) (p * VX + q * VY) (max (p * bX) (q * bY)) κ ν

Sum of two (not necessarily independent) sub-exponential variables, by Hölder's inequality with conjugate exponents p and q. The case p = q = 2 is add.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.add {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X Y : Ω → ℝ} {VX VY bX bY : ℝ} (hX : HasSubexponentialMGF X VX bX κ ν) (hY : HasSubexponentialMGF Y VY bY κ ν) : HasSubexponentialMGF (fun (ω : Ω) => X ω + Y ω) (2 * (VX + VY)) (2 * max bX bY) κ ν

Sum of two (not necessarily independent) sub-exponential variables, by the Cauchy–Schwarz inequality.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.prodMkLeft_compProd {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {b : ℝ} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {Y : Ω'' → ℝ} {VY : ℝ} {η : Kernel Ω Ω''} (h : HasSubexponentialMGF Y VY b η (ν.bind ⇑κ)) : HasSubexponentialMGF Y VY b (prodMkLeft Ω' η) (ν.compProd κ)

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.integrable_exp_add_compProd {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {Y : Ω'' → ℝ} {VY : ℝ} [MeasureTheory.SFinite ν] {η : Kernel (Ω' × Ω) Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubexponentialMGF X V b κ ν) (hY : HasSubexponentialMGF Y VY b η (ν.compProd κ)) {t : ℝ} (ht : b * |t| ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω × Ω'') => Real.exp (t * (X ω.1 + Y ω.2))) (ν.bind ⇑(κ.compProd η))

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.add_compProd {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {Y : Ω'' → ℝ} {VY : ℝ} [MeasureTheory.SFinite ν] {η : Kernel (Ω' × Ω) Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubexponentialMGF X V b κ ν) (hY : HasSubexponentialMGF Y VY b η (ν.compProd κ)) : HasSubexponentialMGF (fun (p : Ω × Ω'') => X p.1 + Y p.2) (V + VY) b (κ.compProd η) ν

For ν : Measure Ω', κ : Kernel Ω' Ω and η : (Ω' × Ω) Ω'', if a random variable X : Ω → ℝ has a sub-exponential mgf with respect to κ and ν and another random variable Y : Ω'' → ℝ has a sub-exponential mgf with respect to η and ν ⊗ₘ κ : Measure (Ω' × Ω), with the same parameter b, then X + Y (random variable on the measurable space Ω × Ω'') has a sub-exponential mgf with respect to κ ⊗ₖ η : Kernel Ω' (Ω × Ω'') and ν.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.add_comp {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} {X : Ω → ℝ} {V b : ℝ} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''} {Y : Ω'' → ℝ} {VY : ℝ} [MeasureTheory.SFinite ν] {η : Kernel Ω Ω''} [IsZeroOrMarkovKernel η] (hX : HasSubexponentialMGF X V b κ ν) (hY : HasSubexponentialMGF Y VY b η (ν.bind ⇑κ)) : HasSubexponentialMGF (fun (p : Ω × Ω'') => X p.1 + Y p.2) (V + VY) b (κ.compProd (prodMkLeft Ω' η)) ν

For ν : Measure Ω', κ : Kernel Ω' Ω and η : Ω Ω'', if a random variable X : Ω → ℝ has a sub-exponential mgf with respect to κ and ν and another random variable Y : Ω'' → ℝ has a sub-exponential mgf with respect to η and κ ∘ₘ ν : Measure Ω, with the same parameter b, then X + Y (random variable on the measurable space Ω × Ω'') has a sub-exponential mgf with respect to κ ⊗ₖ prodMkLeft Ω' η : Kernel Ω' (Ω × Ω'') and ν.

Conditionally sub-exponential moment-generating function

def ProbabilityTheory.HasCondSubexponentialMGF {Ω : Type u_1} (m : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) [StandardBorelSpace Ω] (X : Ω → ℝ) (V b : ℝ) (μ : MeasureTheory.Measure Ω := by volume_tac) [MeasureTheory.IsFiniteMeasure μ] : Prop

A random variable X has a conditionally sub-exponential moment-generating function with parameters (V, b) with respect to a sigma-algebra m and a measure μ if for all t with b * |t| ≤ 1, exp (t * X) is μ-integrable and the moment-generating function of X conditioned on m is almost surely bounded by exp (V * t ^ 2 / 2).

The actual definition uses Kernel.HasSubexponentialMGF: HasCondSubexponentialMGF is defined as sub-exponential with respect to the conditional expectation kernel for m and the restriction of μ to the sigma-algebra m.

Equations

• ProbabilityTheory.HasCondSubexponentialMGF m hm X V b μ = ProbabilityTheory.Kernel.HasSubexponentialMGF X V b (ProbabilityTheory.condExpKernel μ m) (μ.trim hm)

theorem ProbabilityTheory.HasCondSubexponentialMGF.mgf_le {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) : ∀ᵐ (ω' : Ω) ∂μ.trim hm, ∀ (t : ℝ), b * |t| ≤ 1 → mgf X ((condExpKernel μ m) ω') t ≤ Real.exp (V * t ^ 2 / 2)

theorem ProbabilityTheory.HasCondSubexponentialMGF.cgf_le {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) (hV : 0 ≤ V) : ∀ᵐ (ω' : Ω) ∂μ.trim hm, ∀ (t : ℝ), b * |t| ≤ 1 → cgf X ((condExpKernel μ m) ω') t ≤ V * t ^ 2 / 2

theorem ProbabilityTheory.HasCondSubexponentialMGF.ae_trim_condExp_le {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) {t : ℝ} (ht : b * |t| ≤ 1) : ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun (ω : Ω) => Real.exp (t * X ω) | m] ω' ≤ Real.exp (V * t ^ 2 / 2)

theorem ProbabilityTheory.HasCondSubexponentialMGF.ae_condExp_le {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) {t : ℝ} (ht : b * |t| ≤ 1) : ∀ᵐ (ω' : Ω) ∂μ, μ[fun (ω : Ω) => Real.exp (t * X ω) | m] ω' ≤ Real.exp (V * t ^ 2 / 2)

@[simp]

theorem ProbabilityTheory.HasCondSubexponentialMGF.fun_zero {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {b : ℝ} : HasCondSubexponentialMGF m hm (fun (x : Ω) => 0) 0 b μ

@[simp]

theorem ProbabilityTheory.HasCondSubexponentialMGF.zero {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {b : ℝ} : HasCondSubexponentialMGF m hm 0 0 b μ

theorem ProbabilityTheory.HasCondSubexponentialMGF.memLp_exp_mul {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) {t : ℝ} (p : NNReal) (ht : b * |↑p * t| ≤ 1) : MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω)) (↑p) μ

theorem ProbabilityTheory.HasCondSubexponentialMGF.integrable_exp_mul {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V b : ℝ} (h : HasCondSubexponentialMGF m hm X V b μ) {t : ℝ} (ht : b * |t| ≤ 1) : MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ

theorem ProbabilityTheory.HasCondSubgaussianMGF.hasCondSubexponentialMGF {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal} (h : HasCondSubgaussianMGF m hm X c μ) (b : ℝ) : HasCondSubexponentialMGF m hm X (↑c) b μ

theorem ProbabilityTheory.HasCondSubexponentialMGF.hasCondSubgaussianMGF {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {V : ℝ} (h : HasCondSubexponentialMGF m hm X V 0 μ) (hV : 0 ≤ V) : HasCondSubgaussianMGF m hm X ⟨V, hV⟩ μ

Sub-exponential moment-generating function

structure ProbabilityTheory.HasSubexponentialMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (X : Ω → ℝ) (V b : ℝ) (μ : MeasureTheory.Measure Ω := by volume_tac) : Prop

X has a sub-exponential moment generating function with parameters (V, b): for every t with b * |t| ≤ 1, exp (t * X) is integrable and mgf X μ t ≤ exp (V * t ^ 2 / 2). For b = 0 this is HasSubgaussianMGF X V μ.

This is equivalent to Kernel.HasSubexponentialMGF X V b (Kernel.const Unit μ) (Measure.dirac ()), as proved in hasSubexponentialMGF_iff_kernel.

• integrable_exp_mul (t : ℝ) : b * |t| ≤ 1 → MeasureTheory.Integrable (fun (ω : Ω) => Real.exp (t * X ω)) μ
• mgf_le (t : ℝ) : b * |t| ≤ 1 → mgf X μ t ≤ Real.exp (V * t ^ 2 / 2)

theorem ProbabilityTheory.hasSubexponentialMGF_iff_kernel {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} : HasSubexponentialMGF X V b μ ↔ Kernel.HasSubexponentialMGF X V b (Kernel.const Unit μ) (MeasureTheory.Measure.dirac ())

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_hasSubexponentialMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {V b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, ProbabilityTheory.HasSubexponentialMGF X V b (κ ω')

theorem ProbabilityTheory.HasSubgaussianMGF.hasSubexponentialMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} (h : HasSubgaussianMGF X c μ) (b : ℝ) : HasSubexponentialMGF X (↑c) b μ

theorem ProbabilityTheory.HasSubexponentialMGF.hasSubgaussianMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V : ℝ} (h : HasSubexponentialMGF X V 0 μ) (hV : 0 ≤ V) : HasSubgaussianMGF X ⟨V, hV⟩ μ

theorem ProbabilityTheory.HasSubexponentialMGF.mono {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {V' b' : ℝ} (hV : V ≤ V') (hb : b ≤ b') : HasSubexponentialMGF X V' b' μ

theorem ProbabilityTheory.HasSubexponentialMGF.aestronglyMeasurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : MeasureTheory.AEStronglyMeasurable X μ

theorem ProbabilityTheory.HasSubexponentialMGF.isFiniteMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : MeasureTheory.IsFiniteMeasure μ

theorem ProbabilityTheory.HasSubexponentialMGF.congr {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {Y : Ω → ℝ} (h' : X =ᵐ[μ] Y) : HasSubexponentialMGF Y V b μ

theorem ProbabilityTheory.HasSubexponentialMGF.memLp_exp_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (p : NNReal) (ht : b * |↑p * t| ≤ 1) : MeasureTheory.MemLp (fun (ω : Ω) => Real.exp (t * X ω)) (↑p) μ

theorem ProbabilityTheory.HasSubexponentialMGF.cgf_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) (hV : 0 ≤ V) {t : ℝ} (ht : b * |t| ≤ 1) : cgf X μ t ≤ V * t ^ 2 / 2

@[simp]

theorem ProbabilityTheory.HasSubexponentialMGF.fun_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] : HasSubexponentialMGF (fun (x : Ω) => 0) 0 b μ

@[simp]

theorem ProbabilityTheory.HasSubexponentialMGF.zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] : HasSubexponentialMGF 0 0 b μ

theorem ProbabilityTheory.HasSubexponentialMGF.neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : HasSubexponentialMGF (-X) V b μ

theorem ProbabilityTheory.HasSubexponentialMGF.fun_neg {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : HasSubexponentialMGF (fun (i : Ω) => -X i) V b μ

Eta-expanded form of ProbabilityTheory.HasSubexponentialMGF.neg

theorem ProbabilityTheory.HasSubexponentialMGF.of_map {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {V b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ} (hY : AEMeasurable Y μ) (h : HasSubexponentialMGF X V b (MeasureTheory.Measure.map Y μ)) : HasSubexponentialMGF (X ∘ Y) V b μ

theorem ProbabilityTheory.HasSubexponentialMGF.map_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {V b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'} {Y : Ω' → Ω} {X : Ω → ℝ} (hY : AEMeasurable Y μ) (hX : AEMeasurable X (MeasureTheory.Measure.map Y μ)) : HasSubexponentialMGF X V b (MeasureTheory.Measure.map Y μ) ↔ HasSubexponentialMGF (X ∘ Y) V b μ

theorem ProbabilityTheory.HasSubexponentialMGF.id_map_iff {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (hX : AEMeasurable X μ) : HasSubexponentialMGF id V b (MeasureTheory.Measure.map X μ) ↔ HasSubexponentialMGF X V b μ

theorem ProbabilityTheory.HasSubexponentialMGF.congr_identDistrib {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ} (hX : HasSubexponentialMGF X V b μ) (hXY : IdentDistrib X Y μ μ') : HasSubexponentialMGF Y V b μ'

theorem ProbabilityTheory.HasSubexponentialMGF.trim {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (hm : m ≤ mΩ) (hXm : Measurable X) (hX : HasSubexponentialMGF X V b μ) : HasSubexponentialMGF X V b (μ.trim hm)

theorem ProbabilityTheory.HasSubexponentialMGF.const_mul {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) (a : ℝ) : HasSubexponentialMGF (fun (ω : Ω) => a * X ω) (a ^ 2 * V) (|a| * b) μ

theorem ProbabilityTheory.HasSubexponentialMGF.zero_mem_interior_integrableExpSet {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : 0 ∈ interior (integrableExpSet X μ)

theorem ProbabilityTheory.HasSubexponentialMGF.aemeasurable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : AEMeasurable X μ

theorem ProbabilityTheory.HasSubexponentialMGF.integrable {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) : MeasureTheory.Integrable X μ

theorem ProbabilityTheory.HasSubexponentialMGF.memLp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) (p : NNReal) : MeasureTheory.MemLp X (↑p) μ

theorem ProbabilityTheory.HasSubexponentialMGF.integrable_pow {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) (n : ℕ) : MeasureTheory.Integrable (fun (ω : Ω) => X ω ^ n) μ

theorem ProbabilityTheory.HasSubexponentialMGF.integral_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) [MeasureTheory.IsProbabilityMeasure μ] : ∫ (x : Ω), X x ∂μ = 0

A sub-exponential random variable is centered.

theorem ProbabilityTheory.HasSubexponentialMGF.ae_eq_zero_of_hasSubexponentialMGF_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b : ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasSubexponentialMGF X 0 b μ) : X =ᵐ[μ] 0

A random variable with sub-exponential parameters (0, b) on a probability space vanishes almost surely: its mgf is identically 1 near 0, so its second moment vanishes.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_ge_le_exp_neg_sq {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (ht : 0 ≤ t) (htb : t * b ≤ V) : μ.real {ω : Ω | t ≤ X ω} ≤ Real.exp (-(t ^ 2 / (2 * V)))

Chernoff bound in the Gaussian regime t * b ≤ V.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_ge_le_exp_neg_div {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) (hb : 0 < b) {t : ℝ} (htb : V ≤ t * b) : μ.real {ω : Ω | t ≤ X ω} ≤ Real.exp (-(t / (2 * b)))

Chernoff bound in the exponential regime V ≤ t * b.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_ge_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ X ω} ≤ Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound for the upper tail of a sub-exponential random variable. When V ≤ 0 or b ≤ 0, the right-hand side is at least 1 and the bound is trivial.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_le_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | X ω ≤ -t} ≤ Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound for the lower tail of a sub-exponential random variable.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_abs_ge_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ |X ω|} ≤ 2 * Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound, two-sided.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_abs_gt_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {V b : ℝ} (h : HasSubexponentialMGF X V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t < |X ω|} ≤ 2 * Real.exp (-min (t ^ 2 / (2 * V)) (t / (2 * b)))

Bernstein-type tail bound, two-sided, with a strict inequality in the event.

theorem ProbabilityTheory.HasSubexponentialMGF.add_of_holderConjugate {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {VX VY bX bY p q : ℝ} (hpq : p.HolderConjugate q) (hX : HasSubexponentialMGF X VX bX μ) (hY : HasSubexponentialMGF Y VY bY μ) : HasSubexponentialMGF (fun (ω : Ω) => X ω + Y ω) (p * VX + q * VY) (max (p * bX) (q * bY)) μ

Sum of two (not necessarily independent) sub-exponential variables, by Hölder's inequality with conjugate exponents p and q. The case p = q = 2 is add.

theorem ProbabilityTheory.HasSubexponentialMGF.add {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {VX VY bX bY : ℝ} (hX : HasSubexponentialMGF X VX bX μ) (hY : HasSubexponentialMGF Y VY bY μ) : HasSubexponentialMGF (fun (ω : Ω) => X ω + Y ω) (2 * (VX + VY)) (2 * max bX bY) μ

Sum of two (not necessarily independent) sub-exponential variables, by the Cauchy–Schwarz inequality.

theorem ProbabilityTheory.HasSubexponentialMGF.add_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b : ℝ} {Y : Ω → ℝ} {VX VY : ℝ} (hX : HasSubexponentialMGF X VX b μ) (hY : HasSubexponentialMGF Y VY b μ) (hindep : IndepFun X Y μ) : HasSubexponentialMGF (X + Y) (VX + VY) b μ

theorem ProbabilityTheory.HasSubexponentialMGF.sub_of_indepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b : ℝ} {Y : Ω → ℝ} {VX VY : ℝ} (hX : HasSubexponentialMGF X VX b μ) (hY : HasSubexponentialMGF Y VY b μ) (hindep : IndepFun X Y μ) : HasSubexponentialMGF (fun (ω : Ω) => X ω - Y ω) (VX + VY) b μ

theorem ProbabilityTheory.HasSubexponentialMGF.sum_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} (s : Finset ι) (h : ∀ i ∈ s, HasSubexponentialMGF (X i) (V i) b μ) : HasSubexponentialMGF (∑ i ∈ s, X i) (∑ i ∈ s, V i) b μ

theorem ProbabilityTheory.HasSubexponentialMGF.fun_sum_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} [Fintype ι] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} (h : ∀ (i : ι), HasSubexponentialMGF (X i) (V i) b μ) : HasSubexponentialMGF (fun (ω : Ω) => ∑ i : ι, X i ω) (∑ i : ι, V i) b μ

theorem ProbabilityTheory.HasSubexponentialMGF.measure_sum_ge_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} {s : Finset ι} (h : ∀ i ∈ s, HasSubexponentialMGF (X i) (V i) b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ ∑ i ∈ s, X i ω} ≤ Real.exp (-min (t ^ 2 / (2 * ∑ i ∈ s, V i)) (t / (2 * b)))

Bernstein's inequality for the upper tail of a sum of independent sub-exponential random variables.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_sum_le_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} {s : Finset ι} (h : ∀ i ∈ s, HasSubexponentialMGF (X i) (V i) b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | ∑ i ∈ s, X i ω ≤ -t} ≤ Real.exp (-min (t ^ 2 / (2 * ∑ i ∈ s, V i)) (t / (2 * b)))

Bernstein's inequality for the lower tail of a sum of independent sub-exponential random variables.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_sum_range_ge_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {V b : ℝ} {X : ℕ → Ω → ℝ} (h_indep : iIndepFun X μ) {n : ℕ} (h : ∀ i < n, HasSubexponentialMGF (X i) V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ ∑ i ∈ Finset.range n, X i ω} ≤ Real.exp (-min (t ^ 2 / (2 * ↑n * V)) (t / (2 * b)))

Bernstein's inequality for the upper tail of a sum of n independent sub-exponential random variables with the same parameters.

theorem ProbabilityTheory.HasSubexponentialMGF.measure_sum_range_le_le_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {V b : ℝ} {X : ℕ → Ω → ℝ} (h_indep : iIndepFun X μ) {n : ℕ} (h : ∀ i < n, HasSubexponentialMGF (X i) V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | ∑ i ∈ Finset.range n, X i ω ≤ -t} ≤ Real.exp (-min (t ^ 2 / (2 * ↑n * V)) (t / (2 * b)))

Bernstein's inequality for the lower tail of a sum of n independent sub-exponential random variables with the same parameters.

theorem ProbabilityTheory.HasSubexponentialMGF.average_of_iIndepFun {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} [Fintype ι] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} (h : ∀ (i : ι), HasSubexponentialMGF (X i) (V i) b μ) : HasSubexponentialMGF (fun (ω : Ω) => (∑ i : ι, X i ω) / ↑(Fintype.card ι)) ((∑ i : ι, V i) / ↑(Fintype.card ι) ^ 2) (b / ↑(Fintype.card ι)) μ

The average of K independent sub-exponential variables with parameters (V i, b) has parameters ((∑ i, V i) / K ^ 2, b / K).

theorem ProbabilityTheory.HasSubexponentialMGF.measure_abs_average_ge_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} {ι : Type u_2} [Fintype ι] [Nonempty ι] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) {V : ι → ℝ} (h : ∀ (i : ι), HasSubexponentialMGF (X i) (V i) b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ |(∑ i : ι, X i ω) / ↑(Fintype.card ι)|} ≤ 2 * Real.exp (-(↑(Fintype.card ι) * min (t ^ 2 / (2 * ((∑ i : ι, V i) / ↑(Fintype.card ι)))) (t / (2 * b))))

Tail bound for an average of independent sub-exponential variables with parameters (V i, b): writing K for the number of variables and V̄ := (∑ i, V i) / K, P(|(∑ i, X i) / K| ≥ t) ≤ 2 exp (-K min (t ^ 2 / (2 V̄)) (t / (2 b))).

theorem ProbabilityTheory.HasSubexponentialMGF.measure_abs_average_ge_le_of_forall {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {V b : ℝ} {ι : Type u_2} [Fintype ι] [Nonempty ι] {X : ι → Ω → ℝ} (h_indep : iIndepFun X μ) (h : ∀ (i : ι), HasSubexponentialMGF (X i) V b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ |(∑ i : ι, X i ω) / ↑(Fintype.card ι)|} ≤ 2 * Real.exp (-(↑(Fintype.card ι) * min (t ^ 2 / (2 * V)) (t / (2 * b))))

Tail bound for an average of independent sub-exponential variables with the same parameters (V, b).

theorem ProbabilityTheory.HasSubexponentialMGF.measureReal_le_le_exp {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b : ℝ} {Y : Ω → ℝ} {VX VY : ℝ} (hX : HasSubexponentialMGF (fun (ω : Ω) => X ω - ∫ (x : Ω), X x ∂μ) VX b μ) (hY : HasSubexponentialMGF (fun (ω : Ω) => Y ω - ∫ (x : Ω), Y x ∂μ) VY b μ) (hindep : IndepFun X Y μ) (h_le : ∫ (x : Ω), Y x ∂μ ≤ ∫ (x : Ω), X x ∂μ) : μ.real {ω : Ω | X ω ≤ Y ω} ≤ Real.exp (-min ((∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) ^ 2 / (2 * (VX + VY))) ((∫ (x : Ω), X x ∂μ - ∫ (x : Ω), Y x ∂μ) / (2 * b)))

For X, Y two independent random variables with sub-exponential fluctuations such that μ[X] ≥ μ[Y], the probability that X ≤ Y is bounded by a Bernstein-type term.

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_integral_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {V b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} [IsMarkovKernel κ] (h : HasSubexponentialMGF X V b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, ∫ (x : Ω), X x ∂κ ω' = 0

theorem ProbabilityTheory.Kernel.HasSubexponentialMGF.ae_eq_zero_of_hasSubexponentialMGF_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {b : ℝ} {Ω' : Type u_2} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'} {κ : Kernel Ω' Ω} [IsMarkovKernel κ] (h : HasSubexponentialMGF X 0 b κ ν) : ∀ᵐ (ω' : Ω') ∂ν, X =ᵐ[κ ω'] 0

theorem ProbabilityTheory.exp_le_one_add_add_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) : Real.exp x ≤ 1 + x + 3 / 4 * x ^ 2

Second-order bound on the exponential on [-1, 1], from Real.exp_bound.

theorem ProbabilityTheory.hasSubexponentialMGF_of_abs_le_of_integral_eq_zero {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] {M v : ℝ} (hm : AEMeasurable X μ) (hM : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ M) (hc : ∫ (x : Ω), X x ∂μ = 0) (hv : ∫ (x : Ω), (X ^ 2) x ∂μ ≤ v) : HasSubexponentialMGF X (3 * v / 2) M μ

If |X| ≤ M almost surely, X is centered and μ[X ^ 2] ≤ v, then X has a sub-exponential mgf with parameters (3 * v / 2, M).

theorem ProbabilityTheory.hasSubexponentialMGF_sub_integral_of_abs_le {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] {M : ℝ} (hm : AEMeasurable X μ) (hM : ∀ᵐ (ω : Ω) ∂μ, |X ω| ≤ M) : HasSubexponentialMGF (fun (ω : Ω) => X ω - ∫ (x : Ω), X x ∂μ) (3 * variance X μ / 2) (2 * M) μ

If |X| ≤ M almost surely, then X - μ[X] has a sub-exponential mgf with parameters (3 * Var[X] / 2, 2 * M).

theorem ProbabilityTheory.HasSubexponentialMGF.add_of_hasCondSubexponentialMGF {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {b : ℝ} [StandardBorelSpace Ω] [MeasureTheory.IsFiniteMeasure μ] {Y : Ω → ℝ} {VX VY : ℝ} (hm : m ≤ mΩ) (hX : HasSubexponentialMGF X VX b (μ.trim hm)) (hY : HasCondSubexponentialMGF m hm Y VY b μ) : HasSubexponentialMGF (X + Y) (VX + VY) b μ

If X is sub-exponential with parameters (VX, b) with respect to the restriction of μ to a sub-sigma-algebra m and Y is conditionally sub-exponential with parameters (VY, b) with respect to m and μ then X + Y is sub-exponential with parameters (VX + VY, b) with respect to μ.

HasSubexponentialMGF X VX b (μ.trim hm) can be obtained from HasSubexponentialMGF X VX b μ if X is m-measurable. See HasSubexponentialMGF.trim.

theorem ProbabilityTheory.HasSubexponentialMGF.sum_of_hasCondSubexponentialMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} [StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ} {VY : ℕ → ℝ} {ℱ : MeasureTheory.Filtration ℕ mΩ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_adapted : MeasureTheory.Adapted ℱ Y) (h0 : HasSubexponentialMGF (Y 0) (VY 0) b μ) (n : ℕ) (h_sub : ∀ i < n - 1, HasCondSubexponentialMGF (↑ℱ i) ⋯ (Y (i + 1)) (VY (i + 1)) b μ) : HasSubexponentialMGF (fun (ω : Ω) => ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, VY i) b μ

Let Y be a random process adapted to a filtration ℱ, such that for all i : ℕ, Y i is conditionally sub-exponential with parameters (VY i, b) with respect to ℱ (i - 1). In particular, n ↦ ∑ i ∈ range n, Y i is a martingale. Then the sum ∑ i ∈ range n, Y i is sub-exponential with parameters (∑ i ∈ range n, VY i, b).

theorem ProbabilityTheory.measure_sum_ge_le_of_hasCondSubexponentialMGF {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {b : ℝ} [StandardBorelSpace Ω] {Y : ℕ → Ω → ℝ} {VY : ℕ → ℝ} {ℱ : MeasureTheory.Filtration ℕ mΩ} [MeasureTheory.IsZeroOrProbabilityMeasure μ] (h_adapted : MeasureTheory.Adapted ℱ Y) (h0 : HasSubexponentialMGF (Y 0) (VY 0) b μ) (n : ℕ) (h_sub : ∀ i < n - 1, HasCondSubexponentialMGF (↑ℱ i) ⋯ (Y (i + 1)) (VY (i + 1)) b μ) {t : ℝ} (ht : 0 ≤ t) : μ.real {ω : Ω | t ≤ ∑ i ∈ Finset.range n, Y i ω} ≤ Real.exp (-min (t ^ 2 / (2 * ∑ i ∈ Finset.range n, VY i)) (t / (2 * b)))

Bernstein-type inequality for sums of conditionally sub-exponential random variables.