Lemma 8.6.2 — some endpoint lies in at least n/2d of n pairwise intersecting d-intervals
ProvedMatousekLP.DIntervals.exists_endpoint_in_manycombinatoricscountingd-intervalsp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1
Let and , and let be -intervals (a finite sequence, so repetitions are allowed) such that for all . Then there is an index and an endpoint of such that
This is the counting step behind the section's capstone: in a pairwise intersecting sequence, a single endpoint is covered by a fixed fraction of the members. Allowing repetitions is what later lets rational weights be replaced by multiplicities.
Formalization Note The sequence is indexed by Fin n (the book's are 0, …, n-1). The count is the number of indices , counted with repetitions, and is real division. The hypothesis is implicit in the book's and is stated explicitly, since with there is no endpoint at all.
Preamble
import Mathlib import Definitions.Def_MatousekLP_DIntervals_DInterval open Finset
Formal statement
namespace MatousekLP.DIntervals
open Classical in
/-- Lemma 8.6.2 (p. 179): if `J_1, …, J_n` (`n ≥ 1`, repetitions allowed) are `d`-intervals with
`J_i ∩ J_j ≠ ∅` for all `i, j`, then some endpoint `p` of some `J_i` lies in at least `n / 2d`
of the `J_j`. Indices `1, …, n` are `0, …, n-1`. -/
theorem exists_endpoint_in_many {d n : ℕ} (hd : 1 ≤ d) (hn : 0 < n) (J : Fin n → DInterval d)
(hJ : ∀ i j, ((J i).toSet ∩ (J j).toSet).Nonempty) :
∃ i : Fin n, ∃ p ∈ (J i).endpoints,
(n : ℝ) / (2 * d) ≤ ((univ.filter fun j => p ∈ (J j).toSet).card : ℝ) := by sorry
end MatousekLP.DIntervals
Source
Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, p. 179, Lemma 8.6.2
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.