English
Let μ be finite and f a submartingale. Then μ[∑_{k<n} upcrossingStrat(a,b,f,N,k)·(f(k+1)−f(k))] ≤ μ[f_n] − μ[f_0].
Русский
Пусть μ конечна, f — субмартингейл. Тогда интеграл суммы по k<n от upcrossingStrat(a,b,f,N,k)·(f(k+1)−f(k)) не превосходит μ[f_n] − μ[f_0].
LaTeX
$$$\\mu\\left[\\sum_{k=0}^{n-1} \\mathrm{upcrossingStrat}(a,b,f,N,k)\\,(f(k+1)-f(k))\\right] \\le \\mu[f_n] - \\mu[f_0].$$$
Lean4
theorem sum_mul_upcrossingStrat_le [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) :
μ[∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)] ≤ μ[f n] - μ[f 0] :=
by
have h₁ : (0 : ℝ) ≤ μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] :=
by
have := (hf.sum_sub_upcrossingStrat_mul a b N).setIntegral_le (zero_le n) MeasurableSet.univ
rw [setIntegral_univ, setIntegral_univ] at this
refine le_trans ?_ this
simp only [Finset.range_zero, Finset.sum_empty, integral_zero', le_refl]
have h₂ :
μ[∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)] =
μ[∑ k ∈ Finset.range n, (f (k + 1) - f k)] -
μ[∑ k ∈ Finset.range n, upcrossingStrat a b f N k * (f (k + 1) - f k)] :=
by
simp only [sub_mul, one_mul, Finset.sum_sub_distrib, Pi.sub_apply, Finset.sum_apply, Pi.mul_apply]
refine
integral_sub
(Integrable.sub (integrable_finset_sum _ fun i _ => hf.integrable _)
(integrable_finset_sum _ fun i _ => hf.integrable _))
?_
convert (hf.sum_upcrossingStrat_mul a b N).integrable n using 1
ext; simp
rw [h₂, sub_nonneg] at h₁
refine le_trans h₁ ?_
simp_rw [Finset.sum_range_sub, integral_sub' (hf.integrable _) (hf.integrable _), le_refl]
