English
If μ is a finite measure and f is adapted to ℱ with a < b, then the random variable ω ↦ upcrossingsBefore(a, b, f, N, ω) (viewed as a real-valued function) is μ-integrable for every N.
Русский
Если μ — конечная мера и f адаптирован к ℱ при a < b, то случайная величина ω ↦ upcrossingsBefore(a, b, f, N, ω) считается интегрируемой по μ для каждого N.
LaTeX
$$Integrable\left(\lambda \omega. (upcrossingsBefore(a,b,f,N)\,\omega):\mathbb{R}\right)\,\mu$$
Lean4
theorem integrable_upcrossingsBefore [IsFiniteMeasure μ] (hf : Adapted ℱ f) (hab : a < b) :
Integrable (fun ω => (upcrossingsBefore a b f N ω : ℝ)) μ :=
haveI : ∀ᵐ ω ∂μ, ‖(upcrossingsBefore a b f N ω : ℝ)‖ ≤ N :=
by
filter_upwards with ω
rw [Real.norm_eq_abs, Nat.abs_cast, Nat.cast_le]
exact upcrossingsBefore_le _ _ hab
⟨Measurable.aestronglyMeasurable (measurable_from_top.comp (hf.measurable_upcrossingsBefore hab)), .of_bounded this⟩
