FiniteGaps.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The minimum positive gap in a finite set of indices

A set of n ordered indices whose distinct elements are separated by at least h occupies a span of at least h * (n - 1). Taking the least positive gap therefore supplies a closest-return pair with this packing bound.

theorem OAI.QuantitativeVanDerWaerden.gap_mul_card_sub_one_le_span line 19
Source documentation
Pairwise separation forces a lower bound on the span of a finite set. The proof adds the largest index and accounts for its gap from the preceding largest index.
```
theorem gap_mul_card_sub_one_le_span (J : Finset ℕ) (hJ : J.Nonempty) (h : ℕ)
    (hgap : ∀ i ∈ J, ∀ j ∈ J, i < j → h ≤ j - i) :
    h * (J.card - 1) ≤ J.max' hJ - J.min' hJ := by
…
```

theorem OAI.QuantitativeVanDerWaerden.exists_min_gap line 61

Source documentation

Every finite set with at least two elements has an attained minimum positive gap; its size also obeys the packing bound.

theorem exists_min_gap (J : Finset ℕ) (hcard : 2 ≤ J.card) :
    ∃ a ∈ J, ∃ b ∈ J, a < b ∧ 0 < b - a ∧
      (∀ i ∈ J, ∀ j ∈ J, i < j → b - a ≤ j - i) ∧
      (∀ hJ : J.Nonempty,
        (b - a) * (J.card - 1) ≤ J.max' hJ - J.min' hJ) := by
…