SzemerediRegularity.card_eq_of_mem_parts_chunk
theorem SzemerediRegularity.card_eq_of_mem_parts_chunk :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
{G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U : Finset α} {hU : U ∈ P.parts} {s : Finset α},
s ∈ (SzemerediRegularity.chunk hP G ε hU).parts →
s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card ∨
s.card = Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
This theorem, "SzemerediRegularity.card_eq_of_mem_parts_chunk", asserts that for any type 'α' with finite elements (indicated by the instance 'Fintype α'), given an equipartition 'P' of the set of all elements of type 'α', a simple graph 'G' on 'α', a real number 'ε', a subset 'U' that is an element of the parts of 'P', and another subset 's', if 's' is an element of the parts of the chunk of the regularity lemma applied to 'P', 'G', 'ε', and 'U', then the number of elements in 's' is either the total number of elements in 'α' divided by the step bound of the number of parts in 'P' or this value plus one.
In other words, each part of the chunk created by Szemeredi's Regularity Lemma will have a size that's equal to the size of the universal set divided by a certain bound (obtained from the original partition's size), or that value incremented by one, thereby ensuring a level of uniformity or "equitable" distribution in the size of the chunks.
More concisely: Given an equipartition P of a finite set α, a simple graph G on α, real number ε, and a subset U of α belonging to a chunk of Szemeredi's Regularity Lemma applied to P, G, and ε, the size of subset s in the chunk containing U satisfies |s| = |α| / bound(P) or |α| / bound(P) + 1.
|
SzemerediRegularity.edgeDensity_chunk_not_uniform
theorem SzemerediRegularity.edgeDensity_chunk_not_uniform :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
{G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [inst_3 : Nonempty α],
P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
100 ≤ 4 ^ P.parts.card * ε ^ 5 →
ε ≤ 1 →
∀ {hU : U ∈ P.parts} {hV : V ∈ P.parts},
U ≠ V →
¬G.IsUniform ε U V →
↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤
(((SzemerediRegularity.chunk hP G ε hU).parts.product
(SzemerediRegularity.chunk hP G ε hV).parts).sum
fun ab => ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
16 ^ P.parts.card
This theorem establishes a lower bound on the edge densities between non-uniform parts of the increment operation in Szemeredi Regularity. Specifically, for a given type $\alpha$ with decidable equality, a simple graph $G$ on $\alpha$ with a decidable adjacency relation, and two finite sets $U$ and $V$ of type $\alpha$, it states that if $U$ and $V$ are distinct parts of a certain equipartition $P$, and the edge density between $U$ and $V$ does not satisfy a uniformity condition dictated by a real number $\epsilon$ between 0 and 1, then the square of the edge density between $U$ and $V$ minus a certain function of $\epsilon$ is less than or equal to the average of the squares of the edge densities over all pairs of parts in the increment of $P$ with respect to $G$ and $\epsilon$, divided by $16$ to the power of the number of parts in $P$. This holds under the conditions that the cardinality of $α$ is at least $P$'s parts cardinality times $16$ to the power of its parts cardinality, and $100$ is less than or equal to $4$ to the power of $P$'s parts cardinality times $\epsilon$ to the power of $5$.
More concisely: For a simple graph on a decidable type with finite, distinct parts in a certain equipartition, the square of the edge density between any two non-uniform parts, not satisfying a uniformity condition, is bounded above by the average square edge density of all pairs in the increment of the partition, divided by 16 to the power of the partition's cardinality, under specific cardinality conditions.
|
SzemerediRegularity.edgeDensity_chunk_uniform
theorem SzemerediRegularity.edgeDensity_chunk_uniform :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
{G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [inst_3 : Nonempty α],
P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
100 ≤ 4 ^ P.parts.card * ε ^ 5 →
∀ (hU : U ∈ P.parts) (hV : V ∈ P.parts),
↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 ≤
(((SzemerediRegularity.chunk hP G ε hU).parts.product (SzemerediRegularity.chunk hP G ε hV).parts).sum
fun ab => ↑(G.edgeDensity ab.1 ab.2) ^ 2) /
16 ^ P.parts.card
The theorem `SzemerediRegularity.edgeDensity_chunk_uniform` establishes a lower bound on the edge densities between different parts of a graph partition obtained through Szemeredi's Regularity Lemma. Given a type `α` with a finite number of elements (Fintype) and decidable equality, a partition `P` of a finite set (equi-partition), a simple graph `G` with vertices from `α` and a decidable adjacency relation, and two finite sets `U` and `V` of `α`, it asserts that if the cardinality of P's parts times 16 raised to the same cardinality is less than or equal to the total number of elements in `α` and if 100 is less than or equal to 4 raised to the cardinality of P's parts times a certain value `ε` raised to the power of 5, then for any `U` and `V` that belong to the parts of `P`, the square of the edge density of `U` and `V` minus `ε` to the power of 5 divided by 25 is less than or equal to the average of squares of edge densities over all possible partitions of `U` and `V`, the latter derived from the regularity chunks of `U` and `V` in `P`, divided by 16 raised to the cardinality of P's parts.
More concisely: Given a finite graph with a partition satisfying certain conditions, the square of the edge density between any two parts minus a power of ε is bounded above by the average of squares of edge densities between all possible partitions, derived from regularity chunks.
|