English
For a finite measure μ and a real-valued Submartingale f with respect to filtration ℱ, the Doob upcrossing inequality yields a bound: (b − a) ∫ upcrossings ≤ sup_N ∫ (f_N − a)^+.
Русский
Для конечной меры μ и подмартингейла f относительно фильтрации ℱ выполняется неравенство Доуба для upcrossings: (b−a)∫ upcrossings ≤ sup_N ∫ (f_N − a)^+.
LaTeX
$$$(b-a) \int_{\Omega} upcrossings(a,b,f)(\omega) \, d\mu(\omega) \le \sup_{N} \int_{\Omega} (f(N,\omega) - a)^{+} \, d\mu(\omega)$$$
Lean4
/-- A variant of Doob's upcrossing estimate obtained by taking the supremum on both sides. -/
theorem mul_lintegral_upcrossings_le_lintegral_pos_part [IsFiniteMeasure μ] (a b : ℝ) (hf : Submartingale f ℱ μ) :
ENNReal.ofReal (b - a) * ∫⁻ ω, upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ ω, ENNReal.ofReal ((f N ω - a)⁺) ∂μ :=
by
by_cases hab : a < b
· simp_rw [upcrossings]
have : ∀ N, ∫⁻ ω, ENNReal.ofReal ((f N ω - a)⁺) ∂μ = ENNReal.ofReal (∫ ω, (f N ω - a)⁺ ∂μ) :=
by
intro N
rw [ofReal_integral_eq_lintegral_ofReal]
· exact (hf.sub_martingale (martingale_const _ _ _)).pos.integrable _
· exact Eventually.of_forall fun ω => posPart_nonneg _
rw [lintegral_iSup']
· simp_rw [this, ENNReal.mul_iSup, iSup_le_iff]
intro N
rw [(by simp : ∫⁻ ω, upcrossingsBefore a b f N ω ∂μ = ∫⁻ ω, ↑(upcrossingsBefore a b f N ω : ℝ≥0) ∂μ),
lintegral_coe_eq_integral, ← ENNReal.ofReal_mul (sub_pos.2 hab).le]
· simp_rw [NNReal.coe_natCast]
exact
(ENNReal.ofReal_le_ofReal (hf.mul_integral_upcrossingsBefore_le_integral_pos_part a b N)).trans
(le_iSup (α := ℝ≥0∞) _ N)
· simp only [NNReal.coe_natCast, hf.adapted.integrable_upcrossingsBefore hab]
· exact fun n => measurable_from_top.comp_aemeasurable (hf.adapted.measurable_upcrossingsBefore hab).aemeasurable
· filter_upwards with ω N M hNM
rw [Nat.cast_le]
exact upcrossingsBefore_mono hab hNM ω
· rw [not_lt, ← sub_nonpos] at hab
rw [ENNReal.ofReal_of_nonpos hab, zero_mul]
exact zero_le _
