Graph regularity, finite weak regularity, and arity-3 hypergraph complexes
The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.
TheoremFinite Frieze–Kannan weak regularity#
For ε > 0, the vertices of G have a partition
P into at most 4 ^ ⌈1 / ε²⌉ parts such that, for all vertex sets A and B, the number of
edges from A to B is within ε * (card V) ^ 2 of its stepped prediction
G.steppedCount P A B.
SimpleGraph.frieze_kannan.{u_1} {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
[DecidableRel G.Adj] {ε : ℝ} (hε : 0 < ε) :
∃ P,
P.parts.card ≤ 4 ^ ⌈1 / ε ^ 2⌉₊ ∧
∀ (A B : Finset V),
|↑(G.interedges A B).card - G.steppedCount P A B| ≤ ε * ↑(Fintype.card V) ^ 2
Uses 1
TheoremStrong graph regularity#
Let ε > 0 and let F : ℕ → ℝ be a positive schedule. Every
equipartition P₀ of a finite graph G is almost refined, up to ε, by the coarse partition P
of a strong regularity witness (P, Q), where P has at least l parts for any requested
l ≤ card α, and Q has at most strongGraphRegularityBound ε F (max l #P₀.parts) parts.
SimpleGraph.exists_strong_regular.{u_1} {α : Type u_1} [Fintype α] [DecidableEq α]
(G : SimpleGraph α) [DecidableRel G.Adj] (P₀ : Finpartition Finset.univ)
(hP₀ : P₀.IsEquipartition) {l : ℕ} (hl : l ≤ Fintype.card α) {ε : ℝ} (hε : 0 < ε) {F : ℕ → ℝ}
(hF : ∀ (n : ℕ), 0 < F n) :
∃ P Q, G.StrongRegular P Q ε F (max l P₀.parts.card) ∧ P.AlmostRefines P₀ ε ∧ l ≤ P.parts.card
TheoremSzemerédi's regularity lemma relative to a seed#
Every equipartition P₀ of a finite
graph is almost refined, up to ε, by an ε-uniform equipartition with at most
refiningRegularityBound ε #P₀.parts parts.
SimpleGraph.exists_regular_equipartition_almost_refining.{u_1} {α : Type u_1} [Fintype α]
[DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} (P₀ : Finpartition Finset.univ)
(hP₀ : P₀.IsEquipartition) (hε : 0 < ε) :
∃ P,
P.IsEquipartition ∧
P.IsUniform G ε ∧
P.AlmostRefines P₀ ε ∧ P.parts.card ≤ TauCeti.refiningRegularityBound ε P₀.parts.card
Lean
Formalized in Tau Ceti as SimpleGraph.exists_regular_equipartition_almost_refining.
Other forms
Szemerédi's regularity lemma relative to a seed, with a minimum number of parts. Formalized in Tau Ceti as SimpleGraph.exists_regular_almostRefines_le_card.
SimpleGraph.exists_regular_almostRefines_le_card.{u_1} {α : Type u_1} [Fintype α] [DecidableEq α]
(G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} (P₀ : Finpartition Finset.univ)
(hP₀ : P₀.IsEquipartition) {l : ℕ} (hl : l ≤ Fintype.card α) (hε : 0 < ε) :
∃ P,
P.IsEquipartition ∧
P.IsUniform G ε ∧
P.AlmostRefines P₀ ε ∧
l ≤ P.parts.card ∧
P.parts.card ≤
TauCeti.nestedRefinementBound ε
(max (max l P₀.parts.card) ⌈2 * ↑(max l P₀.parts.card) / ε⌉₊)
Sources
- Tau Ceti documentation:
SimpleGraph.exists_regular_equipartition_almost_refining - Source of
SimpleGraph.exists_regular_equipartition_almost_refiningin TauCeti/Combinatorics/Regularity/Graph/SeededRegularity.lean - Tau Ceti roadmap status: Graph regularity, finite weak regularity, and arity-3 hypergraph complexes
Uses 2 · Used by 1
TheoremInduced counting lemma for three cells#
Let A 0, A 1, A 2 be pairwise ε-uniform
cells of G, and J a graph on Fin 3. Then the number of maps g with g i ∈ A i such that
g i and g j are adjacent in G exactly when i and j are adjacent in J differs from
|A 0| |A 1| |A 2| times the product, over the pairs i < j, of the edge density of
(A i, A j) (if i and j are adjacent in J) or of its nonedge density 1 - d(A i, A j)
(otherwise), that is SimpleGraph.patternDensity, by at most 3 ε |A 0| |A 1| |A 2|.
SimpleGraph.abs_card_induced_fin_three_sub_le.{u_1, u_2} {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜]
[LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜}
(J : SimpleGraph (Fin 3)) [DecidableRel J.Adj] {A : Fin 3 → Finset α}
(hA : ∀ (i j : Fin 3), i < j → G.IsUniform ε (A i) (A j)) :
|↑{g ∈ Fintype.piFinset A | ∀ (i j : Fin 3), J.Adj i j ↔ G.Adj (g i) (g j)}.card -
(∏ i, ↑(A i).card) * ∏ p, G.patternDensity (J.Adj (↑p).1 (↑p).2) (A (↑p).1) (A (↑p).2)| ≤
3 * ε * ∏ i, ↑(A i).card
TheoremFinite partition energy is graphon partition energy#
For a graph G on Fin m with
0 < m and a partition P of its vertices, the size-weighted energy of P is the partition
energy of the graphon of G over the partition of the unit interval grouping the vertex cells by
the parts of P.
SimpleGraph.graphonPartitionEnergy_finiteGraphGraphon {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m))
[DecidableRel G.Adj] (P : Finpartition Finset.univ) :
TauCeti.DenseGraphLimits.graphonPartitionEnergy MeasureTheory.volume P.cellPartition ⋯
(TauCeti.DenseGraphLimits.finiteGraphGraphon G) =
G.weightedEnergy P
Lean
Formalized in Tau Ceti as SimpleGraph.graphonPartitionEnergy_finiteGraphGraphon.
Sources
DefinitionSimpleGraph.cutDiscrepancy#
The cut discrepancy of G with respect to P: the largest deviation, over all rectangles
(A, B), between the number of edges from A to B and its stepped prediction. It is
count-scaled, so it lies between 0 and (card V) ^ 2.
SimpleGraph.cutDiscrepancy.{u_1} {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V)
[DecidableRel G.Adj] (P : Finpartition Finset.univ) : ℝ
Used by 1
StructureTauCeti.TriadicComplex3#
A triadic complex on V: a finite palette of pairColorCount pair colors chosen by the
complex, a lower skeleton over that palette, and a finite family of polyads over that skeleton.
TauCeti.TriadicComplex3.{u_2} (V : Type u_2) [Fintype V] [DecidableEq V] : Type u_2
Used by 1
DefinitionTauCeti.Colored3Graph.TopRegularOverMostPolyads#
H is (η, r)-top-regular over most polyads of C: the polyads over which H is not
(η, r)-top-regular carry at most an ε-proportion of the selected support.
TauCeti.Colored3Graph.TopRegularOverMostPolyads.{u_1, u_2} {V : Type u_1} [Fintype V]
[DecidableEq V] {κ : Type u_2} [DecidableEq κ] (H : TauCeti.Colored3Graph κ V)
(C : TauCeti.TriadicComplex3 V) (η ε : ℝ) (r : ℕ) : Prop
Lean
Formalized in Tau Ceti as TauCeti.Colored3Graph.TopRegularOverMostPolyads.
Sources
Uses 2
DefinitionTauCeti.Colored3Graph.IsTopRegularOverPolyad#
H is (δ, r)-top-regular over the polyad P when, for every top color c and every
family of r subpolyads of P whose union support has at least δ times the size of the
support of P, the relative density of c on that union is within δ of the relative density
of c over P. Members of the family may repeat, so this tests unions of at most r
subpolyads.
TauCeti.Colored3Graph.IsTopRegularOverPolyad.{u_1, u_2, u_3} {κ : Type u_1} {κ₂ : Type u_2}
{V : Type u_3} [Fintype V] [DecidableEq V] {S : TauCeti.PairSkeleton3 κ₂ V}
(P : TauCeti.Polyad3 S) [DecidableEq κ] (H : TauCeti.Colored3Graph κ V) (δ : ℝ) (r : ℕ) : Prop
Used by 2
TheoremSlicing lemma#
If H is (δ, r)-top-regular over P at a positive rank, then it is
(max (2δ) (δ / α), r)-top-regular over every polyad P' whose pair graphs lie in those of P
and whose support is at least an α-fraction of the support of P. The polyad P' may live
over a different skeleton, so this is how top regularity passes to a refined lower skeleton.
TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subset.{u_1, u_2, u_3, u_4}
{κ : Type u_1} {κ₂ : Type u_2} {V : Type u_3} [Fintype V] [DecidableEq V]
{S : TauCeti.PairSkeleton3 κ₂ V} {P : TauCeti.Polyad3 S} [DecidableEq κ]
{H : TauCeti.Colored3Graph κ V} {δ : ℝ} {r : ℕ} {κ₂' : Type u_4}
{S' : TauCeti.PairSkeleton3 κ₂' V} {P' : TauCeti.Polyad3 S'}
(h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂)
(h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂)
(h : TauCeti.Colored3Graph.IsTopRegularOverPolyad P H δ r) (hr : 1 ≤ r) {α : ℝ} (hα : 0 < α)
(hP' : α * ↑P.support.card ≤ ↑P'.support.card) :
TauCeti.Colored3Graph.IsTopRegularOverPolyad P' H (max (2 * δ) (δ / α)) r
Lean
Formalized in Tau Ceti as TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subset.
Sources
- Tau Ceti documentation:
TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subset - Source of
TauCeti.Colored3Graph.IsTopRegularOverPolyad.of_pairSupport_subsetin TauCeti/Combinatorics/Hypergraph/Polyad/TopRegular.lean - Tau Ceti roadmap status: Graph regularity, finite weak regularity, and arity-3 hypergraph complexes
Uses 1
TheoremCauchy–Schwarz on a resolved witness#
The squared deviation of its density from any
real number a, multiplied by its size, is bounded by the sum of the squared deviations of
the fine densities from a. The empty witness is allowed.
TauCeti.Colored3Graph.card_mul_sq_relDensityOn_sub_le_sum.{u_1, u_3, u_4} {κ : Type u_1}
{κ₂' : Type u_3} {V : Type u_4} [Fintype V] [DecidableEq V] [DecidableEq κ]
(H : TauCeti.Colored3Graph κ V) {T : TauCeti.PairSkeleton3 κ₂' V} (c : κ)
(U : Finset { x // Function.Injective x })
(hU :
∀ (x y : { x // Function.Injective x }),
TauCeti.Polyad3.ofTriple T x = TauCeti.Polyad3.ofTriple T y → (x ∈ U ↔ y ∈ U))
(a : ℝ) :
↑U.card * (↑(H.relDensityOn c U) - a) ^ 2 ≤
∑ x ∈ U, (↑(H.relativeDensity c (TauCeti.Polyad3.ofTriple T x)) - a) ^ 2
Lean
Formalized in Tau Ceti as TauCeti.Colored3Graph.card_mul_sq_relDensityOn_sub_le_sum.
Other forms
Cauchy–Schwarz on a resolved rectangle. Formalized in Tau Ceti as TauCeti.PairColorSystem.card_mul_sq_pairColorDensity_sub_le_sum.
TauCeti.PairColorSystem.card_mul_sq_pairColorDensity_sub_le_sum.{u_1, u_2} {κ : Type u_1}
{V : Type u_2} [Fintype V] [DecidableEq V] (S : TauCeti.PairColorSystem κ V)
{Q : Finpartition Finset.univ} {X Y : Finset V} (hX : ∀ C ∈ Q.parts, C ⊆ X ∨ Disjoint C X)
(hY : ∀ C ∈ Q.parts, C ⊆ Y ∨ Disjoint C Y) (c : κ) (a : ℝ) :
↑{p ∈ X ×ˢ Y | p.1 ≠ p.2}.card * (↑(TauCeti.pairColorDensity S c X Y) - a) ^ 2 ≤
∑ p ∈ X ×ˢ Y with p.1 ≠ p.2, (↑(TauCeti.pairColorDensity S c (Q.part p.1) (Q.part p.2)) - a) ^ 2
Sources
TheoremSzemerédi's regularity lemma below a starting equipartition#
If P₁ is an equipartition
with at least 7 parts and 100 ≤ 4 ^ #P₁.parts * ε ^ 5, and the graph is large enough, then
some ε-uniform equipartition refines P₁ and has at most
stepBound^[⌊4 / ε ^ 5⌋₊ + 1] #P₁.parts parts.
SimpleGraph.szemeredi_regularity_le.{u_1} {α : Type u_1} [Fintype α] [DecidableEq α]
(G : SimpleGraph α) [DecidableRel G.Adj] {ε : ℝ} {P₁ : Finpartition Finset.univ}
(hP₁ : P₁.IsEquipartition) (hP₇ : 7 ≤ P₁.parts.card) (hPε : 100 ≤ 4 ^ P₁.parts.card * ε ^ 5)
(hα :
SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] P₁.parts.card *
16 ^ SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊] P₁.parts.card ≤
Fintype.card α) :
∃ P ≤ P₁,
P.IsEquipartition ∧
P.IsUniform G ε ∧
P.parts.card ≤ SzemerediRegularity.stepBound^[⌊4 / ε ^ 5⌋₊ + 1] P₁.parts.card
TheoremSzemerédi's regularity lemma refining an equipartition exactly#
Every equipartition P of a
finite graph is refined exactly by a δ-uniform equipartition with at most
nestedRefinementBound δ #P.parts parts.
SimpleGraph.exists_regular_exact_refining_equipartition.{u_1} {α : Type u_1} [Fintype α]
[DecidableEq α] (G : SimpleGraph α) [DecidableRel G.Adj] (P : Finpartition Finset.univ)
(hP : P.IsEquipartition) {δ : ℝ} (hδ : 0 < δ) :
∃ Q ≤ P,
Q.IsEquipartition ∧
Q.IsUniform G δ ∧ Q.parts.card ≤ TauCeti.nestedRefinementBound δ P.parts.card
Lean
Formalized in Tau Ceti as SimpleGraph.exists_regular_exact_refining_equipartition.
Sources
Uses 1 · Used by 2
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.