α : Type u_1
β : Type ?u.1695258
γ : Type ?u.1695261
δ : Type ?u.1695264
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c✝ : (∑' (i : α), a i) ≤ c
tsum_le_c : (∫⁻ (a_1 : α), a a_1 ∂count) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ ↑↑count {i | ε ≤ a i} ≤ c / ε
α : Type u_1
β : Type ?u.1695258
γ : Type ?u.1695261
δ : Type ?u.1695264
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c : (∑' (i : α), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ ↑↑count {i | ε ≤ a i} ≤ c / ε
rw [← lintegral_count] at tsum_le_c
α : Type u_1
β : Type ?u.1695258
γ : Type ?u.1695261
δ : Type ?u.1695264
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c✝ : (∑' (i : α), a i) ≤ c
tsum_le_c : (∫⁻ (a_1 : α), a a_1 ∂count) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
α : Type u_1
β : Type ?u.1695258
γ : Type ?u.1695261
δ : Type ?u.1695264
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c✝ : (∑' (i : α), a i) ≤ c
tsum_le_c : (∫⁻ (a_1 : α), a a_1 ∂count) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ ↑↑count {i | ε ≤ a i} ≤ c / ε
apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans
no goals
α : Type u_1
β : Type ?u.1695258
γ : Type ?u.1695261
δ : Type ?u.1695264
m : MeasurableSpace α
μ ν : Measure α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
a : α → ℝ≥0∞
a_mble : Measurable a
c : ℝ≥0∞
tsum_le_c✝ : (∑' (i : α), a i) ≤ c
tsum_le_c : (∫⁻ (a_1 : α), a a_1 ∂count) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
ε_ne_top : ε ≠ ⊤
⊢ (∫⁻ (a_1 : α), a a_1 ∂count) / ε ≤ c / ε
exact ENNReal.div_le_div tsum_le_c rfl.le