English
Let a: α → ℝ≥0∞ be measurable, with ∑' i, a(i) ≤ c for some c ∈ ℝ≥0∞. For ε ∈ ℝ≥0∞ with ε ≠ 0 and ε ≠ ∞, the counting measure of the set {i : ε ≤ a(i)} is at most c/ε.
Русский
Пусть a: α → ℝ≥0∞ измерима, и сумма по всем i удовлетворяет ∑' i, a(i) ≤ c. Тогда записываемое множество {i | ε ≤ a(i)} имеет размерность не более c/ε, при любых ε ≠ 0, ∞.
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_.ENNReal.count_const_le_le_of_tsum_le [MeasurableSingletonClass α] {a : α → ℝ≥0∞} (a_mble : Measurable a)
{c : ℝ≥0∞} (tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) (ε_ne_top : ε ≠ ∞) :
Measure.count {i : α | ε ≤ a i} ≤ c / ε :=
by
rw [← lintegral_count] at tsum_le_c
apply (MeasureTheory.meas_ge_le_lintegral_div a_mble.aemeasurable ε_ne_zero ε_ne_top).trans
exact ENNReal.div_le_div tsum_le_c rfl.le
