English
If HasSubgaussianMGF X 0 μ, then X equals zero μ-almost everywhere.
Русский
Если HasSubgaussianMGF X 0 μ, то X равно нулю μ-почти везде.
LaTeX
$$$\mathrm{HasSubgaussianMGF}(X,0,\mu) \Rightarrow X =_{\mu}^{ae} 0$$$
Lean4
/-- Let `Y` be a random process adapted to a filtration `ℱ`, such that for all `i : ℕ`, `Y i` is
conditionally sub-Gaussian with parameter `cY i` 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-Gaussian with parameter `∑ i ∈ range n, cY i`. -/
theorem HasSubgaussianMGF_sum_of_HasCondSubgaussianMGF [IsZeroOrProbabilityMeasure μ] (h_adapted : Adapted ℱ Y)
(h0 : HasSubgaussianMGF (Y 0) (cY 0) μ) (n : ℕ)
(h_subG : ∀ i < n - 1, HasCondSubgaussianMGF (ℱ i) (ℱ.le i) (Y (i + 1)) (cY (i + 1)) μ) :
HasSubgaussianMGF (fun ω ↦ ∑ i ∈ Finset.range n, Y i ω) (∑ i ∈ Finset.range n, cY i) μ := by
induction n with
| zero => simp
| succ n hn =>
induction n with
| zero => simp [h0]
| succ n =>
specialize hn fun i hi ↦ h_subG i (by cutsat)
simp_rw [Finset.sum_range_succ _ (n + 1)]
refine HasSubgaussianMGF_add_of_HasCondSubgaussianMGF (ℱ.le n) ?_ (h_subG n (by cutsat))
refine HasSubgaussianMGF.trim (ℱ.le n) ?_ hn
refine Finset.measurable_fun_sum (Finset.range (n + 1)) fun m hm ↦ ((h_adapted m).mono (ℱ.mono ?_)).measurable
simp only [Finset.mem_range] at hm
cutsat
