[Merged by Bors] - feat(measure_theory/integral/lebesgue): Add Markov inequalities for tsum and card using counting measure.

[kkytola]

Add Markov inequalities for tsum and finset.card using the counting measure to translate the Markov inequality from measure theory to these.

---

I don't know if it is considered bad to do cardinality proofs via importing measure theory. But I tend to believe the measure theory library is very convenient to use compared to cardinalities directly, so I'd prefer to allow this. Markov's inequality is an example of where I think there is a small advantage, but other tools including convergence theorems will be convenient to translate from lintegrals to tsums.

Perhaps the reviewers can comment on whether this import-heavy approach is acceptable/desirable at all.

[fpvandoorn]

I am not happy that these proofs about tsum are done using measure theory, and it's definitely not good that they are in the measure theory library (instead of in a file topology/algebra/infinite_sum/something).
Since similar arguments are already in mathlib without using measure theory, can you try to mimic/use those arguments?

[sgouezel]

I don't mind having some inequalities on infinite sums depending on measure theory, as it's often the most efficient way to prove them. But the file containing these inequalities should definitely not be in the measure_theory folder, if the statements of the inequalities don't involve measures. Could you create a new file (next to already existing files in the topology folder on infinite sums) for the results whose statements do not mention measures?
(And in this way, if someone wants to refactor later the proof to give direct elementary proofs, this shouldn't break anything).

[kkytola]

I don't mind having some inequalities on infinite sums depending on measure theory, as it's often the most efficient way to prove them. ...

Unsurprisingly, I wholeheartedly agree with this! (And besides many inequalities, something like a dominated convergence for summation would be an easy consequence of measure theory but not nice to develop from scratch).

... (And in this way, if someone wants to refactor later the proof to give direct elementary proofs, this shouldn't break anything).

For the last statements of this PR of Markov's inequality which don't have counting measure in the hypotheses or the conclusion, I can actually refactor right away and make these not use measure theory --- proposal below (golfs welcome!). I think the proofs are slightly worse, but the imports are lighter. Unless someone disagrees, I could switch to these and put them in the appropriate files for now. (I mainly care about unblocking the remaining portmanteau implications, so I would settle for the least controversial approach and argue about measure theory or not later.)

import topology.instances.ennreal

noncomputable theory

open set ennreal nnreal
open_locale ennreal nnreal

variables {X : Type*}

open_locale topological_space

/-- A sum of extended nonnegative reals which is finite can have only finitely many terms
above any positive threshold.-/
lemma _root_.ennreal.finite_const_le_of_tsum_ne_top {X : Type*} {a : X → ℝ≥0∞}
  (tsum_ne_top : ∑' i, a i ≠ ∞) {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) :
  {i : X | ε ≤ a i}.finite :=
begin
  by_cases ε_infty : ε = ∞,
  { rw ε_infty,
    by_contra maybe_infinite,
    obtain ⟨j, hj⟩ := set.infinite.nonempty maybe_infinite,
    exact tsum_ne_top (le_antisymm le_top (le_trans hj (le_tsum' (@ennreal.summable _ a) j))), },
  have key := (summable_coe.mpr (summable_to_nnreal_of_tsum_ne_top tsum_ne_top)).tendsto_cofinite_zero
              (Iio_mem_nhds (to_real_pos ε_ne_zero ε_infty)),
  simp only [filter.mem_map, filter.mem_cofinite, preimage] at key,
  have obs : {i : X | ↑((a i).to_nnreal) ∈ Iio ε.to_real}ᶜ = {i : X | ε ≤ a i},
  { ext i,
    simpa only [mem_Iio, mem_compl_iff, mem_set_of_eq, not_lt]
      using to_real_le_to_real ε_infty (ennreal.ne_top_of_tsum_ne_top tsum_ne_top _), },
  rwa obs at key,
end

/-- Markov's inequality for `finset.card` and `tsum` in `ℝ≥0∞`. -/
lemma _root_.ennreal.finset_card_const_le_le_of_tsum_le {X : Type*} {a : X → ℝ≥0∞}
  {c : ℝ≥0∞} (c_ne_top : c ≠ ∞) (tsum_le_c : ∑' i, a i ≤ c)
  {ε : ℝ≥0∞} (ε_ne_zero : ε ≠ 0) :
  ∃ hf : {i : X | ε ≤ a i}.finite, ↑hf.to_finset.card ≤ c / ε :=
begin
  by_cases ε = ∞,
  { have obs : {i : X | ε ≤ a i} = ∅,
    { rw eq_empty_iff_forall_not_mem,
      intros i hi,
      have oops := (le_trans hi (le_tsum' (@ennreal.summable _ a) i)).trans tsum_le_c,
      rw h at oops,
      exact c_ne_top (le_antisymm le_top oops), },
    simp only [obs, finite_empty, finite_empty_to_finset, finset.card_empty,
               algebra_map.coe_zero, zero_le', exists_true_left], },
  have hf : {i : X | ε ≤ a i}.finite,
    from ennreal.finite_const_le_of_tsum_ne_top
          (lt_of_le_of_lt tsum_le_c c_ne_top.lt_top).ne ε_ne_zero,
  use hf,
  have at_least : ∀ i ∈ hf.to_finset, ε ≤ a i,
  { intros i hi,
    simpa only [finite.mem_to_finset, mem_set_of_eq] using hi, },
  have partial_sum := @sum_le_tsum _ _ _ _ _ a hf.to_finset (λ _ _, zero_le') (@ennreal.summable _ a),
  have lower_bound := finset.sum_le_sum at_least,
  simp only [finset.sum_const, nsmul_eq_mul] at lower_bound,
  have key := (ennreal.le_div_iff_mul_le (or.inl ε_ne_zero) (or.inl h)).mpr lower_bound,
  exact le_trans key (ennreal.div_le_div_right (partial_sum.trans tsum_le_c) _),
end

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests