English
Under finite measure μ and adapted sets s_n, almost surely the limsup of the indicator sums equals the limsup of the corresponding conditional-expectation sums.
Русский
При конечной мере μ и адаптированных множествах s_n почти surely границы (limsup) сумм индикаторов совпадают с лимитом соответственно условных ожиданий.
LaTeX
$$$ \forall n, MeasurableSet[\mathcal{F}_n](s_n) \Rightarrow \forall^{\mathrm{a.e.}} \omega,\ Tendsto_{n\to\infty} \sum_{k< n} \mathbf{1}_{s_{k+1}}(\omega) =\to\infty \text{ iff } \, \ Tendsto_{n\to\infty} \sum_{k< n} \mathbb{E}[\mathbf{1}_{s_{k+1}}|\mathcal{F}_k](\omega) =\infty. $$$
Lean4
theorem tendsto_sum_indicator_atTop_iff' [IsFiniteMeasure μ] {s : ℕ → Set Ω} (hs : ∀ n, MeasurableSet[ℱ n] (s n)) :
∀ᵐ ω ∂μ,
Tendsto (fun n => ∑ k ∈ Finset.range n, (s (k + 1)).indicator (1 : Ω → ℝ) ω) atTop atTop ↔
Tendsto (fun n => ∑ k ∈ Finset.range n, (μ[(s (k + 1)).indicator (1 : Ω → ℝ)|ℱ k]) ω) atTop atTop :=
by
have :=
tendsto_sum_indicator_atTop_iff (Eventually.of_forall fun ω n => ?_) (adapted_process hs) (integrable_process μ hs)
(Eventually.of_forall <| process_difference_le s)
swap
· rw [process, process, ← sub_nonneg, Finset.sum_apply, Finset.sum_apply, Finset.sum_range_succ_sub_sum]
exact Set.indicator_nonneg (fun _ _ => zero_le_one) _
simp_rw [process, predictablePart_process_ae_eq] at this
simpa using this
