Lubell frames and asymptotic context

The Lubell frame

noncomputable def HypergraphLowerBound.M (t : ℕ) : ℕ

M_t = lcm { C(t-1, r) : 1 ≤ r ≤ t-1 }.

Equations

• HypergraphLowerBound.M t = (Finset.Icc 1 (t - 1)).lcm fun (r : ℕ) => (t - 1).choose r

noncomputable def HypergraphLowerBound.lubellMultiplicity (t j : ℕ) : ℕ

The multiplicity attached to each j-subset in the Lubell family.

Equations

• HypergraphLowerBound.lubellMultiplicity t j = HypergraphLowerBound.M t / (t - 1).choose (j - 1)

@[implicit_reducible]

noncomputable def HypergraphLowerBound.lubellCap (t : ℕ) : Fin t → ℕ

The constant capacity vector of the Lubell frame.

Equations

• HypergraphLowerBound.lubellCap t = Function.const (Fin t) (HypergraphLowerBound.M t)

def HypergraphLowerBound.supportPatternEmbedding {t j : ℕ} (hj : 2 ≤ j) : { S : Finset (Fin t) // S ∈ (Finset.powersetCard j Finset.univ).val } ↪ SupportPattern t

Embed a j-subset of [t] into the type of support patterns.

Equations

• HypergraphLowerBound.supportPatternEmbedding hj = { toFun := fun (S : { S : Finset (Fin t) // S ∈ (Finset.powersetCard j Finset.univ).val }) => ⟨↑S, ⋯⟩, inj' := ⋯ }

noncomputable def HypergraphLowerBound.supportPatternsOfCard (t j : ℕ) : Multiset (SupportPattern t)

All support patterns of size j on [t], each occurring once.

Equations

• HypergraphLowerBound.supportPatternsOfCard t j = if hj : 2 ≤ j then Multiset.map (⇑(HypergraphLowerBound.supportPatternEmbedding hj)) (Finset.powersetCard j Finset.univ).val.attach else 0

noncomputable def HypergraphLowerBound.lubellLayer (t j : ℕ) : Multiset (SupportPattern t)

The j-subsets in the Lubell multiset, each with the prescribed multiplicity.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HypergraphLowerBound.lubellFrame (t : ℕ) : Multiset (SupportPattern t)

The Lubell support multiset on [t].

Equations

• HypergraphLowerBound.lubellFrame t = (Finset.Icc 2 t).val.bind (HypergraphLowerBound.lubellLayer t)

noncomputable def HypergraphLowerBound.lubellCardSum (t : ℕ) : ℕ

The explicit cardinality expression for the Lubell frame.

Equations

• HypergraphLowerBound.lubellCardSum t = ∑ j ∈ Finset.Icc 2 t, t.choose j * HypergraphLowerBound.lubellMultiplicity t j

Vandermonde-Chu identity for the frame bound

Infrastructure for the frame bound

Vandermonde-Chu identity ingredients

theorem HypergraphLowerBound.lubell_is_frame (t : ℕ) (ht : 2 ≤ t) : IsFrame (lubellFrame t) (lubellCap t) ∧ (lubellFrame t).card = lubellCardSum t

The Lubell multiset L_t is an (M_t, ..., M_t)-frame with |L_t| = M_t * t * (h_t - 1).

Digit sum formula for k_n

@[irreducible]

def HypergraphLowerBound.s2 : ℕ → ℕ

Sum of binary digits of m.

Equations

• HypergraphLowerBound.s2 0 = 0
• HypergraphLowerBound.s2 n.succ = (n + 1) % 2 + HypergraphLowerBound.s2 ((n + 1) / 2)

@[implicit_reducible]

def HypergraphLowerBound.digitSumPrefix (n : ℕ) : ℕ

The prefix sum of binary digit counts appearing in the formula for k n.

Equations

• HypergraphLowerBound.digitSumPrefix n = (Finset.range n).sum HypergraphLowerBound.s2

theorem HypergraphLowerBound.digit_sum_formula (n : ℕ) (hn : 1 ≤ n) : k n = n + digitSumPrefix n

k_n = n + Σ_{j=0}^{n-1} s_2(j), and k_n / (n log_2 n) → 1/2.

noncomputable def HypergraphLowerBound.fixedTCoeff (t : ℕ) : ℝ

The asymptotic coefficient (h_t - 1) / log_2 t appearing in the fixed-t bound.

Equations

• HypergraphLowerBound.fixedTCoeff t = (↑(harmonic t) - 1) / Real.logb 2 ↑t

The fixed-t lower bound

theorem HypergraphLowerBound.fixed_t_bound (t : ℕ) (ht : 2 ≤ t) : ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ↑(H n) ≥ fixedTCoeff t * ↑n * Real.logb 2 ↑n - C * ↑n

For fixed t ≥ 2, H(n) ≥ (h_t - 1) / log_2(t) · n log_2(n) - C_t · n.

noncomputable def HypergraphLowerBound.degree (edges : Finset (Finset ℕ)) (v : ℕ) : ℕ

The number of edges in edges containing the vertex v.

Equations

• HypergraphLowerBound.degree edges v = {e ∈ edges | v ∈ e}.card

The asymptotic theorem

theorem HypergraphLowerBound.asymptotic_lower_bound : 2 * Real.log 2 ≤ Filter.liminf (fun (n : ℕ) => ↑(H n) / ↑(k n)) Filter.atTop

The asymptotic lower bound: liminf H(n)/k_n ≥ 2 ln 2.

theorem HypergraphLowerBound.thm_asymptotic : (∀ (t : ℕ), 2 ≤ t → ∃ (C : ℝ), 0 < C ∧ ∀ (n : ℕ), 1 ≤ n → ↑(H n) ≥ fixedTCoeff t * ↑n * Real.logb 2 ↑n - C * ↑n) ∧ 2 * Real.log 2 ≤ Filter.liminf (fun (n : ℕ) => ↑(H n) / ↑(k n)) Filter.atTop

The asymptotic theorem of frontier.tex, packaging the fixed-t lower bound and its consequence for the liminf ratio H(n) / k_n.