mathlib3 documentation

combinatorics.simple_graph.regularity.chunk

Chunk of the increment partition for Szemerédi Regularity Lemma #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

TODO #

Once ported to mathlib4, this file will be a great golfing ground for Heather's new tactic rel_congr.

References #

Yaël Dillies, Bhavik Mehta, Formalising Szemerédi’s Regularity Lemma in Lean

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.

source
noncomputable def szemeredi_regularity.chunk {α : Type u_1} [fintype α] {P : finpartition finset.univ} (hP : P.is_equipartition) (G : simple_graph α) (ε : ℝ) {U : finset α} (hU : U ∈ P.parts) :
finpartition U

The portion of szemeredi_regularity.increment which partitions U.

Equations
source
noncomputable def szemeredi_regularity.star {α : Type u_1} [fintype α] {P : finpartition finset.univ} (hP : P.is_equipartition) (G : simple_graph α) (ε : ℝ) {U : finset α} (hU : U ∈ P.parts) (V : finset α) :
finset (finset α)

The portion of szemeredi_regularity.chunk which is contained in the witness of non uniformity of U and V.

Equations

Density estimates #

We estimate the density between parts of chunk.

source
theorem szemeredi_regularity.bUnion_star_subset_nonuniform_witness {α : Type u_1} [fintype α] {P : finpartition finset.univ} (hP : P.is_equipartition) (G : simple_graph α) (ε : ℝ) {U : finset α} (hU : U ∈ P.parts) (V : finset α) :
(szemeredi_regularity.star hP G ε hU V).bUnion id ⊆ G.nonuniform_witness ε U V
source
theorem szemeredi_regularity.star_subset_chunk {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} {V : finset α} :
szemeredi_regularity.star hP G ε hU V ⊆ (szemeredi_regularity.chunk hP G ε hU).parts

chunk #

source
theorem szemeredi_regularity.card_chunk {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} (hm : fintype.card α / szemeredi_regularity.step_bound P.parts.card ≠ 0) :
(szemeredi_regularity.chunk hP G ε hU).parts.card = 4 ^ P.parts.card
source
theorem szemeredi_regularity.card_eq_of_mem_parts_chunk {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} {s : finset α} (hs : s ∈ (szemeredi_regularity.chunk hP G ε hU).parts) :
s.card = fintype.card α / szemeredi_regularity.step_bound P.parts.card ∨ s.card = fintype.card α / szemeredi_regularity.step_bound P.parts.card + 1
source
theorem szemeredi_regularity.m_le_card_of_mem_chunk_parts {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} {s : finset α} (hs : s ∈ (szemeredi_regularity.chunk hP G ε hU).parts) :
fintype.card α / szemeredi_regularity.step_bound P.parts.card ≤ s.card
source
theorem szemeredi_regularity.card_le_m_add_one_of_mem_chunk_parts {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} {s : finset α} (hs : s ∈ (szemeredi_regularity.chunk hP G ε hU).parts) :
s.card ≤ fintype.card α / szemeredi_regularity.step_bound P.parts.card + 1
source
theorem szemeredi_regularity.card_bUnion_star_le_m_add_one_card_star_mul {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U : finset α} {hU : U ∈ P.parts} {V : finset α} :
↑(((szemeredi_regularity.star hP G ε hU V).bUnion id).card) ≤ ↑((szemeredi_regularity.star hP G ε hU V).card) * (↑(fintype.card α / szemeredi_regularity.step_bound P.parts.card) + 1)

Final bounds #

Those inequalities are the end result of all this hard work.

source
theorem szemeredi_regularity.edge_density_chunk_not_uniform {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U 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 : ¬G.is_uniform ε U V) :
↑(G.edge_density U V) ^ 2 - ε ^ 5 / 25 + ε ^ 4 / 3 ≤ ((szemeredi_regularity.chunk hP G ε hU).parts ×ˢ (szemeredi_regularity.chunk hP G ε hV).parts).sum (λ (ab : finset α × finset α), ↑(G.edge_density ab.fst ab.snd) ^ 2) / 16 ^ P.parts.card

Lower bound on the edge densities between non-uniform parts of szemeredi_regularity.increment.

source
theorem szemeredi_regularity.edge_density_chunk_uniform {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} {U 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) :
↑(G.edge_density U V) ^ 2 - ε ^ 5 / 25 ≤ ((szemeredi_regularity.chunk hP G ε hU).parts ×ˢ (szemeredi_regularity.chunk hP G ε hV).parts).sum (λ (ab : finset α × finset α), ↑(G.edge_density ab.fst ab.snd) ^ 2) / 16 ^ P.parts.card

Lower bound on the edge densities between parts of szemeredi_regularity.increment. This is the blanket lower bound used the uniform parts.