Chunk of the increment partition for Szemerédi Regularity Lemma #
In the proof of Szemerédi Regularity Lemma, we need to partition each part of a starting partition to increase the energy. This file defines those partitions of parts and shows that they locally increase the energy.
This entire file is internal to the proof of Szemerédi Regularity Lemma.
Main declarations #
SzemerediRegularity.chunk: The partition of a part of the starting partition.SzemerediRegularity.edgeDensity_chunk_uniform:chunkdoes not locally decrease the edge density between uniform parts too much.SzemerediRegularity.edgeDensity_chunk_not_uniform:chunklocally increases the edge density between non-uniform parts.
TODO #
Once ported to mathlib4, this file will be a great golfing ground for Heather's new tactic
gcongr.
References #
[Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean][srl_itp]
Definitions #
We define chunk, the partition of a part, and star, the sets of parts of chunk that are
contained in the corresponding witness of non-uniformity.
noncomputable def
SzemerediRegularity.chunk
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
(hP : Finpartition.IsEquipartition P)
(G : SimpleGraph α)
(ε : ℝ)
{U : Finset α}
(hU : U ∈ P.parts)
:
The portion of SzemerediRegularity.increment which partitions U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
SzemerediRegularity.star
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
(hP : Finpartition.IsEquipartition P)
(G : SimpleGraph α)
(ε : ℝ)
{U : Finset α}
(hU : U ∈ P.parts)
(V : Finset α)
:
The portion of SzemerediRegularity.chunk which is contained in the witness of non-uniformity
of U and V.
Equations
- SzemerediRegularity.star hP G ε hU V = Finset.filter (fun (x : Finset α) => x ⊆ SimpleGraph.nonuniformWitness G ε U V) (SzemerediRegularity.chunk hP G ε hU).parts
Instances For
theorem
SzemerediRegularity.biUnion_star_subset_nonuniformWitness
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
(hP : Finpartition.IsEquipartition P)
(G : SimpleGraph α)
(ε : ℝ)
{U : Finset α}
(hU : U ∈ P.parts)
(V : Finset α)
:
Finset.biUnion (SzemerediRegularity.star hP G ε hU V) id ⊆ SimpleGraph.nonuniformWitness G ε U V
theorem
SzemerediRegularity.star_subset_chunk
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
{V : Finset α}
:
SzemerediRegularity.star hP G ε hU V ⊆ (SzemerediRegularity.chunk hP G ε hU).parts
theorem
SzemerediRegularity.card_chunk
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
(hm : Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≠ 0)
:
(SzemerediRegularity.chunk hP G ε hU).parts.card = 4 ^ P.parts.card
theorem
SzemerediRegularity.card_eq_of_mem_parts_chunk
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
{s : Finset α}
(hs : 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
theorem
SzemerediRegularity.m_le_card_of_mem_chunk_parts
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
{s : Finset α}
(hs : s ∈ (SzemerediRegularity.chunk hP G ε hU).parts)
:
Fintype.card α / SzemerediRegularity.stepBound P.parts.card ≤ s.card
theorem
SzemerediRegularity.card_le_m_add_one_of_mem_chunk_parts
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
{s : Finset α}
(hs : s ∈ (SzemerediRegularity.chunk hP G ε hU).parts)
:
s.card ≤ Fintype.card α / SzemerediRegularity.stepBound P.parts.card + 1
theorem
SzemerediRegularity.card_biUnion_star_le_m_add_one_card_star_mul
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{hU : U ∈ P.parts}
{V : Finset α}
:
↑(Finset.biUnion (SzemerediRegularity.star hP G ε hU V) id).card ≤ ↑(SzemerediRegularity.star hP G ε hU V).card * (↑(Fintype.card α / SzemerediRegularity.stepBound P.parts.card) + 1)
Final bounds #
Those inequalities are the end result of all this hard work.
theorem
SzemerediRegularity.edgeDensity_chunk_not_uniform
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{V : Finset α}
[Nonempty α]
(hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α)
(hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5)
(hε₁ : ε ≤ 1)
{hU : U ∈ P.parts}
{hV : V ∈ P.parts}
(hUVne : U ≠ V)
(hUV : ¬SimpleGraph.IsUniform G ε U V)
:
↑(SimpleGraph.edgeDensity G U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤ (Finset.sum (Finset.product (SzemerediRegularity.chunk hP G ε hU).parts (SzemerediRegularity.chunk hP G ε hV).parts)
fun (ab : Finset α × Finset α) => ↑(SimpleGraph.edgeDensity G ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
Lower bound on the edge densities between non-uniform parts of SzemerediRegularity.increment.
theorem
SzemerediRegularity.edgeDensity_chunk_uniform
{α : Type u_1}
[Fintype α]
{P : Finpartition Finset.univ}
{hP : Finpartition.IsEquipartition P}
{G : SimpleGraph α}
{ε : ℝ}
{U : Finset α}
{V : Finset α}
[Nonempty α]
(hPα : P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α)
(hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5)
(hU : U ∈ P.parts)
(hV : V ∈ P.parts)
:
↑(SimpleGraph.edgeDensity G U V) ^ 2 - ε ^ 5 / 25 ≤ (Finset.sum (Finset.product (SzemerediRegularity.chunk hP G ε hU).parts (SzemerediRegularity.chunk hP G ε hV).parts)
fun (ab : Finset α × Finset α) => ↑(SimpleGraph.edgeDensity G ab.1 ab.2) ^ 2) / 16 ^ P.parts.card
Lower bound on the edge densities between parts of SzemerediRegularity.increment. This is the
blanket lower bound used the uniform parts.