English
Markov-type inequality: if a tsum of a_i is ≤ c and ε>0, then there is a finite set of indices where ε≤a_i whose cardinal is ≤ c/ε.
Русский
Неравенство Маркова: если сумма ∑ a_i ≤ c и ε>0, то существует конечное подмножество индексов, где a_i ≥ ε, обладающее размерностью ≤ c/ε.
LaTeX
$$$c\\neq \\infty$ and $\\sum' a_i \\le c$ and $ε>0$ imply ∃hf.{i|ε≤a_i}.Finite with #hf ≤ c/ε$$
Lean4
/-- Markov's inequality for `Finset.card` and `tsum` in `ℝ≥0∞`. -/
theorem finset_card_const_le_le_of_tsum_le {ι : Type*} {a : ι → ℝ≥0∞} {c : ℝ≥0∞} (c_ne_top : c ≠ ∞)
(tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) :
∃ hf : {i : ι | ε ≤ a i}.Finite, #hf.toFinset ≤ c / ε :=
by
have hf : {i : ι | ε ≤ a i}.Finite :=
finite_const_le_of_tsum_ne_top (ne_top_of_le_ne_top c_ne_top tsum_le_c) ε_ne_zero
refine ⟨hf, (ENNReal.le_div_iff_mul_le (.inl ε_ne_zero) (.inr c_ne_top)).2 ?_⟩
calc
#hf.toFinset * ε = ∑ _i ∈ hf.toFinset, ε := by rw [Finset.sum_const, nsmul_eq_mul]
_ ≤ ∑ i ∈ hf.toFinset, a i := (Finset.sum_le_sum fun i => hf.mem_toFinset.1)
_ ≤ ∑' i, a i := (ENNReal.sum_le_tsum _)
_ ≤ c := tsum_le_c
