-- Mathlib/Probability/StrongLaw.lean
theorem tsum_prob_mem_Ioi_lt_top {X : Ω → ℝ} (hint : Integrable X) (hnonneg : 0 ≤ X) :
    (∑' j : ℕ, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)}) < ∞

Proof state:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
N : ℕ
hN : N ∈ Set.Ici K
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
exact sum_prob_mem_Ioc_le hint hnonneg hN

Result:
no goals

Proof state:
case hm
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Monotone fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro m n hmn x hx

Result:
case hm
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
m n : ℕ
hmn : m ≤ n
x : Ω
hx : x ∈ (fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}) m
⊢ x ∈ (fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}) n

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} ⊆ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro ω hω

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
⊢ (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) ≤ᶠ[atTop] fun x => ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
filter_upwards [Ici_mem_atTop K] with N hN

Result:
case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
N : ℕ
hN : N ∈ Set.Ici K
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
⊢ ∀ (K : ℕ), ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
intro K

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
apply le_of_tendsto_of_tendsto A tendsto_const_nhds

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
A : Tendsto (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) atTop (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j}))
⊢ (fun N => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N}) ≤ᶠ[atTop] fun x => ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
apply Set.Subset.antisymm _ _

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ {ω | X ω ∈ Set.Ioi ↑i} ⊆ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
⊢ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N} ⊆ {ω | X ω ∈ Set.Ioi ↑i}

Proof state:
case intro
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
N : ℕ
hN : X ω ≤ ↑N
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
exact Set.mem_iUnion.2 ⟨N, hω, hN⟩

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Tendsto (fun N => ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ {ω | X ω ∈ Set.Ioi ↑i}))

Tactic:
rw [this]

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Tendsto (fun N => ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ (⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N})))

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)

Result:
case intro
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
ω : Ω
hω : ω ∈ {ω | X ω ∈ Set.Ioi ↑i}
N : ℕ
hN : X ω ≤ ↑N
⊢ ω ∈ ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
⊢ ∑' (j : ℕ), ℙ {ω | X ω ∈ Set.Ioi ↑j} < ⊤

Tactic:
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

Result:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
⊢ ∀ (K : ℕ), ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Proof state:
case hm
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
m n : ℕ
hmn : m ≤ n
x : Ω
hx : x ∈ (fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}) m
⊢ x ∈ (fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}) n

Tactic:
exact ⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Tendsto (fun N => ℙ {ω | X ω ∈ Set.Ioc ↑i ↑N}) atTop (𝓝 (ℙ (⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N})))

Tactic:
apply tendsto_measure_iUnion_atTop

Result:
case hm
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Monotone fun N => {ω | X ω ∈ Set.Ioc ↑i ↑N}