mul_integral_upcrossingsBefore_le_integral_pos_part_aux

English

Under IsFiniteMeasure μ and f a submartingale, the inequality μ[upcrossingsBefore a b f N] ≤ μ[upcrossingsBefore a b f N] holds after integrating the product with (b−a).

Русский

Для конечной меры и субмартингейла неравенство сохраняется после интегрирования по произведению.

LaTeX

$$$$ (b-a) \\cdot \\mu[\\mathrm{upcrossingsBefore}(a,b,f,N)] \\le \\mu[\\int (f(N,\\omega)-a)^{+} d\\omega]. $$$$

Lean4

theorem mul_integral_upcrossingsBefore_le_integral_pos_part_aux [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (hab : a < b) : (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[fun ω => (f N ω - a)⁺] :=
  by
  refine
    le_trans (le_of_eq ?_)
      (integral_mul_upcrossingsBefore_le_integral (hf.sub_martingale (martingale_const _ _ _)).pos
        (fun ω => posPart_nonneg _) (fun ω => posPart_nonneg _) (sub_pos.2 hab))
  simp_rw [sub_zero, ← upcrossingsBefore_pos_eq hab]
  rfl

Похожие утверждения