English
Under IsFiniteMeasure μ and a < b, the integral inequality (b − a) μ[upcrossingsBefore a b f N] ≤ μ[(f N ω − a)⁺] holds, via an auxiliary lemma.
Русский
При конечной мере μ и a < b выполняется неравенство интегралов, используя вспомогательную лемму.
LaTeX
$$$ (b - a) \\cdot \\mu[\\mathrm{upcrossingsBefore}(a,b,f,N)] \\le \\mu[\\lambda \\omega. (f(N,\\omega) - a)^{+}] $$$
Lean4
theorem integral_mul_upcrossingsBefore_le_integral [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ) (hfN : ∀ ω, a ≤ f N ω)
(hfzero : 0 ≤ f 0) (hab : a < b) : (b - a) * μ[upcrossingsBefore a b f N] ≤ μ[f N] :=
calc
(b - a) * μ[upcrossingsBefore a b f N] ≤ μ[∑ k ∈ Finset.range N, upcrossingStrat a b f N k * (f (k + 1) - f k)] :=
by
rw [← integral_const_mul]
refine integral_mono_of_nonneg ?_ ((hf.sum_upcrossingStrat_mul a b N).integrable N) ?_
· exact Eventually.of_forall fun ω => mul_nonneg (sub_nonneg.2 hab.le) (Nat.cast_nonneg _)
· filter_upwards with ω
simpa using mul_upcrossingsBefore_le (hfN ω) hab
_ ≤ μ[f N] - μ[f 0] := hf.sum_mul_upcrossingStrat_le
_ ≤ μ[f N] := (sub_le_self_iff _).2 (integral_nonneg hfzero)
