English
The tail sums of the upper tails of X are finite: sum_j P(X ∈ (j, ∞)) < ∞.
Русский
Сумма хвостов распределения P(X ∈ (j, ∞)) конечна.
LaTeX
$$$\sum_{j=0}^{\infty} \mathbb{P}(X \in (j, \infty)) < \infty$$$
Lean4
theorem tsum_prob_mem_Ioi_lt_top {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) :
(∑' j : ℕ, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)}) < ∞ :=
by
suffices ∀ K : ℕ, ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)} ≤ ENNReal.ofReal (𝔼[X] + 1) from
(le_of_tendsto_of_tendsto (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds (Eventually.of_forall this)).trans_lt
ENNReal.ofReal_lt_top
intro K
have A :
Tendsto (fun N : ℕ => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N}) atTop
(𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)})) :=
by
refine tendsto_finset_sum _ fun i _ => ?_
have : {ω | X ω ∈ Set.Ioi (i : ℝ)} = ⋃ N : ℕ, {ω | X ω ∈ Set.Ioc (i : ℝ) N} :=
by
apply Set.Subset.antisymm _ _
· intro ω hω
obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
· simp +contextual only [Set.mem_Ioc, Set.mem_Ioi, Set.iUnion_subset_iff, Set.setOf_subset_setOf, imp_true_iff]
rw [this]
apply tendsto_measure_iUnion_atTop
intro m n hmn x hx
exact ⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩
apply le_of_tendsto_of_tendsto A tendsto_const_nhds
filter_upwards [Ici_mem_atTop K] with N hN
exact sum_prob_mem_Ioc_le hint hnonneg hN
