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

Stream: new members

[Kalle Kytölä]

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ä]

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ä]

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ä]

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ä]

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

[Kalle Kytölä]

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]

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

and the following might help:
docs#ennreal.sum_le_tsum
docs#finset.sum_le_sum
docs#finset.sum_const
docs#set.finite.to_finset
docs#set.finite_or_infinite
docs#set.infinite.exists_subset_card_eq

[Kalle Kytölä]

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ä]

...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,
  { by_contradiction con,
    simpa only [@measure.count_apply_infinite ι _ ⊤ con, top_le_iff, ennreal.coe_ne_top]
      using key, },
  rw @measure.count_apply_finite ι ⊤ _ _ hf at key,
  use hf,
  exact_mod_cast key,
end

But I don't particularly enjoy carrying around the finiteness proof to even be able to write the cardinality. This is one reason why the counting measure seems nicer. Another reason is that one can apply the existing Markov's inequality right away.