LeanPool.AsymptoticTrianglePacking.Internal — generic selection tools

Two elementary tools used to extract a single good outcome of a nibble round.

• exists_notMem_of_measureReal_add_lt_one — if two events have total probability < 1, some outcome avoids both. (This is what replaces the union bound over vertices: the two events are "too many bad vertices" and "too little coverage", and each is controlled by a Markov inequality.)
• card_filter_mul_le_sum — the counting form of Markov's inequality: at most (∑ᵢ gᵢ)/t indices satisfy t ≤ gᵢ, for a nonnegative g.
• measureReal_ge_le_integral_div — the real-valued Markov inequality.

placeholder-free and axiom-clean [propext, Classical.choice, Quot.sound].

theorem LeanPool.AsymptoticTrianglePacking.Internal.exists_notMem_of_measureReal_add_lt_one {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume] {A B : Set Ω} (h : MeasureTheory.volume.real A + MeasureTheory.volume.real B < 1) : ∃ ω ∉ A, ω ∉ B

If two events have total probability < 1, some outcome avoids both.

theorem LeanPool.AsymptoticTrianglePacking.Internal.measureReal_ge_le_integral_div {Ω : Type u_1} [MeasureTheory.MeasureSpace Ω] {f : Ω → ℝ} (hf : ∀ (ω : Ω), 0 ≤ f ω) (hint : MeasureTheory.Integrable f MeasureTheory.volume) {c : ℝ} (hc : 0 < c) : MeasureTheory.volume.real {ω : Ω | c ≤ f ω} ≤ (∫ (ω : Ω), f ω) / c

Markov's inequality, real-valued form.

theorem LeanPool.AsymptoticTrianglePacking.Internal.card_filter_mul_le_sum {ι : Type u_2} [Fintype ι] (g : ι → ℝ) (hg : ∀ (i : ι), 0 ≤ g i) (t : ℝ) : ↑{i : ι | t ≤ g i}.card * t ≤ ∑ i : ι, g i

Counting Markov. At most (∑ᵢ gᵢ)/t indices satisfy t ≤ gᵢ.