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 the partition obtained by gluing the parts partitions together (the increment partition) and shows that the energy globally increases.

This entire file is internal to the proof of Szemerédi Regularity Lemma.

Main declarations #

szemeredi_regularity.increment: The increment partition.
szemeredi_regularity.card_increment: The increment partition is much bigger than the original, but by a controlled amount.
szemeredi_regularity.energy_increment: The increment partition has energy greater than the original by a known (small) fixed amount.

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

source

noncomputable def szemeredi_regularity.increment {α : Type u_1} [fintype α] {P : finpartition finset.univ} (hP : P.is_equipartition) (G : simple_graph α) (ε : ℝ) :

finpartition finset.univ

The increment partition in Szemerédi's Regularity Lemma.

If an equipartition is not uniform, then the increment partition is a (much bigger) equipartition with a slightly higher energy. This is helpful since the energy is bounded by a constant (see szemeredi_regularity.energy_le_one), so this process eventually terminates and yields a not-too-big uniform equipartition.

Equations

szemeredi_regularity.increment hP G ε = P.bind (λ (U : finset α), szemeredi_regularity.chunk hP G ε)

source

theorem szemeredi_regularity.card_increment {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) (hPG : ¬P.is_uniform G ε) :

(szemeredi_regularity.increment hP G ε).parts.card = szemeredi_regularity.step_bound P.parts.card

The increment partition has a prescribed (very big) size in terms of the original partition.

source

theorem szemeredi_regularity.increment_is_equipartition {α : Type u_1} [fintype α] {P : finpartition finset.univ} (hP : P.is_equipartition) (G : simple_graph α) (ε : ℝ) :

(szemeredi_regularity.increment hP G ε).is_equipartition

source

theorem szemeredi_regularity.off_diag_pairs_le_increment_energy {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} :

P.parts.off_diag.attach.sum (λ (x : {x // x ∈ P.parts.off_diag}), pair_contrib G ε hP x / ↑((szemeredi_regularity.increment hP G ε).parts.card) ^ 2) ≤ (szemeredi_regularity.increment hP G ε).energy G

source

theorem szemeredi_regularity.pair_contrib_lower_bound {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} [nonempty α] (x : {i // i ∈ P.parts.off_diag}) (hε₁ : ε ≤ 1) (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) (hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5) :

↑(G.edge_density x.val.fst x.val.snd) ^ 2 - ε ^ 5 / 25 + ite (G.is_uniform ε x.val.fst x.val.snd) 0 (ε ^ 4 / 3) ≤ ↑(pair_contrib G ε hP x) / 16 ^ P.parts.card

source

theorem szemeredi_regularity.uniform_add_nonuniform_eq_off_diag_pairs {α : Type u_1} [fintype α] {P : finpartition finset.univ} {hP : P.is_equipartition} {G : simple_graph α} {ε : ℝ} [nonempty α] (hε₁ : ε ≤ 1) (hP₇ : 7 ≤ P.parts.card) (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) (hPε : 100 ≤ 4 ^ P.parts.card * ε ^ 5) (hPG : ¬P.is_uniform G ε) :

(P.parts.off_diag.sum (λ (x : finset α × finset α), ↑(G.edge_density x.fst x.snd) ^ 2) + ↑(P.parts.card) ^ 2 * (ε ^ 5 / 4)) / ↑(P.parts.card) ^ 2 ≤ P.parts.off_diag.attach.sum (λ (x : {x // x ∈ P.parts.off_diag}), ↑(pair_contrib G ε hP x) / ↑((szemeredi_regularity.increment hP G ε).parts.card) ^ 2)

source

theorem szemeredi_regularity.energy_increment {α : Type u_1} [fintype α] {P : finpartition finset.univ} {G : simple_graph α} {ε : ℝ} [nonempty α] (hP : P.is_equipartition) (hP₇ : 7 ≤ P.parts.card) (hε : 100 < 4 ^ P.parts.card * ε ^ 5) (hPα : P.parts.card * 16 ^ P.parts.card ≤ fintype.card α) (hPG : ¬P.is_uniform G ε) (hε₁ : ε ≤ 1) :

↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((szemeredi_regularity.increment hP G ε).energy G)

The increment partition has energy greater than the original one by a known fixed amount.