Markov's inequality for finite sums

If a nonnegative function f on a finite set s is at least m on {x ∈ s | p x}, then m times the cardinality of that subset is at most ∑ x ∈ s, f x (Finset.mul_card_filter_le_sum, Finset.card_filter_mul_le_sum).

Main results

• Finset.mul_card_filter_le_sum: m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x for f : α → ℕ.
• Finset.card_filter_mul_le_sum: (#{x ∈ s | p x} : R) * m ≤ ∑ x ∈ s, f x for 0 ≤ f x.

theorem Finset.card_filter_mul_le_sum {α : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsOrderedAddMonoid R] (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → R) {m : R} (hf : ∀ x ∈ s, 0 ≤ f x) (hm : ∀ x ∈ s, p x → m ≤ f x) : ↑{x ∈ s | p x}.card * m ≤ ∑ x ∈ s, f x

Markov's inequality for a nonnegative Finset sum: if 0 ≤ f x on s and m ≤ f x whenever x ∈ s satisfies p x, then #{x ∈ s | p x} * m ≤ ∑ x ∈ s, f x.

theorem Finset.mul_card_filter_le_sum {α : Type u_1} (s : Finset α) (p : α → Prop) [DecidablePred p] (f : α → ℕ) {m : ℕ} (hm : ∀ x ∈ s, p x → m ≤ f x) : m * {x ∈ s | p x}.card ≤ ∑ x ∈ s, f x

Markov's inequality for a Finset sum: if m ≤ f x whenever x ∈ s satisfies p x, then m * #{x ∈ s | p x} ≤ ∑ x ∈ s, f x.