English
Hoeffding's lemma: if X is integrable and almost surely lies in [a,b] and has zero mean under μ, then HasSubgaussianMGF X with parameter ((|b-a|_+)/2)^2.
Русский
Лемма Хоффdinga: если X интегрируем и почти surely лежит в [a,b] и имеет нулевое математическое ожидание по μ, то HasSubgaussianMGF X c с c=((|b-a|_+)/2)^2.
LaTeX
$$$[IsProbabilityMeasure\, \mu] \Rightarrow \forall a,b, hm,AEMeasurable(X,\mu), hb,hc,ht\; \mathrm{HasSubgaussianMGF}(X, ((|b-a|)_+/2)^2,\mu)$$$
Lean4
/-- **Hoeffding's lemma**: with respect to a probability measure `μ`, if `X` is a random variable
that has expectation zero and is almost surely in `Set.Icc a b` for some `a ≤ b`, then `X` has a
sub-Gaussian moment-generating function with parameter `((b - a) / 2) ^ 2`. -/
theorem hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero [IsProbabilityMeasure μ] {a b : ℝ} (hm : AEMeasurable X μ)
(hb : ∀ᵐ ω ∂μ, X ω ∈ Set.Icc a b) (hc : μ[X] = 0) : HasSubgaussianMGF X ((‖b - a‖₊ / 2) ^ 2) μ
where
integrable_exp_mul t := integrable_exp_mul_of_mem_Icc hm hb
mgf_le
t := by
obtain ht | ht | ht := lt_trichotomy 0 t
· exact ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero hm hb hc ht
· simp [← ht]
calc
_ = mgf (-X) μ (-t) := by simp [mgf]
_ ≤ exp ((‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2) :=
by
apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
· filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
· rw [integral_neg, hc, neg_zero]
· rwa [Left.neg_pos_iff]
_ = exp (((‖b - a‖₊ / 2) ^ 2) * t ^ 2 / 2) := by ring_nf
