## Stream: new members

### Topic: bounding the number (cardinality) of large terms in a sum

#### Kalle Kytölä (Jul 20 2022 at 08:37):

I have had difficulties with the following types of arguments in Lean many times.

Suppose $(a_i)_{i \in I}$ are nonnegative, $a_i \ge 0$ for all $i \in I$, and their (topological) sum is at most $c < \infty$, i.e.,

$\sum_{i \in I} a_i \le c < \infty .$

Obviously for any $\varepsilon > 0$, the number of terms that are at least $\varepsilon$ is at most $c / \varepsilon$, i.e.,

$\# \big\{ i \in I \; \big| \; a_i \ge \varepsilon \big\} \; \le \; \frac{c}{\varepsilon}.$

(Here $\#$ means any reasonable interpretation of the cardinality so that we can write a comparison with the right hand side $c/\varepsilon \in [0,+\infty]$. :grinning:)

#### Kalle Kytölä (Jul 20 2022 at 08:38):

I tried many spellings of cardinalities in Lean, but always got stuck somewhere. Interestingly, I also did not find this result (or anything closely related) in mathlib! (This seems basic enough to exist, no?)

My main question is: how to idiomatically state this obvious fact in Lean? And a second question: does it exist and did I just miss it?

#### Kalle Kytölä (Jul 20 2022 at 08:39):

For reference, below is one horrendous spelling of it. (Absolutely ridiculous spelling in the second lemma below! Of course changing the spelling to the contrapositive is possible but equally ridiculous.)

So a way of phrasing the question is: what should I write below instead?

import topology.instances.ennreal

noncomputable theory
open set function
open_locale ennreal nnreal

lemma ennreal.tsum_const_ge_of_card_ge
{ι : Type*} (c : ℝ≥0∞) {n : ℕ} (card_ge_n : ∃ e : fin n → ι, injective e) :
↑n * c ≤ (∑' (i : ι), c) :=
begin
rcases card_ge_n with ⟨e, e_inj⟩,
convert tsum_le_tsum_of_inj e e_inj (λ _ _, zero_le _) _
(show summable (λ (k : fin n), c), from ennreal.summable)
(show summable (λ (i : ι), c), from ennreal.summable),
swap, { exact λ _, rfl.le, },
rw tsum_fintype,
simp only [finset.sum_const, finset.card_fin, nsmul_eq_mul],
end

lemma ennreal.card_const_le_le_of_tsum_le {ι : Type*} (a : ι → ℝ≥0∞)
{c : ℝ≥0∞} (c_ne_top : c ≠ ∞) (h : ∑' i, a i ≤ c) {ε : ℝ≥0∞} (ε_pos : 0 < ε) (ε_ne_top : ε ≠ ∞) :
∀ (n : ℕ), c / ε < n → ¬ (∃ e : fin n → {i : ι | ε ≤ a i}, injective e) :=
begin
intros n hn con,
rcases con with ⟨e, e_inj⟩,
set a' := indicator {i : ι | ε ≤ a i} (λ _, ε) with def_a',
have a'_le_a : ∀ i, a' i ≤ a i,
{ intro i,
by_cases ind : i ∈ {i : ι | ε ≤ a i},
{ simp only [def_a', ind, indicator_of_mem],
exact ind, },
{ simp only [def_a', ind, indicator_of_not_mem, not_false_iff, zero_le], }, },
have lower_bound := tsum_le_tsum a'_le_a ennreal.summable ennreal.summable,
have bound_on_lower_bound := lower_bound.trans h,
rw (show (∑' i, a' i) = (∑' (i : {i : ι | ε ≤ a i}), ε), by rw ← tsum_subtype)
at bound_on_lower_bound,
have oops := (ennreal.tsum_const_ge_of_card_ge ε ⟨e, e_inj⟩).trans bound_on_lower_bound,
have c_lt : c < n * ε,
{ convert (ennreal.mul_lt_mul_right ε_pos.ne.symm ε_ne_top).mpr hn,
rw ennreal.div_mul_cancel ε_pos.ne.symm ε_ne_top, },
exact lt_irrefl c (lt_of_lt_of_le c_lt oops),
end


#### Kalle Kytölä (Jul 20 2022 at 08:41):

I just realized I had not tried counting measure and Markov inequality. :face_palm:

I expected cardinalities to be the way to go...

#### Kalle Kytölä (Jul 20 2022 at 08:43):

Is counting measure the canonical spelling of cardinality in these types of settings?

#### Kalle Kytölä (Jul 20 2022 at 09:07):

With docs#measure_theory.lintegral_count, one can convert tsums to integrals, and one should be able to use Markov's inequality as usually in measure theory.

But for this purpose, are we missing the following instance? (I'm assuming that one would usually want to use the counting measure on the finest possible sigma algebra (⊤ : measurable_space ι) when converting to tsum).

instance measurable_space.top.measurable_singleton_class {ι : Type*} :
@measurable_singleton_class ι (⊤ : measurable_space ι) :=
{ measurable_set_singleton := λ i, measurable_space.measurable_set_top, }


#### Junyan Xu (Jul 20 2022 at 15:40):

I think this is a reasonable statement:

import topology.instances.ennreal

noncomputable theory
open set function
open_locale ennreal nnreal

lemma ennreal.card_const_le_le_of_tsum_le {ι : Type*} (a : ι → ℝ≥0∞)
(h : ∑' i, a i ≠ ⊤) {ε : ℝ≥0∞} (ε_pos : 0 < ε) :
∃ hf : {i : ι | ε ≤ a i}.finite, ↑hf.to_finset.card ≤ (∑' i, a i) / ε :=
sorry


#### Kalle Kytölä (Jul 22 2022 at 20:59):

Thanks! I now tend to think ( :thinking: :duck:) that the counting measure works a lot better than cardinalities in these types of situations, however. With the one extra measurable_singleton_class instance, one can write for example:

import topology.instances.ennreal
import measure_theory.integral.lebesgue

noncomputable theory
open set function measure_theory
open_locale ennreal nnreal

instance measurable_space.top.measurable_singleton_class {ι : Type*} :
@measurable_singleton_class ι (⊤ : measurable_space ι) :=
{ measurable_set_singleton := λ i, measurable_space.measurable_set_top, }

lemma tsum_eq_lintegral_count_top {ι : Type*} (a : ι → ℝ≥0∞) :
(∑' (i : ι), a i) = ∫⁻ i, a i ∂(@measure.count ι ⊤) :=
by rw lintegral_count

lemma ennreal.tsum_const_eq {ι : Type*} (c : ℝ≥0∞) :
(∑' (i : ι), c) = (@measure.count ι ⊤ (univ : set ι)) * c :=
by rw [tsum_eq_lintegral_count_top, lintegral_const, mul_comm]

lemma ennreal.count_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) (ε_ne_top : ε ≠ ∞) :
@measure.count ι ⊤ {i : ι | ε ≤ a i} ≤ c / ε :=
begin
rw tsum_eq_lintegral_count_top at tsum_le_c,
apply (measure_theory.meas_ge_le_lintegral_div measurable_from_top.ae_measurable ε_ne_zero ε_ne_top).trans,
exact ennreal.div_le_div tsum_le_c rfl.le,
end


#### Kalle Kytölä (Jul 22 2022 at 21:00):

...and for example the cardinality version reduces to this by:

lemma finset_card_const_le_le_of_tsum_le {ι : Type*} (a : ι → ℝ≥0∞)
{c : ℝ≥0} (tsum_le_c : ∑' i, a i ≤ c) {ε : ℝ≥0} (ε_ne_zero : ε ≠ 0) :
∃ hf : {i : ι | ↑ε ≤ a i}.finite, ↑hf.to_finset.card ≤ c / ε :=
begin
have key := ennreal.count_const_le_le_of_tsum_le a ennreal.coe_ne_top tsum_le_c
(ennreal.coe_ne_zero.mpr ε_ne_zero) ennreal.coe_ne_top,
rw ← ennreal.coe_div ε_ne_zero at key,
have hf : {i : ι | ↑ε ≤ a i}.finite,