English
Doob's maximal inequality bounds the tail probability of the running maximum by the last value and a suitable indicator integrable bound.
Русский
Неравенство максимума Дуба ограничивает хвостовую вероятность максимума по последнему значению и соответствующему интегрируемому пределу.
LaTeX
$$$ \\text{maximal inequality: } ε \\cdot μ\\{ω : ε ≤ \\sup_{0≤k≤n} f_k(ω)\\} ≤ ∫_{\\{ε ≤ \\sup_{0≤k≤n} f_k\\}} f_n \; dμ $$$
Lean4
theorem smul_le_stoppedValue_hitting [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) {ε : ℝ≥0} (n : ℕ) :
ε • μ {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω} ≤
ENNReal.ofReal
(∫ ω in {ω | (ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω},
stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω ∂μ) :=
by
have hn : Set.Icc 0 n = {k | k ≤ n} := by ext x; simp
have :
∀ ω,
((ε : ℝ) ≤ (range (n + 1)).sup' nonempty_range_add_one fun k => f k ω) →
(ε : ℝ) ≤ stoppedValue f (hitting f {y : ℝ | ↑ε ≤ y} 0 n) ω :=
by
intro x hx
simp_rw [le_sup'_iff, mem_range, Nat.lt_succ_iff] at hx
refine stoppedValue_hitting_mem ?_
simp only [Set.mem_setOf_eq, hn]
exact
let ⟨j, hj₁, hj₂⟩ := hx
⟨j, hj₁, hj₂⟩
have h :=
setIntegral_ge_of_const_le
(measurableSet_le measurable_const
(Finset.measurable_range_sup'' fun n _ => (hsub.stronglyMeasurable n).measurable.le (𝒢.le n)))
(measure_ne_top _ _) this
(Integrable.integrableOn
(hsub.integrable_stoppedValue (hitting_isStoppingTime hsub.adapted measurableSet_Ici) hitting_le))
rw [ENNReal.le_ofReal_iff_toReal_le, ENNReal.toReal_smul]
· exact h
· exact ENNReal.mul_ne_top (by simp) (measure_ne_top _ _)
· exact le_trans (mul_nonneg ε.coe_nonneg ENNReal.toReal_nonneg) h
