SzemerediRegularity.energy_increment
theorem SzemerediRegularity.energy_increment :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {G : SimpleGraph α}
[inst_2 : DecidableRel G.Adj] {ε : ℝ} [inst_3 : Nonempty α] (hP : P.IsEquipartition),
7 ≤ P.parts.card →
100 ≤ 4 ^ P.parts.card * ε ^ 5 →
P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
¬P.IsUniform G ε →
0 ≤ ε → ε ≤ 1 → ↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((SzemerediRegularity.increment hP G ε).energy G)
The theorem `SzemerediRegularity.energy_increment` states that for any finite type `α` with a decidable equality relation, a partition `P` of a universal finite set `Finset.univ`, a simple graph `G` of type `α` with a decidable adjacency relation, a real number `ε` between 0 and 1 (inclusive), given that `α` is nonempty, `P` is an equipartition, the cardinality of the parts of `P` is at least 7, the value of `4` raised to the power of the cardinality of `P` times `ε` to the power of 5 is at least 100, and the product of the cardinality of `P` and `16` raised to the power of the cardinality of `P` is no larger than the cardinality of `α`, if `P` is not a uniform partition of `G` with respect to `ε`, then the energy of the increment partition is greater than or equal to the energy of the original partition `P` increased by a known fixed amount `ε` to the power 5 divided by 4.
More concisely: If a finite set `α` with a decidable equality relation, a decidable simple graph `G` over `α`, a real number `ε`, and a nonempty equipartition `P` of `Finset.univ` with at least 7 parts satisfying specific cardinality conditions violate uniformity with respect to `G` and `ε`, then the energy increment of `P` exceeds the energy of `P` increased by a constant depending on `ε`.
|
SzemerediRegularity.card_increment
theorem SzemerediRegularity.card_increment :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
{G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ},
P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
¬P.IsUniform G ε →
(SzemerediRegularity.increment hP G ε).parts.card = SzemerediRegularity.stepBound P.parts.card
This theorem, named `SzemerediRegularity.card_increment`, states the following: Given a type `α` that is finite and has decidable equality, a partition `P` of the universal finite set of type `α`, and a simple graph `G` on `α` with a decidable adjacency relation, along with a real number `ε`. If the cardinality of the partition `P` times `16` raised to the power of the cardinality of `P` is less than or equal to the cardinality of the type `α`, and `P` is not a uniform partition of the graph `G` with respect to `ε`, then the cardinality of the partition resulting from the increment of the Szemerédi regularity procedure applied to `P`, `G`, and `ε` is equal to the step bound of the cardinality of `P`, where the step bound of a natural number `n` is defined as `n` times `4` raised to the power of `n`.
More concisely: If a finite type `α` with decidable equality, a partition `P` of `α`, and a simple graph `G` on `α` with decidable adjacency relation satisfy `|P|(16|P|)^|P| <= |α|` and `P` is not uniformly regular with respect to `G` and `ε`, then the cardinality of the next partition obtained from the Szemerédi regularity procedure is equal to the step bound of `|P|`.
|