English
Let a: α → NNReal be measurable, Summable, and with ∑' i, a(i) ≤ c for some c ∈ NNReal. For ε ≠ 0, the counting measure of {i : ε ≤ a(i)} is bounded by c/ε.
Русский
Пусть a: α → NNReal измерима, суммируема и имеет ∑' i, a(i) ≤ c. Тогда для ε ≠ 0 верно bound: число индексов i, где ε ≤ a(i), не превосходит c/ε.
LaTeX
$$$\operatorname{count} \{i : ε \le a(i)\} \le c / ε$$$
Lean4
/-- Markov's inequality for the counting measure with hypothesis using `tsum` in `ℝ≥0`. -/
theorem _root_.NNReal.count_const_le_le_of_tsum_le [MeasurableSingletonClass α] {a : α → ℝ≥0} (a_mble : Measurable a)
(a_summable : Summable a) {c : ℝ≥0} (tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0} (ε_ne_zero : ε ≠ 0) :
Measure.count {i : α | ε ≤ a i} ≤ c / ε :=
by
rw [show (fun i => ε ≤ a i) = fun i => (ε : ℝ≥0∞) ≤ ((↑) ∘ a) i by simp only [ENNReal.coe_le_coe, Function.comp]]
apply
ENNReal.count_const_le_le_of_tsum_le (measurable_coe_nnreal_ennreal.comp a_mble) _ (mod_cast ε_ne_zero)
(@ENNReal.coe_ne_top ε)
convert ENNReal.coe_le_coe.mpr tsum_le_c
simp_rw [Function.comp_apply]
rw [ENNReal.tsum_coe_eq a_summable.hasSum]
