α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ↑↑count {i | ↑ε ≤ (ENNReal.some ∘ a) i} ≤ ↑c / ↑ε
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ↑↑count {i | ε ≤ a i} ≤ ↑c / ↑ε
rw [show (fun i => ε ≤ a i) = fun i => (ε : ℝ≥0∞) ≤ ((↑) ∘ a) i by
    funext i
    simp only [ENNReal.coe_le_coe, Function.comp]]
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (∑' (i : α), (ENNReal.some ∘ a) i) ≤ ↑c
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ↑↑count {i | ↑ε ≤ (ENNReal.some ∘ a) i} ≤ ↑c / ↑ε
apply
  ENNReal.count_const_le_le_of_tsum_le (measurable_coe_nnreal_ennreal.comp a_mble) _
    (by exact_mod_cast ε_ne_zero) (@ENNReal.coe_ne_top ε)
case h.e'_3
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (∑' (i : α), (ENNReal.some ∘ a) i) = ↑(∑' (i : α), a i)
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (∑' (i : α), (ENNReal.some ∘ a) i) ≤ ↑c
convert ENNReal.coe_le_coe.mpr tsum_le_c
no goals
case h.e'_3
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (∑' (i : α), (ENNReal.some ∘ a) i) = ↑(∑' (i : α), a i)
erw [ENNReal.tsum_coe_eq a_summable.hasSum]
case h
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
i : α
⊢ (ε ≤ a i) = (↑ε ≤ (ENNReal.some ∘ a) i)
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ (fun i => ε ≤ a i) = fun i => ↑ε ≤ (ENNReal.some ∘ a) i
funext i
no goals
case h
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
i : α
⊢ (ε ≤ a i) = (↑ε ≤ (ENNReal.some ∘ a) i)
simp only [ENNReal.coe_le_coe, Function.comp]
no goals
α : Type u_1
β : Type ?u.1696412
γ : Type ?u.1696415
δ : Type ?u.1696418
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0
a_mble : Measurable a
a_summable : Summable a
c : ℝ≥0
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0
ε_ne_zero : ε ≠ 0
⊢ ↑ε ≠ 0
exact_mod_cast ε_ne_zero