Forbidden intersection theorems

DefinitionErdős Problem 703: exponential gap for a forbidden intersection size#✓fully proved

The proposition that for every \(\varepsilon > 0\) there is \(\delta > 0\) such that for all natural numbers \(n\) and \(r\) with \(\varepsilon n < r < (1/2 - \varepsilon) n\), every family \(\mathcal{F}\) of subsets of \(\{1, \dots, n\}\) with \(|A \cap B| \ne r\) for all \(A, B \in \mathcal{F}\) (including \(A = B\)) has \(|\mathcal{F}| < (2 - \delta)^n\). Equivalently, \(T(n, r) < (2 - \delta)^n\), where \(T(n, r)\) is the largest size of such a family.

def forbiddenIntersectionExponentialGap : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ δ : ℝ, 0 < δ ∧ ∀ n r : ℕ, ε * n < r → (r : ℝ) < (1 / 2 - ε) * n →
    ∀ F : Finset (Finset (Fin n)), (∀ A ∈ F, ∀ B ∈ F, (A ∩ B).card ≠ r) →
      (F.card : ℝ) < (2 - δ) ^ n

Used by 1

Used byFrankl–Rödl forbidden intersection theorem

TheoremFrankl–Rödl forbidden intersection theorem#●ready to prove

For every \(\varepsilon > 0\) there is \(\delta > 0\) such that for all natural numbers \(n\) and \(r\) with \(\varepsilon n < r < (1/2 - \varepsilon) n\), every family \(\mathcal{F}\) of subsets of \(\{1, \dots, n\}\) with \(|A \cap B| \ne r\) for all \(A, B \in \mathcal{F}\) (including \(A = B\)) has \(|\mathcal{F}| < (2 - \delta)^n\). This answers the second question of Erdős Problem 703 in the affirmative.

public theorem_wanted forbiddenIntersectionExponentialGap_holds :
    forbiddenIntersectionExponentialGap

Sources

• T. F. Bloom, Erdős Problems, Problem #703, https://www.erdosproblems.com/703 (status PROVED (LEAN)); resolution: P. Frankl and V. Rödl, Forbidden intersections, Trans. Amer. Math. Soc. 300 (1987), 259-286, erdosproblems.com/703: 'The answer to the second question is yes, proved by Frankl and Rödl', https://www.erdosproblems.com/703.

Uses 1

Statement usesErdős Problem 703: exponential gap for a forbidden intersection size

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.