Support gadgets and the substitution theorem

Support patterns and frames

def HypergraphLowerBound.SupportPattern (t : ℕ) : Type

A support pattern on [t] is a subset of Fin t of size at least 2.

Equations

• HypergraphLowerBound.SupportPattern t = { S : Finset (Fin t) // 2 ≤ S.card }

@[reducible, inline]

abbrev HypergraphLowerBound.BlockFamily (t : ℕ) : Type

The block hypergraphs used in a substitution construction.

Equations

• HypergraphLowerBound.BlockFamily t = HypergraphLowerBound.HypergraphFamily (Fin t) ℕ

@[reducible, inline]

abbrev HypergraphLowerBound.SupportOcc {t : ℕ} (F : Multiset (SupportPattern t)) : Type

An occurrence of a support pattern in a support multiset.

Equations

• HypergraphLowerBound.SupportOcc F = Fin F.card

noncomputable def HypergraphLowerBound.supportPatternAt {t : ℕ} (F : Multiset (SupportPattern t)) (s : SupportOcc F) : SupportPattern t

The support pattern attached to a given support-vertex occurrence.

Equations

• HypergraphLowerBound.supportPatternAt F s = F.toList.get ⟨↑s, ⋯⟩

noncomputable def HypergraphLowerBound.supportSetAt {t : ℕ} (F : Multiset (SupportPattern t)) (s : SupportOcc F) : Finset (Fin t)

The underlying subset of [t] attached to a support occurrence.

Equations

• HypergraphLowerBound.supportSetAt F s = ↑(HypergraphLowerBound.supportPatternAt F s)

noncomputable def HypergraphLowerBound.omegaCount {t : ℕ} (F : Multiset (SupportPattern t)) (T I : Finset (Fin t)) : ℕ

omegaCount F T I counts the occurrences of support patterns S in F with S ⊆ T and |S ∩ I| = 1, counting multiplicity.

Equations

• HypergraphLowerBound.omegaCount F T I = {s : HypergraphLowerBound.SupportOcc F | HypergraphLowerBound.supportSetAt F s ⊆ T ∧ (HypergraphLowerBound.supportSetAt F s ∩ I).card = 1}.card

def HypergraphLowerBound.IsFrame {t : ℕ} (F : Multiset (SupportPattern t)) (cap : Fin t → ℕ) : Prop

A support multiset F is an n-frame if the frame inequality holds for every I ⊆ T ⊆ [t].

Equations

• HypergraphLowerBound.IsFrame F cap = ∀ (T I : Finset (Fin t)), I ⊆ T → HypergraphLowerBound.omegaCount F T I ≤ (T \ I).sum cap

inductive HypergraphLowerBound.SubstVertex (t : ℕ) (F : Multiset (SupportPattern t)) : Type

Vertices of the substituted hypergraph: tagged block vertices together with one vertex for each occurrence of a support pattern.

• old {t : ℕ} {F : Multiset (SupportPattern t)} (i : Fin t) (v : ℕ) : SubstVertex t F
• new {t : ℕ} {F : Multiset (SupportPattern t)} (s : Fin F.card) : SubstVertex t F

def HypergraphLowerBound.instDecidableEqSubstVertex.decEq {t✝ : ℕ} {F✝ : Multiset (SupportPattern t✝)} (x✝ x✝¹ : SubstVertex t✝ F✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• HypergraphLowerBound.instDecidableEqSubstVertex.decEq (HypergraphLowerBound.SubstVertex.old i v) (HypergraphLowerBound.SubstVertex.new s) = isFalse ⋯
• HypergraphLowerBound.instDecidableEqSubstVertex.decEq (HypergraphLowerBound.SubstVertex.new s) (HypergraphLowerBound.SubstVertex.old i v) = isFalse ⋯
• HypergraphLowerBound.instDecidableEqSubstVertex.decEq (HypergraphLowerBound.SubstVertex.new a) (HypergraphLowerBound.SubstVertex.new b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HypergraphLowerBound.instDecidableEqSubstVertex {t✝ : ℕ} {F✝ : Multiset (SupportPattern t✝)} : DecidableEq (SubstVertex t✝ F✝)

Equations

• HypergraphLowerBound.instDecidableEqSubstVertex = HypergraphLowerBound.instDecidableEqSubstVertex.decEq

@[reducible, inline]

abbrev HypergraphLowerBound.SubstitutedHypergraph {t : ℕ} (F : Multiset (SupportPattern t)) : Type

The substituted hypergraph whose vertices live in SubstVertex t F.

Equations

• HypergraphLowerBound.SubstitutedHypergraph F = HypergraphLowerBound.Hypergraph (HypergraphLowerBound.SubstVertex t F)

noncomputable def HypergraphLowerBound.supportVerticesOnBlock {t : ℕ} (F : Multiset (SupportPattern t)) (i : Fin t) : Finset (SubstVertex t F)

The support vertices incident to every edge in block i.

Equations

• HypergraphLowerBound.supportVerticesOnBlock F i = Finset.image HypergraphLowerBound.SubstVertex.new {s : HypergraphLowerBound.SupportOcc F | i ∈ HypergraphLowerBound.supportSetAt F s}

noncomputable def HypergraphLowerBound.liftBlockEdge {t : ℕ} (F : Multiset (SupportPattern t)) (i : Fin t) (e : Finset ℕ) : Finset (SubstVertex t F)

Lift one edge from block i into the substituted hypergraph.

Equations

• HypergraphLowerBound.liftBlockEdge F i e = Finset.image (fun (v : ℕ) => HypergraphLowerBound.SubstVertex.old i v) e ∪ HypergraphLowerBound.supportVerticesOnBlock F i

noncomputable def HypergraphLowerBound.substitutionHypergraph {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) : SubstitutedHypergraph F

The substitution hypergraph F[G_1, ..., G_t], realized as the hypergraph whose vertices are tagged block vertices plus support vertices, and whose edges are the lifted edges of the blocks.

Equations

• HypergraphLowerBound.substitutionHypergraph F blocks = Finset.univ.biUnion fun (i : Fin t) => Finset.image (HypergraphLowerBound.liftBlockEdge F i) (blocks i)

noncomputable def HypergraphLowerBound.selectedBlockEdges {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (i : Fin t) : Hypergraph ℕ

The selected edges from block i inside a chosen subfamily P of the substituted hypergraph.

Equations

• HypergraphLowerBound.selectedBlockEdges F blocks P i = {e ∈ blocks i | HypergraphLowerBound.liftBlockEdge F i e ∈ P}

noncomputable def HypergraphLowerBound.selectedBlockCount {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (i : Fin t) : ℕ

The number of selected edges from block i.

Equations

• HypergraphLowerBound.selectedBlockCount F blocks P i = Finset.card (HypergraphLowerBound.selectedBlockEdges F blocks P i)

noncomputable def HypergraphLowerBound.selectedOldVertexCount {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (i : Fin t) (v : ℕ) : ℕ

The number of selected edges from block i containing v.

Equations

• HypergraphLowerBound.selectedOldVertexCount F blocks P i v = {e ∈ HypergraphLowerBound.selectedBlockEdges F blocks P i | v ∈ e}.card

noncomputable def HypergraphLowerBound.selectedSupportCount {t : ℕ} {F : Multiset (SupportPattern t)} (P : SubstitutedHypergraph F) (s : SupportOcc F) : ℕ

The number of selected substituted edges incident to a support occurrence.

Equations

• HypergraphLowerBound.selectedSupportCount P s = {E ∈ P | HypergraphLowerBound.SubstVertex.new s ∈ E}.card

noncomputable def HypergraphLowerBound.tOf {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) : Finset (Fin t)

The blocks from which at most one selected edge is taken.

Equations

• HypergraphLowerBound.tOf F blocks P = {i : Fin t | HypergraphLowerBound.selectedBlockCount F blocks P i ≤ 1}

noncomputable def HypergraphLowerBound.iOf {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) : Finset (Fin t)

The blocks from which exactly one selected edge is taken.

Equations

• HypergraphLowerBound.iOf F blocks P = {i : Fin t | HypergraphLowerBound.selectedBlockCount F blocks P i = 1}

noncomputable def HypergraphLowerBound.oldUniqueVerticesOnBlock {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (i : Fin t) : Finset ℕ

The old vertices in block i that are seen exactly once by the selected family P.

Equations

• HypergraphLowerBound.oldUniqueVerticesOnBlock F blocks P i = {v ∈ HypergraphLowerBound.vertexSet (blocks i) | HypergraphLowerBound.selectedOldVertexCount F blocks P i v = 1}

noncomputable def HypergraphLowerBound.newUniqueSupportVertices {t : ℕ} (F : Multiset (SupportPattern t)) (P : SubstitutedHypergraph F) : Finset (SupportOcc F)

The support-vertex occurrences seen exactly once by the selected family P.

Equations

• HypergraphLowerBound.newUniqueSupportVertices F P = {s : HypergraphLowerBound.SupportOcc F | HypergraphLowerBound.selectedSupportCount P s = 1}

noncomputable def HypergraphLowerBound.oldUniqueVertexUnion {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) : Finset (SubstVertex t F)

The uniquely covered old vertices in the substituted hypergraph, grouped blockwise.

Equations

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

noncomputable def HypergraphLowerBound.newUniqueVertexUnion {t : ℕ} (F : Multiset (SupportPattern t)) (P : SubstitutedHypergraph F) : Finset (SubstVertex t F)

The uniquely covered support vertices in the substituted hypergraph.

Equations

• HypergraphLowerBound.newUniqueVertexUnion F P = Finset.image HypergraphLowerBound.SubstVertex.new (HypergraphLowerBound.newUniqueSupportVertices F P)

noncomputable def HypergraphLowerBound.oldVertexUnion {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) : Finset (SubstVertex t F)

The old vertices coming from the block hypergraphs, tagged by their block index.

Equations

• HypergraphLowerBound.oldVertexUnion F blocks = Finset.univ.biUnion fun (i : Fin t) => Finset.image (HypergraphLowerBound.SubstVertex.old i) (HypergraphLowerBound.vertexSet (blocks i))

noncomputable def HypergraphLowerBound.allNewVertices {t : ℕ} (F : Multiset (SupportPattern t)) : Finset (SubstVertex t F)

All support vertices of the substituted hypergraph, indexed by their occurrences in F.

Equations

• HypergraphLowerBound.allNewVertices F = Finset.image HypergraphLowerBound.SubstVertex.new Finset.univ

@[simp]

theorem HypergraphLowerBound.mem_supportVerticesOnBlock_iff {t : ℕ} {F : Multiset (SupportPattern t)} {i : Fin t} {s : SupportOcc F} : SubstVertex.new s ∈ supportVerticesOnBlock F i ↔ i ∈ supportSetAt F s

@[simp]

theorem HypergraphLowerBound.old_mem_liftBlockEdge_iff {t : ℕ} {F : Multiset (SupportPattern t)} {i j : Fin t} {v : ℕ} {e : Finset ℕ} : SubstVertex.old i v ∈ liftBlockEdge F j e ↔ i = j ∧ v ∈ e

@[simp]

theorem HypergraphLowerBound.new_mem_liftBlockEdge_iff {t : ℕ} {F : Multiset (SupportPattern t)} {s : SupportOcc F} {i : Fin t} {e : Finset ℕ} : SubstVertex.new s ∈ liftBlockEdge F i e ↔ i ∈ supportSetAt F s

theorem HypergraphLowerBound.liftBlockEdge_injective {t : ℕ} (F : Multiset (SupportPattern t)) (i : Fin t) : Function.Injective (liftBlockEdge F i)

theorem HypergraphLowerBound.selectedBlockEdges_subset {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (i : Fin t) : selectedBlockEdges F blocks P i ⊆ blocks i

theorem HypergraphLowerBound.mem_vertexSet_of_count_eq_one {V : Type u_1} [DecidableEq V] {edges P : Hypergraph V} {x : V} (hP : P ⊆ edges) (hx : {E ∈ P | x ∈ E}.card = 1) : x ∈ vertexSet edges

theorem HypergraphLowerBound.liftBlockEdge_ne_of_ne {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (hEdgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)) {i j : Fin t} (hij : i ≠ j) {e e' : Finset ℕ} (he : e ∈ blocks i) (he' : e' ∈ blocks j) : liftBlockEdge F i e ≠ liftBlockEdge F j e'

theorem HypergraphLowerBound.liftedBlockImages_disjoint {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (hEdgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)) {i j : Fin t} (hij : i ≠ j) : Disjoint (Finset.image (liftBlockEdge F i) (blocks i)) (Finset.image (liftBlockEdge F j) (blocks j))

theorem HypergraphLowerBound.old_mem_vertexSet_substitution_iff {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (i : Fin t) (v : ℕ) : SubstVertex.old i v ∈ vertexSet (substitutionHypergraph F blocks) ↔ v ∈ vertexSet (blocks i)

theorem HypergraphLowerBound.new_mem_vertexSet_substitution_iff {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (s : SupportOcc F) : SubstVertex.new s ∈ vertexSet (substitutionHypergraph F blocks) ↔ ∃ i ∈ supportSetAt F s, Finset.Nonempty (blocks i)

theorem HypergraphLowerBound.old_selected_count_eq {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (hP : P ⊆ substitutionHypergraph F blocks) (i : Fin t) (v : ℕ) : {E ∈ P | SubstVertex.old i v ∈ E}.card = selectedOldVertexCount F blocks P i v

theorem HypergraphLowerBound.filter_new_eq_biUnion {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (hP : P ⊆ substitutionHypergraph F blocks) (s : SupportOcc F) : {E ∈ P | SubstVertex.new s ∈ E} = (supportSetAt F s).biUnion fun (i : Fin t) => Finset.image (liftBlockEdge F i) (selectedBlockEdges F blocks P i)

theorem HypergraphLowerBound.selectedImages_disjoint {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (hEdgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)) {S : Finset (Fin t)} : (↑S).PairwiseDisjoint fun (i : Fin t) => Finset.image (liftBlockEdge F i) (selectedBlockEdges F blocks P i)

theorem HypergraphLowerBound.new_selected_count_eq_sum {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (hP : P ⊆ substitutionHypergraph F blocks) (hEdgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)) (s : SupportOcc F) : selectedSupportCount P s = ∑ i ∈ supportSetAt F s, selectedBlockCount F blocks P i

@[simp]

theorem HypergraphLowerBound.mem_tOf_iff {t : ℕ} {F : Multiset (SupportPattern t)} {blocks : BlockFamily t} {P : SubstitutedHypergraph F} {i : Fin t} : i ∈ tOf F blocks P ↔ selectedBlockCount F blocks P i ≤ 1

@[simp]

theorem HypergraphLowerBound.mem_iOf_iff {t : ℕ} {F : Multiset (SupportPattern t)} {blocks : BlockFamily t} {P : SubstitutedHypergraph F} {i : Fin t} : i ∈ iOf F blocks P ↔ selectedBlockCount F blocks P i = 1

theorem HypergraphLowerBound.card_inter_iOf_eq_sum_indicator {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (S : Finset (Fin t)) : (S ∩ iOf F blocks P).card = ∑ i ∈ S, if selectedBlockCount F blocks P i = 1 then 1 else 0

theorem HypergraphLowerBound.sum_selected_eq_card_inter_iOf {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (S : Finset (Fin t)) (hST : S ⊆ tOf F blocks P) : ∑ i ∈ S, selectedBlockCount F blocks P i = (S ∩ iOf F blocks P).card

theorem HypergraphLowerBound.sum_selected_eq_one_iff {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (S : Finset (Fin t)) : ∑ i ∈ S, selectedBlockCount F blocks P i = 1 ↔ S ⊆ tOf F blocks P ∧ (S ∩ iOf F blocks P).card = 1

theorem HypergraphLowerBound.new_unique_iff {t : ℕ} (F : Multiset (SupportPattern t)) (blocks : BlockFamily t) (P : SubstitutedHypergraph F) (hP : P ⊆ substitutionHypergraph F blocks) (hEdgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)) (s : SupportOcc F) : selectedSupportCount P s = 1 ↔ supportSetAt F s ⊆ tOf F blocks P ∧ (supportSetAt F s ∩ iOf F blocks P).card = 1

theorem HypergraphLowerBound.support_vertex_realized {t : ℕ} (F : Multiset (SupportPattern t)) (edgeCounts : Fin t → ℕ) (blocks : BlockFamily t) (hFrame : IsFrame F edgeCounts) (hEdgeCounts : ∀ (i : Fin t), Finset.card (blocks i) = edgeCounts i) (s : SupportOcc F) : ∃ i ∈ supportSetAt F s, Finset.Nonempty (blocks i)

Substitution theorem

structure HypergraphLowerBound.PartitionedBlocks {t : ℕ} (cap : Fin t → ℕ) (blocks : BlockFamily t) : Prop

The assumptions on a family of block hypergraphs needed for the qualitative substitution theorem.

• vertexDisjoint : Pairwise fun (i j : Fin t) => Disjoint (vertexSet (blocks i)) (vertexSet (blocks j))
• edgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)
• partitionBound (i : Fin t) : NoLargePartition (blocks i) (cap i)

structure HypergraphLowerBound.CountedBlocks {t : ℕ} (edgeCounts vertexCounts : Fin t → ℕ) (blocks : BlockFamily t) extends HypergraphLowerBound.PartitionedBlocks edgeCounts blocks : Prop

The additional edge/vertex count data needed for the quantitative recurrence.

• vertexDisjoint : Pairwise fun (i j : Fin t) => Disjoint (vertexSet (blocks i)) (vertexSet (blocks j))
• edgeDisjoint : Pairwise fun (i j : Fin t) => Disjoint (blocks i) (blocks j)
• partitionBound (i : Fin t) : NoLargePartition (blocks i) (edgeCounts i)
• edgeCard (i : Fin t) : Finset.card (blocks i) = edgeCounts i
• vertexCard (i : Fin t) : (vertexSet (blocks i)).card = vertexCounts i

theorem HypergraphLowerBound.substitution_theorem {t : ℕ} (F : Multiset (SupportPattern t)) (cap : Fin t → ℕ) (blocks : BlockFamily t) (hFrame : IsFrame F cap) (hBlocks : PartitionedBlocks cap blocks) : NoLargePartition (substitutionHypergraph F blocks) (Finset.univ.sum cap)

If F is an n-frame and each block hypergraph has no partition larger than its capacity, then the substituted hypergraph has no partition larger than the total capacity. The hypotheses on pairwise disjoint vertex and edge sets match the setup in frontier.tex.

theorem HypergraphLowerBound.frame_recurrence {t : ℕ} (F : Multiset (SupportPattern t)) (edgeCounts vertexCounts : Fin t → ℕ) (blocks : BlockFamily t) (hFrame : IsFrame F edgeCounts) (hBlocks : CountedBlocks edgeCounts vertexCounts blocks) : Finset.card (substitutionHypergraph F blocks) = Finset.univ.sum edgeCounts ∧ (vertexSet (substitutionHypergraph F blocks)).card = Finset.univ.sum vertexCounts + F.card ∧ NoLargePartition (substitutionHypergraph F blocks) (Finset.univ.sum edgeCounts)

Quantitative corollary of the substitution theorem used throughout the recursive constructions. Since hypergraphs are encoded by their edge sets, "no isolated vertices" is implicit in the use of vertexSet.