Theory Szemeredi_Regularity.Szemeredi

section ‹Szemerédi's Regularity Lemma›

theory Szemeredi
  imports "HOL-Library.Disjoint_Sets" "Girth_Chromatic.Ugraphs" "HOL-Analysis.Convex"

begin

text‹We formalise Szemerédi's Regularity Lemma, which is a major result in the study of large graphs
(extremal graph theory).
We follow Yufei Zhao's notes ``Graph Theory and Additive Combinatorics'' (MIT),
latest version here: 🌐‹https://yufeizhao.com/gtacbook/›
and W.T. Gowers's notes ``Topics in Combinatorics'' (University of Cambridge, Lent 2004, Chapter 3)
🌐‹https://www.dpmms.cam.ac.uk/~par31/notes/tic.pdf›.
We also used an earlier version of Zhao's book: 🌐‹https://yufeizhao.com/gtac/gtac.pdf›.›


subsection ‹Partitions›

subsubsection ‹Partitions indexed by integers›

definition finite_graph_partition :: "[uvert set, uvert set set, nat] ⇒ bool"
  where "finite_graph_partition V P n ≡ partition_on V P ∧ finite P ∧ card P = n"

lemma finite_graph_partition_0 [iff]:
  "finite_graph_partition V P 0 ⟷ V = {} ∧ P = {}"
  by (auto simp: finite_graph_partition_def partition_on_def)

lemma finite_graph_partition_empty [iff]:
  "finite_graph_partition {} P n ⟷ P = {} ∧ n = 0"
  by (auto simp: finite_graph_partition_def partition_on_def)

lemma finite_graph_partition_equals:
  "finite_graph_partition V P n ⟹ (⋃P) = V"
  by (meson finite_graph_partition_def partition_on_def)

lemma finite_graph_partition_subset:
  "⟦finite_graph_partition V P n; X ∈ P⟧ ⟹ X ⊆ V"
  using finite_graph_partition_equals by blast

lemma trivial_graph_partition_exists:
  assumes "V ≠ {}"
  shows "finite_graph_partition V {V} (Suc 0)"
  by (simp add: assms finite_graph_partition_def partition_on_space)

lemma finite_graph_partition_finite:
  assumes "finite_graph_partition V P k" "finite V" "X ∈ P"
  shows "finite X"
  by (meson assms finite_graph_partition_subset infinite_super)

lemma finite_graph_partition_gt0:
  assumes "finite_graph_partition V P k" "finite V" "X ∈ P"
  shows "card X > 0"
  by (metis assms card_0_eq finite_graph_partition_def finite_graph_partition_finite gr_zeroI partition_on_def)

lemma card_finite_graph_partition:
  assumes "finite_graph_partition V P k" "finite V"
  shows "(∑X∈P. card X) = card V"
  by (metis assms finite_graph_partition_def finite_graph_partition_finite product_partition)

subsubsection ‹Tools to combine the refinements of the partition @{term "P i"} for each @{term i}›

text ‹These are needed to retain the ``intuitive'' idea of partitions as indexed by integers.›

subsection ‹Edges›

text ‹All edges between two sets of vertices, @{term X} and @{term Y}, in a graph, @{term G}›

definition all_edges_between :: "nat set ⇒ nat set ⇒ nat set × nat set set ⇒ (nat × nat) set"
  where "all_edges_between X Y G ≡ {(x,y). x∈X ∧ y∈Y ∧ {x,y} ∈ uedges G}"

lemma all_edges_between_subset: "all_edges_between X Y G ⊆ X×Y"
  by (auto simp: all_edges_between_def)

lemma max_all_edges_between: 
  assumes "finite X" "finite Y"
  shows "card (all_edges_between X Y G) ≤ card X * card Y"
  by (metis assms card_mono finite_SigmaI all_edges_between_subset card_cartesian_product)

lemma all_edges_between_empty [simp]:
  "all_edges_between {} Z G = {}" "all_edges_between Z {} G = {}"
  by (auto simp: all_edges_between_def)

lemma all_edges_between_disjnt1:
  assumes "disjnt X Y"
  shows "disjnt (all_edges_between X Z G) (all_edges_between Y Z G)"
  using assms by (auto simp: all_edges_between_def disjnt_iff)

lemma all_edges_between_disjnt2:
  assumes "disjnt Y Z"
  shows "disjnt (all_edges_between X Y G) (all_edges_between X Z G)"
  using assms by (auto simp: all_edges_between_def disjnt_iff)

lemma all_edges_between_Un1:
  "all_edges_between (X ∪ Y) Z G = all_edges_between X Z G ∪ all_edges_between Y Z G"
  by (auto simp: all_edges_between_def)

lemma all_edges_between_Un2:
  "all_edges_between X (Y ∪ Z) G = all_edges_between X Y G ∪ all_edges_between X Z G"
  by (auto simp: all_edges_between_def)

lemma finite_all_edges_between:
  assumes "finite X" "finite Y"
  shows "finite (all_edges_between X Y G)"
  by (meson all_edges_between_subset assms finite_cartesian_product finite_subset)

subsection ‹Edge Density and Regular Pairs›

text ‹The edge density between two sets of vertices, @{term X} and @{term Y}, in @{term G}.
      Authors disagree on whether the sets are assumed to be disjoint!.
      Quite a few authors assume disjointness, e.g. Malliaris and Shelah 🌐‹https://www.jstor.org/stable/23813167›.›
definition "edge_density X Y G ≡ card(all_edges_between X Y G) / (card X * card Y)"

lemma edge_density_ge0: "edge_density X Y G ≥ 0"
  by (auto simp: edge_density_def)

lemma edge_density_le1: "edge_density K Y G ≤ 1"
proof (cases "finite K ∧ finite Y")
  case True
  then show ?thesis 
    using of_nat_mono [OF max_all_edges_between, of K Y]
    by (fastforce simp add: edge_density_def divide_simps)
qed (auto simp: edge_density_def)

lemma all_edges_between_swap:
  "all_edges_between X Y G = (λ(x,y). (y,x)) ` (all_edges_between Y X G)"
  unfolding all_edges_between_def
  by (auto simp add: insert_commute image_iff split: prod.split)

lemma card_all_edges_between_commute:
  "card (all_edges_between X Y G) = card (all_edges_between Y X G)"
proof -
  have "inj_on (λ(x, y). (y, x)) A" for A :: "(nat*nat)set"
    by (auto simp: inj_on_def)
  then show ?thesis
    by (simp add: all_edges_between_swap [of X Y] card_image)
qed

lemma edge_density_commute: "edge_density X Y G = edge_density Y X G"
  by (simp add: edge_density_def card_all_edges_between_commute mult.commute)


text ‹$\epsilon$-regular pairs, for two sets of vertices. Again, authors disagree on whether the
sets need to be disjoint, though it seems that overlapping sets cause double-counting. Authors also
disagree about whether or not to use the strict subset relation here. The proofs below are easier if
it is strict but later proofs require the non-strict version. The two definitions can be proved to
be equivalent under fairly mild conditions, but even those conditions turn out to be onerous.›

definition regular_pair::  "real ⇒ uvert set  ⇒ uvert set ⇒ ugraph ⇒ bool" 
     ("_-regular'_pair" [999]1000)
  where "ε-regular_pair X Y G ≡ 
    ∀A B. A ⊆ X ∧ B ⊆ Y ∧ (card A ≥ ε * card X) ∧ (card B ≥ ε * card Y) ⟶
              ¦edge_density A B G - edge_density X Y G¦ ≤ ε" for ε::real

lemma regular_pair_commute: "ε-regular_pair X Y G ⟷ ε-regular_pair Y X G"
  by (metis edge_density_commute regular_pair_def)

lemma edge_density_Un:
  assumes "disjnt X1 X2" "finite X1" "finite X2"
  shows "edge_density (X1 ∪ X2) Y G = (edge_density X1 Y G * card X1 + edge_density X2 Y G * card X2) / (card X1 + card X2)"
proof (cases "finite Y")
  case True
  with assms show ?thesis 
    by (simp add: edge_density_def all_edges_between_disjnt1 all_edges_between_Un1 finite_all_edges_between card_Un_disjnt card_ge_0_finite divide_simps)
qed (simp add: edge_density_def)

lemma edge_density_partition:
  assumes "finite_graph_partition U P n"
  shows "edge_density U W G = (∑X∈P. edge_density X W G * card X) / card U"
proof (cases "finite U")
  case True
  have "finite P"
    using assms finite_graph_partition_def by blast
  then show ?thesis
    using True assms
  proof (induction P arbitrary: n U)
    case empty
    then show ?case
      by (simp add: edge_density_def finite_graph_partition_def partition_on_def)
  next
    case (insert X P)
    then have "n > 0"
      by (metis finite_graph_partition_0 gr_zeroI insert_not_empty)
    with insert.prems insert.hyps 
    have UX: "finite_graph_partition (U-X) P (n-1)"
      by (auto simp: finite_graph_partition_def partition_on_def disjnt_iff pairwise_insert)
    then have finU: "finite (⋃P)"
      by (simp add: finite_graph_partition_equals insert)
    then have sumXP: "card U = card X + card (⋃P)"
      by (metis UX card_finite_graph_partition finite_graph_partition_equals insert.hyps insert.prems sum.insert)
    have FUX: "finite (U - X)"
      by (simp add: insert.prems)
    have XUP: "X ∪ (⋃P) = U"
      using finite_graph_partition_equals insert.prems(2) by auto
    then have "edge_density U W G = edge_density (X ∪ ⋃P) W G"
      by auto
    also have "… = (edge_density X W G * card X + edge_density (⋃P) W G * card (⋃P)) 
                  / (card X + card (⋃P))"
    proof (rule edge_density_Un)
      show "disjnt X (⋃P)"
        using UX disjnt_iff finite_graph_partition_equals by auto
      show "finite X"
        using XUP ‹finite U› by blast
    qed (use finU in auto)
    also have "… = (edge_density X W G * card X + edge_density (U-X) W G * card (⋃P)) 
                  / card U"
      using UX card_finite_graph_partition finite_graph_partition_equals insert.prems(1) insert.prems(2) sumXP by auto
    also have "… = (∑Y ∈ insert X P. edge_density Y W G * card Y) / card U"
      using UX insert.prems insert.hyps 
      apply (simp add: insert.IH [OF FUX UX] divide_simps algebra_simps finite_graph_partition_equals)
      by (metis (no_types, lifting) Diff_eq_empty_iff finite_graph_partition_empty sum.empty)
    finally show ?case .
  qed
qed (simp add: edge_density_def)

text‹Let @{term P}, @{term Q} be partitions of a set of vertices @{term V}. 
  Then @{term P} refines @{term Q} if for all @{term ‹A ∈ P›} there is @{term ‹B ∈ Q›} 
  such that @{term ‹A ⊆ B›}.›

text ‹For the sake of generality, and following Zhao's Online Lecture 
🌐‹https://www.youtube.com/watch?v=vcsxCFSLyP8&t=16s›
we do not impose disjointness: we do not include @{term "i≠j"} below.›

definition irregular_set:: "[real, ugraph, uvert set set] ⇒ (uvert set × uvert set) set"
  ("_-irregular'_set" [999]1000)
  where "ε-irregular_set ≡ λG P. {(R,S)|R S. R∈P ∧ S∈P ∧ ¬ ε-regular_pair R S G}"
  for ε::real

text‹A regular partition may contain a few irregular pairs as long as their total size is bounded as follows.›
definition regular_partition:: "[real, ugraph, uvert set set] ⇒ bool" 
    ("_-regular'_partition" [999]1000)
  where
  "ε-regular_partition ≡ λG P . 
     partition_on (uverts G) P ∧
     (∑(R,S) ∈ irregular_set ε G P. card R * card S) ≤ ε * (card (uverts G))⇧2" for ε::real

lemma irregular_set_subset: "ε-irregular_set G P ⊆ P × P"
  by (auto simp: irregular_set_def)

lemma irregular_set_swap: "(i,j) ∈ ε-irregular_set G P ⟷ (j,i) ∈ ε-irregular_set G P"
  by (auto simp add: irregular_set_def regular_pair_commute)

lemma finite_irregular_set [simp]: "finite P ⟹ finite (ε-irregular_set G P)"
  by (metis finite_SigmaI finite_subset irregular_set_subset)

subsection ‹Energy of a Graph›

text ‹Definition 3.7 (Energy), written @{term "q(U,W)"}›
definition energy_graph_subsets:: "[uvert set, uvert set, ugraph] ⇒ real" where
  "energy_graph_subsets U W G ≡
     card U * card W * (edge_density U W G)⇧2 / (card (uverts G))⇧2"

text ‹Definition for partitions›
definition energy_graph_partitions :: "[ugraph, uvert set set, uvert set set] ⇒ real"
  where "energy_graph_partitions G P Q ≡ ∑R∈P.∑S∈Q. energy_graph_subsets R S G"

lemma energy_graph_subsets_0 [simp]: 
     "energy_graph_subsets {} B G = 0" "energy_graph_subsets A {} G = 0"
  by (auto simp: energy_graph_subsets_def)

lemma energy_graph_subsets_ge0 [simp]:
  "energy_graph_subsets U W G ≥ 0"
  by (auto simp: energy_graph_subsets_def)

lemma energy_graph_partitions_ge0 [simp]:
  "energy_graph_partitions G U W ≥ 0"
  by (auto simp: sum_nonneg energy_graph_partitions_def)

lemma energy_graph_subsets_commute: 
  "energy_graph_subsets U W G = energy_graph_subsets W U G"
  by (simp add: energy_graph_subsets_def edge_density_commute)

lemma energy_graph_partitions_commute:
  "energy_graph_partitions G W U = energy_graph_partitions G U W"
  by (simp add: energy_graph_partitions_def energy_graph_subsets_commute sum.swap [where A=W])

text‹Definition 3.7 (Energy of a Partition), or following Gowers, mean square density:
 a version of energy for a single partition of the vertex set. › 

abbreviation mean_square_density :: "[ugraph, uvert set set] ⇒ real"
  where "mean_square_density G P ≡ energy_graph_partitions G P P"

lemma mean_square_density: 
  "mean_square_density G U ≡ 
          (∑R∈U. ∑S∈U. card R * card S * (edge_density R S G)⇧2) / (card (uverts G))⇧2"
  by (simp add: energy_graph_partitions_def energy_graph_subsets_def sum_divide_distrib)

text‹Observation: the energy is between 0 and 1 because the edge density is bounded above by 1.›

lemma sum_partition_le:
  assumes "finite_graph_partition V P k" "finite V"
  shows "(∑R∈P. ∑S∈P. real (card R * card S)) ≤ (real(card V))⇧2"
proof -
  have "finite P"
    using assms finite_graph_partition_def by blast
  then show ?thesis
    using assms
  proof (induction P arbitrary: V k)
    case (insert X P)
    have [simp]: "finite Y" if "Y ∈ insert X P" for Y
      by (meson finite_graph_partition_finite insert.prems that)
    have C: "card Y ≤ card V" if"Y ∈ insert X P" for Y
      by (meson card_mono finite_graph_partition_subset insert.prems that)
    have D [simp]: "(∑Y∈P. real (card Y)) = real (card V) - real (card X)"
      by (smt (verit) card_finite_graph_partition insert.hyps insert.prems of_nat_sum sum.cong sum.insert)
    have "disjnt X (⋃P)"
      using insert.prems insert.hyps
      by (auto simp add: finite_graph_partition_def disjnt_iff pairwise_insert partition_on_def)
    with insert have *: "(∑R∈P. ∑S∈P. real (card R * card S)) ≤ (real (card (V - X)))⇧2"
      unfolding finite_graph_partition_def
      by (simp add: lessThan_Suc partition_on_insert disjoint_family_on_insert sum.distrib)
    have [simp]: "V ∩X = X"
      using finite_graph_partition_equals insert.prems by blast 
    have "(∑R ∈ insert X P. ∑S ∈ insert X P. real (card R * card S)) 
      = real (card X * card X) + 2 * (card V - card X) * card X
        + (∑R∈P. ∑S∈P. real (card R * card S))"
      using ‹X ∉ P› ‹finite P›
      by (simp add: C of_nat_diff sum.distrib algebra_simps flip: sum_distrib_right)
    also have "… ≤ real (card X * card X) + 2 * (card V - card X) * card X + (real (card (V - X)))⇧2"
      using * by linarith
    also have "… ≤ (real (card V))⇧2"
      by (simp add: of_nat_diff C card_Diff_subset_Int algebra_simps power2_eq_square)
    finally show ?case .
  qed auto
qed

lemma mean_square_density_bounded: 
  assumes "finite_graph_partition (uverts G) P k" "finite (uverts G)" 
  shows "mean_square_density G P ≤ 1"
proof-
  have "(∑R∈P. ∑S∈P. real (card R * card S) * (edge_density R S G)⇧2) 
     ≤ (∑R∈P. ∑S∈P. real (card R * card S))"
    by (intro sum_mono mult_right_le_one_le) (auto simp: abs_square_le_1 edge_density_ge0 edge_density_le1)
  also have "… ≤ (real(card (uverts G)))⇧2"
    using sum_partition_le assms by blast 
  finally show ?thesis 
    by (simp add: mean_square_density divide_simps)
qed

subsection ‹Partitioning and Energy›

text‹See Gowers's remark after Lemma 11. 
 Further partitioning of subsets of the vertex set cannot make the energy decrease. 
 We follow Gowers's proof, which avoids the use of probability.›

lemma sum_products_le:
  fixes a :: "'a ⇒ real"
  assumes "⋀i. i ∈ I ⟹ a i ≥ 0"
  shows "(∑i∈I. a i * b i)⇧2 ≤ (∑i∈I. a i) * (∑i∈I. a i * (b i)⇧2)"  (is "?L ≤ ?R")
proof -
  have "?L = (∑i∈I. sqrt (a i) * (sqrt (a i) * b i))⇧2"
    by (smt (verit, ccfv_SIG) assms mult.assoc real_sqrt_mult_self sum.cong)
  also have "... ≤ (∑i∈I. (sqrt (a i))⇧2) * (∑i∈I. (sqrt (a i) * b i)⇧2)"
    by (rule Cauchy_Schwarz_ineq_sum)
  also have "... = ?R"
    by (smt (verit) assms mult.assoc mult.commute power2_eq_square real_sqrt_pow2 sum.cong)
  finally show ?thesis .
qed

lemma energy_graph_partition_half:
  assumes P: "finite_graph_partition U P n"
  shows "card U * (edge_density U W G)⇧2 ≤ (∑R∈P. card R * (edge_density R W G)⇧2)"
proof (cases "finite U")
  case True
  have §: "(∑R∈P. card R * edge_density R W G)⇧2 
         ≤ (sum card P) * (∑R∈P. card R * (edge_density R W G)⇧2)"
    by (simp add: sum_products_le)
  have "card U * (edge_density U W G)⇧2 = (∑R∈P. card R * (edge_density U W G)⇧2)"
    by (metis ‹finite U› P sum_distrib_right card_finite_graph_partition of_nat_sum)
  also have "… = edge_density U W G * (∑R∈P. edge_density U W G * card R)"
    by (simp add: sum_distrib_left power2_eq_square mult_ac)
  also have "… = (∑R∈P. edge_density R W G * real (card R)) * edge_density U W G"
  proof -
    have "edge_density U W G * (∑R∈P. edge_density R W G * card R) 
        = edge_density U W G * (edge_density U W G * (∑R∈P. card R))"
      using ‹finite U› assms card_finite_graph_partition  by (auto simp: edge_density_partition [OF P])
    then show ?thesis
      by (simp add: mult.commute sum_distrib_left)
  qed
  also have "… = (∑R∈P. card R * edge_density R W G) * edge_density U W G"
    by (simp add: sum_distrib_left mult_ac)
  also have "… = (∑R∈P. card R * edge_density R W G)⇧2 / card U"
    using assms by (simp add: edge_density_partition [OF P] mult_ac flip: power2_eq_square)
  also have "… ≤ (∑R∈P. card R * (edge_density R W G)⇧2)"
    using § P card_finite_graph_partition ‹finite U› 
    by (force simp add: mult_ac divide_simps simp flip: of_nat_sum)
  finally show ?thesis .
qed (simp add: sum_nonneg)

proposition energy_graph_partition_increase:
  assumes P: "finite_graph_partition U P k" and V: "finite_graph_partition W Q l"
  shows "energy_graph_partitions G P Q ≥ energy_graph_subsets U W G" 
proof -
  have "(card U * card W) * (edge_density U W G)⇧2 = card W * (card U * (edge_density U W G)⇧2)"
    by (simp add: mult_ac)
  also have "… ≤ card W * (∑R∈P. card R * (edge_density R W G)⇧2)"
    by (intro mult_left_mono energy_graph_partition_half) (use assms in auto)
  also have "… = (∑R∈P. card R * (card W * (edge_density W R G)⇧2))"
    by (simp add: sum_distrib_left edge_density_commute mult_ac)
  also have "… ≤ (∑R∈P. card R * (∑S∈Q. card S * (edge_density S R G)⇧2))"
    by (intro mult_left_mono energy_graph_partition_half sum_mono) (use assms in auto)
  also have "… ≤ (∑R∈P. ∑S∈Q. (card R * card S) * (edge_density R S G)⇧2)"
    by (simp add: sum_distrib_left edge_density_commute mult_ac)
  finally
  have "(card U * card W) * (edge_density U W G)⇧2 
    ≤ (∑R∈P. ∑S∈Q. (card R * card S) * (edge_density R S G)⇧2)" .
  then show ?thesis
    unfolding energy_graph_partitions_def energy_graph_subsets_def
    by (simp add: divide_simps flip: sum_divide_distrib)
qed

text ‹The following is the fully general version of Gowers's Lemma 11  
Further partitioning of subsets of the vertex set cannot make the energy decrease.
Note that @{term V} should be @{term "uverts G"} even though this more general version holds.›

lemma energy_graph_partitions_increase_half:
  assumes ref: "refines V Q P" and "finite V" and part_VP: "partition_on V P"
    and U: "{} ∉ U"
  shows "energy_graph_partitions G Q U ≥ energy_graph_partitions G P U" 
        (is "?egQ ≥ ?egP")
proof -
  have "∃F. partition_on R F ∧ F = {S∈Q. S ⊆ R}" if "R∈P" for R
    using ref refines_obtains_subset that by blast
  then obtain F where F: "⋀R. R ∈ P ⟹ partition_on R (F R) ∧ F R = {S∈Q. S ⊆ R}"
    by fastforce
  have injF: "inj_on F P"
    by (metis F inj_on_inverseI partition_on_def)
  have finite_P: "finite R" if "R ∈ P" for R
    by (metis Union_upper ‹finite V› part_VP finite_subset partition_on_def that)
  then have finite_F: "finite (F R)" if "R ∈ P" for R
    using that by (simp add: F)
  have dFP: "disjoint (F ` P)"
    using part_VP 
    by (smt (verit, best) F Union_upper disjnt_iff disjointD le_inf_iff pairwise_imageI partition_on_def subset_empty)
  have F_ne: "F R ≠ {}" if "R ∈ P" for R
    by (metis F Sup_empty part_VP partition_on_def that)
  have F_sums_Q: "(∑R∈P. ∑U∈F R. f U) = (∑S∈Q. f S)" for f :: "nat set ⇒ real"
  proof -
    have "Q = (⋃R ∈ P. F R)"
      using ref by (force simp add: refines_def dest: F)
    then have "(∑S∈Q. f S) = sum f (⋃R ∈ P. F R)"
      by blast
    also have "… = (sum ∘ sum) f (F ` P)"
      by (smt (verit, best) dFP disjnt_def finite_F image_iff pairwiseD sum.Union_disjoint)
    also have "… = (∑R ∈ P. ∑U∈F R. f U)"
      unfolding comp_apply by (metis injF sum.reindex_cong)
    finally show ?thesis
      by simp
  qed
  have "?egP = (∑R ∈ P. ∑T∈U. energy_graph_subsets R T G)"
    by (simp add: energy_graph_partitions_def)
  also have "… ≤ (∑R∈P. ∑T∈U. energy_graph_partitions G (F R) {T})"
  proof -
    have "finite_graph_partition R (F R) (card (F R))"
      if "R ∈ P" for R
      by (meson F finite_F finite_graph_partition_def that) 
    moreover have "finite_graph_partition T {T} (Suc 0)"
      if "T ∈ U" for T
      using U by (metis that trivial_graph_partition_exists)
    ultimately show ?thesis
      using finite_P by (intro sum_mono energy_graph_partition_increase) auto
  qed
  also have "… = (∑R ∈ P. ∑D ∈ F R. ∑T∈U. energy_graph_subsets D T G)"
    by (simp add: energy_graph_partitions_def sum.swap [where B = "U"])
  also have "… = ?egQ"
    by (simp add: energy_graph_partitions_def F_sums_Q)
  finally show ?thesis .
qed

proposition energy_graph_partitions_increase:
  assumes "refines V Q P" "refines V' Q' P'" 
    and "finite V" "finite V'" 
  shows "energy_graph_partitions G Q Q' ≥ energy_graph_partitions G P P'"
proof -
  obtain "{} ∉ P'" "{} ∉ Q"
    using assms unfolding refines_def partition_on_def by presburger
  then show ?thesis
    using assms unfolding refines_def
    by (smt (verit, ccfv_SIG) assms energy_graph_partitions_commute energy_graph_partitions_increase_half)
qed

text ‹The original version of Gowers's Lemma 11 (also in Zhao)
      is not general enough to be used for anything.›
corollary mean_square_density_increase:
  assumes "refines V Q P" "finite V"
  shows "mean_square_density G Q ≥ mean_square_density G P"
  using assms energy_graph_partitions_increase by presburger 


text‹The Energy Boost Lemma says that an 
irregular partition increases the energy substantially. We assume that @{term "𝒰 ⊆ uverts G"} 
and @{term "𝒲 ⊆ uverts G"} are not irregular, as witnessed by their subsets @{term"U1 ⊆ 𝒰"} and @{term"W1 ⊆ 𝒲"}.
The proof follows Lemma 12 of Gowers. ›

definition "part2 X Y ≡ if X ⊂ Y then {X,Y-X} else {Y}"

lemma card_part2: "card (part2 X Y) ≤ 2"
  by (simp add: part2_def card_insert_if)

lemma sum_part2: "⟦X ⊆ Y; f{} = 0⟧ ⟹ sum f (part2 X Y) = f X + f (Y-X)"
  by (force simp add: part2_def sum.insert_if)

lemma partition_part2:
  assumes "A ⊆ B" "A ≠ {}"
  shows "partition_on B (part2 A B)"
  using assms by (auto simp add: partition_on_def part2_def disjnt_iff pairwise_insert)

proposition energy_boost:
  fixes ε::real and U W G
  defines "alpha ≡ edge_density U W G"
  defines "u ≡ λX Y. edge_density X Y G - alpha"
  assumes "finite U" "finite W"
    and "U' ⊆ U" "W' ⊆ W" "ε > 0"
    and U': "card U' ≥ ε * card U" and W': "card W' ≥ ε * card W"
    and gt: "¦u U' W'¦ > ε"
  shows "(∑A ∈ part2 U' U. ∑B ∈ part2 W' W. energy_graph_subsets A B G)
         ≥ energy_graph_subsets U W G + ε^4 * (card U * card W) / (card (uverts G))⇧2"
          (is "?lhs ≥ ?rhs")
proof -
  define UF where "UF ≡ part2 U' U"
  define WF where "WF ≡ part2 W' W"
  obtain [simp]: "finite U" "finite W"
    using assms by (meson finite_subset)
  obtain card': "card U' > 0" "card W' > 0"
    using gt ‹ε > 0› U' W'
    by (force simp: u_def alpha_def edge_density_def mult_le_0_iff zero_less_mult_iff)
  then obtain card: "card U > 0" "card W > 0"
    using assms by fastforce
  then obtain [simp]: "finite U'" "finite W'"
    by (meson card' card_ge_0_finite)
  obtain [simp]: "W' ≠ W - W'" "U' ≠ U - U'"
    by (metis DiffD2 card' all_not_in_conv card.empty less_irrefl)
  have UF_ne: "card x ≠ 0" if "x ∈ UF" for x
    using card' assms that by (auto simp: UF_def part2_def split: if_split_asm)
  have WF_ne: "card x ≠ 0" if "x ∈ WF" for x
    using card' assms that by (auto simp: WF_def part2_def split: if_split_asm)
  have cardUW: "card U = card U' + card(U - U')" "card W = card W' + card(W - W')"
    using card card' ‹U' ⊆ U› ‹W' ⊆ W›
    by (metis card_eq_0_iff card_Diff_subset card_mono le_add_diff_inverse less_le)+
  have "U = (U - U') ∪ U'" "disjnt (U - U') U'"
    using ‹U' ⊆ U› by (force simp: disjnt_iff)+
  then have CU: "card (all_edges_between U Z G) 
          = card (all_edges_between (U - U') Z G) + card (all_edges_between U' Z G)" 
      if "finite Z" for Z 
    by (metis ‹finite U'› all_edges_between_Un1 all_edges_between_disjnt1 ‹finite U› 
        card_Un_disjnt finite_Diff finite_all_edges_between that)

  have "W = (W - W') ∪ W'" "disjnt (W - W') W'"
    using ‹W' ⊆ W› by (force simp: disjnt_iff)+
  then have CW: "card (all_edges_between Z W G) 
          = card (all_edges_between Z (W - W') G) + card (all_edges_between Z W' G)"
    if "finite Z" for Z
    by (metis ‹finite W'› all_edges_between_Un2 all_edges_between_disjnt2 ‹finite W›
        card_Un_disjnt finite_Diff2 finite_all_edges_between that)
  have *: "(∑X∈UF. ∑Y∈WF. real (card (all_edges_between X Y G))) 
         = card (all_edges_between U W G)"
    by (simp add: UF_def WF_def cardUW CU CW sum_part2 ‹U' ⊆ U› ‹W' ⊆ W›)
  have **: "real (card U) * real (card W) = (∑X∈UF. ∑Y∈WF. card X * card Y)"
    by (simp add: UF_def WF_def cardUW sum_part2 ‹U' ⊆ U› ‹W' ⊆ W› algebra_simps)

  let ?S = "∑X∈UF. ∑Y∈WF. (card X * card Y) / (card U * card W) * (edge_density X Y G)⇧2"
  define T where "T ≡ (∑X∈UF. ∑Y∈WF. (card X * card Y) / (card U * card W) * (edge_density X Y G))"
  have §: "2 * T = alpha + alpha * (∑X∈UF. ∑Y∈WF. (card X * card Y) / (card U * card W))"
    unfolding alpha_def T_def
    by (simp add: * ** edge_density_def divide_simps sum_part2 ‹U' ⊆ U› ‹W' ⊆ W› UF_ne WF_ne flip: sum_divide_distrib)
  have "ε * ε ≤ u U' W' * u U' W'"
    by (metis abs_ge_zero abs_mult_self_eq ‹ε > 0› gt less_le mult_mono)
  then have "(ε*ε)*(ε*ε) ≤ (card U' * card W') / (card U * card W) * (u U' W')⇧2"
    using card mult_mono [OF U' W']  ‹ε > 0›
    apply (simp add: divide_simps eval_nat_numeral)
    by (smt (verit, del_insts) mult.assoc mult.commute mult_mono' of_nat_0_le_iff zero_le_mult_iff)
  also have "… ≤ (∑X∈UF. ∑Y∈WF.  (card X * card Y) / (card U * card W) * (u X Y)⇧2)"
    by (simp add: UF_def WF_def sum_part2 ‹U' ⊆ U› ‹W' ⊆ W›)
  also have "… = ?S - 2 * T * alpha
                 + alpha⇧2 * (∑X∈UF. ∑Y∈WF. (card X * card Y) / (card U * card W))"
    by (simp add: u_def T_def power2_diff mult_ac ring_distribs divide_simps 
          sum_distrib_left sum_distrib_right sum_subtractf sum.distrib flip: sum_divide_distrib)
  also have "… = ?S - alpha⇧2"
    using § by (simp add: power2_eq_square algebra_simps)
  finally have 12: "alpha⇧2 + ε^4 ≤ ?S"
    by (simp add: eval_nat_numeral)
  have "?rhs = (alpha⇧2 + ε^4) * (card U * card W / (card (uverts G))⇧2)"
    unfolding alpha_def energy_graph_subsets_def
    by (simp add: ring_distribs divide_simps power2_eq_square)
  also have "… ≤ ?S * (card U * card W / (card (uverts G))⇧2)"
    by (rule mult_right_mono [OF 12]) auto
  also have "… = ?lhs"
    using card unfolding energy_graph_subsets_def UF_def WF_def
    by (auto simp add: algebra_simps sum_part2 ‹U' ⊆ U› ‹W' ⊆ W› )
  finally show ?thesis .
qed

subsection ‹Energy boost for partitions›

text‹We can always find a refinement that increases the energy by a certain amount.›

text ‹A necessary lemma for the tower of exponentials in the result. Angeliki's proof›
lemma le_tower_2: "k * (2 ^ Suc k) ≤ 2^(2^k)"
proof (induction k rule: less_induct)
  case (less k)
  show ?case 
  proof (cases "k ≤ Suc (Suc 0)")
    case False
    define j where "j = k - Suc 0"
    have kj: "k = Suc j"
      using False j_def by force
    with False have §: "(2^j + 3) ≤ (2::nat) ^ k"
      by (simp add: Suc_leI le_less_trans not_less_eq_eq numeral_3_eq_3)
    have "k * (2 ^ Suc k) ≤ 6 * j * 2^j"
      using False by (simp add: kj)
    also have "… ≤ 6 * 2^(2^j)"
      using kj less.IH by force
    also have "… < 2^(2^j + 3)"
      by (simp add: power_add) 
    also have "… ≤ 2^2^k"
      by (simp add: §)
    finally show ?thesis
      by simp      
  qed (auto simp: le_Suc_eq)
qed


text ‹The bound $2 ^{k+1}$  comes from a different source by Zhao:
``Graph Theory and Additive Combinatorics'', 🌐‹https://yufeizhao.com/gtacbook/›.
It's needed because our @{term regular_partition} includes the diagonal; 
otherwise, $k 2^k$ would work. Gowers'  version has a flatly incorrect bound.›
proposition exists_refinement:
  assumes fgp: "finite_graph_partition (uverts G) P k" and "finite (uverts G)" 
    and irreg: "¬ ε-regular_partition G P" and "ε > 0"
  obtains Q where "refines (uverts G) Q P"                     
                    "mean_square_density G Q ≥ mean_square_density G P + ε^5" 
                    "⋀R. R∈P ⟹ card {S∈Q. S ⊆ R} ≤ 2 ^ Suc k"
                    "card Q ≤ k * 2 ^ Suc k"
proof -
  define sum_pp where "sum_pp ≡ (∑(R,S) ∈ ε-irregular_set G P. card R * card S)"
  have cardP: "card P = k"
    using fgp finite_graph_partition_def by force
  then have "k ≠ 0"
    using assms unfolding regular_partition_def irregular_set_def finite_graph_partition_def by fastforce
  with assms have G_nonempty: "0 < card (uverts G)"
    by (metis card_gt_0_iff finite_graph_partition_empty)
  have part_GP: "partition_on (uverts G) P"
    using fgp finite_graph_partition_def by blast 
  then have finP: "finite R" "R ≠ {}" if "R∈P" for R
    using assms that partition_onD3 finite_graph_partition_finite by blast+
  have spp: "sum_pp > ε * (card (uverts G))⇧2"
    by (metis irreg not_le part_GP regular_partition_def sum_pp_def)
  then have sum_irreg_pos: "sum_pp > 0"
    using ‹ε > 0› G_nonempty less_asym by fastforce
  have "∃X⊆R. ∃Y⊆S. ε * card R ≤ card X ∧ ε * card S ≤ card Y ∧
                     ¦edge_density X Y G - edge_density R S G¦ > ε"
    if "(R,S) ∈ ε-irregular_set G P" for R S
    using that fgp finite_graph_partition_subset by (simp add: irregular_set_def regular_pair_def not_le) 
  then obtain X0 Y0 
    where XY0_psub_P: "⋀R S. ⟦(R,S) ∈ ε-irregular_set G P⟧ ⟹ X0 R S ⊆ R ∧ Y0 R S ⊆ S"
    and XY0_eps:
    "⋀R S. (R,S) ∈ ε-irregular_set G P
        ⟹ ε * card R ≤ card (X0 R S) ∧ ε * card S ≤ card (Y0 R S) ∧
            ¦edge_density (X0 R S) (Y0 R S) G - edge_density R S G¦ > ε"
    by metis
  obtain iP where iP: "bij_betw iP P {..<k}"
    by (metis fgp finite_graph_partition_def to_nat_on_finite cardP)
  define X where "X ≡ λR S. if iP R < iP S then Y0 S R else X0 R S"
  define Y where "Y ≡ λR S. if iP R < iP S then X0 S R else Y0 R S"
  have XY_psub_P: "⋀R S. ⟦(R,S) ∈ ε-irregular_set G P⟧ ⟹ X R S ⊆ R ∧ Y R S ⊆ S"
    using XY0_psub_P by (force simp: X_def Y_def irregular_set_swap)
  have XY_eps:
    "⋀R S. (R,S) ∈ ε-irregular_set G P
        ⟹ ε * card R ≤ card (X R S) ∧ ε * card S ≤ card (Y R S) ∧
            ¦edge_density (X R S) (Y R S) G - edge_density R S G¦ > ε"
    using XY0_eps by (force simp: X_def Y_def edge_density_commute irregular_set_swap)
  have card_elem_P: "card R > 0" if "R∈P" for R
    by (metis card_eq_0_iff finP neq0_conv that)
  have XY_nonempty: "X R S ≠ {}" "Y R S ≠ {}" if "(R,S) ∈ ε-irregular_set G P" for R S
    using XY_eps [OF that] that ‹ε > 0› card_elem_P [of R] card_elem_P [of S]
    by (auto simp: irregular_set_def mult_le_0_iff)

  text‹By the assumption that our partition is irregular, there are many irregular pairs.
       For each irregular pair, find pairs of subsets that witness irregularity.›
  define XP where "XP R ≡ ((λS. part2 (X R S) R) ` {S. (R,S) ∈ ε-irregular_set G P})" for R
  define YP where "YP S ≡ ((λR. part2 (Y R S) S) ` {R. (R,S) ∈ ε-irregular_set G P})" for S

  text ‹include degenerate partition to ensure it works whether or not there's an irregular pair›
  define PP where "PP ≡ λR. insert {R} (XP R ∪ YP R)"
  define QS where "QS R ≡ common_refinement (PP R)" for R
  define r where "r R ≡ card (QS R)" for R
  have "finite P"
    using fgp finite_graph_partition_def by blast
  then have finPP: "finite (PP R)" for R
    by (simp add: PP_def XP_def YP_def irregular_set_def)
  have inPP_fin: "P ∈ PP R ⟹ finite P" for P R
    by (auto simp: PP_def XP_def YP_def part2_def)
  have finite_QS: "finite (QS R)" for R
    by (simp add: QS_def finPP finite_common_refinement inPP_fin)

  have part_QS: "partition_on R (QS R)" if "R ∈ P" for R
    unfolding QS_def
  proof (intro partition_on_common_refinement partition_onI)
    show "⋀𝒜. 𝒜 ∈ PP R ⟹ {} ∉ 𝒜"
      using that XY_nonempty XY_psub_P finP
      by (fastforce simp add: PP_def XP_def YP_def part2_def)
  qed (auto simp: disjnt_iff PP_def XP_def YP_def part2_def dest: XY_psub_P)

  have part_P_QS: "finite_graph_partition R (QS R) (r R)" if "R∈P" for R
    by (simp add: finite_QS finite_graph_partition_def part_QS r_def that)
  then have fin_SQ [simp]: "finite (QS R)" if "R∈P" for R
    using QS_def finite_QS by force
  have QS_ne: "{} ∉ QS R" if "R∈P" for R
    using QS_def part_QS partition_onD3 that by blast 
  have QS_subset_P: "q ∈ QS R ⟹ q ⊆ R" if "R∈P" for R q
    by (meson finite_graph_partition_subset part_P_QS that)
  then have QS_inject: "R = R'" 
    if "R∈P" "R'∈P" "q ∈ QS R" "q ∈ QS R'" for R R' q
    by (metis UnionI disjnt_iff equals0I pairwiseD part_GP part_QS partition_on_def that)
  define Q where "Q ≡ (⋃R∈P. QS R)"
  define m where "m ≡ ∑R∈P. r R"
  show thesis
  proof
    show ref_QP: "refines (uverts G) Q P"
      unfolding refines_def
    proof (intro conjI strip part_GP)
      fix X
      assume "X ∈ Q"
      then show "∃Y∈P. X ⊆ Y"
        by (metis QS_subset_P Q_def UN_iff)
    next
      show "partition_on (uverts G) Q"
      proof (intro conjI partition_onI)
        show "⋃Q = uverts G"
        proof
          show "⋃Q ⊆ uverts G"
            using QS_subset_P Q_def fgp finite_graph_partition_equals by fastforce
          show "uverts G ⊆ ⋃Q"
            by (metis Q_def Sup_least UN_upper Union_mono part_GP part_QS partition_onD1)
        qed
        show "disjnt p q" if "p ∈ Q" and "q ∈ Q" and "p ≠ q" for p q
        proof -
          from that 
          obtain R S where "R∈P" "S∈P" 
            and *: "p ∈ QS R" "q ∈ QS S"
            by (auto simp: Q_def QS_def)
          show ?thesis
          proof (cases "R=S")
            case True
            then show ?thesis
              using part_QS [of R]
              by (metis ‹R ∈ P› * pairwiseD partition_on_def ‹p ≠ q›)
          next
            case False
            with * show ?thesis
              by (metis QS_subset_P ‹R ∈ P› ‹S ∈ P› disjnt_iff pairwiseD part_GP partition_on_def subsetD)
          qed
        qed
        show "{} ∉ Q"
          using QS_ne Q_def by blast
      qed
    qed 
    have disj_QSP: "disjoint_family_on QS P"
      unfolding disjoint_family_on_def by (metis Int_emptyI QS_inject)
    let ?PP = "P × P"
    let ?REG = "?PP - ε-irregular_set G P"
    define sum_eps where "sum_eps ≡ (∑(R,S) ∈ ε-irregular_set G P. ε^4 * (card R * card S) / (card (uverts G))⇧2)"
    have A: "energy_graph_subsets R S G + ε^4 * (card R * card S) / (card (uverts G))⇧2
          ≤ energy_graph_partitions G (part2 (X R S) R) (part2 (Y R S) S)"
          (is "?L ≤ ?R")
          if *: "(R,S) ∈ ε-irregular_set G P" for R S
    proof -
      have "R∈P" "S∈P"
        using * by (auto simp: irregular_set_def)
      have "?L ≤ (∑A ∈ part2 (X R S) R. ∑B ∈ part2 (Y R S) S. energy_graph_subsets A B G)"
        using XY_psub_P [OF *] XY_eps [OF *] assms
        by (intro energy_boost ‹R ∈ P› ‹S ∈ P› finP ‹ε>0›) auto
      also have "… ≤ ?R"
        by (simp add: energy_graph_partitions_def)
      finally show ?thesis .
    qed
    have B: "energy_graph_partitions G (part2 (X R S) R) (part2 (Y R S) S)
          ≤ energy_graph_partitions G (QS R) (QS S)"
      if "(R,S) ∈ ε-irregular_set G P" for R S
    proof -
      have "R∈P" "S∈P" using that by (auto simp: irregular_set_def)
      have [simp]: "¬ X R S ⊂ R ⟷ X R S = R" "¬ Y R S ⊂ S ⟷ Y R S = S"
        using XY_psub_P that by blast+
      have XPX: "part2 (X R S) R ∈ PP R"
        using that by (simp add: PP_def XP_def)
      have I: "partition_on R (QS R)"
        using QS_def ‹R ∈ P› part_QS by force
      moreover have "∀q ∈ QS R. ∃b ∈ part2 (X R S) R. q ⊆ b"
        using common_refinement_exists [OF _ XPX] by (simp add: QS_def)
      ultimately have ref_XP: "refines R (QS R) (part2 (X R S) R)"
        by (simp add: refines_def XY_nonempty XY_psub_P that partition_part2)
      have YPY: "part2 (Y R S) S ∈ PP S"
        using that by (simp add: PP_def YP_def)
      have J: "partition_on S (QS S)"
        using QS_def ‹S ∈ P› part_QS by force
      moreover have "∀q ∈ QS S. ∃b ∈ part2 (Y R S) S. q ⊆ b"
        using common_refinement_exists [OF _ YPY] by (simp add: QS_def)
      ultimately have ref_YP: "refines S (QS S) (part2 (Y R S) S)"
        by (simp add: XY_nonempty XY_psub_P that partition_part2 refines_def)
      show ?thesis
        using ‹R ∈ P› ‹S ∈ P›
        by (simp add: finP energy_graph_partitions_increase [OF ref_XP ref_YP])
    qed
    have "mean_square_density G P + ε^5 ≤ mean_square_density G P + sum_eps"
    proof -
      have "ε^5 = (ε * (card (uverts G))⇧2) * (ε^4 / (card (uverts G))⇧2)"
        using G_nonempty by (simp add: field_simps eval_nat_numeral)
      also have "… ≤ sum_pp * (sum_eps / sum_pp)"
      proof (rule mult_mono)
        show "ε^4 / real ((card (uverts G))⇧2) ≤ sum_eps / sum_pp"
          using sum_irreg_pos sum_eps_def sum_pp_def
          by (auto simp add: case_prod_unfold sum.neutral simp flip: sum_distrib_left sum_divide_distrib of_nat_sum of_nat_mult)
      qed (use spp sum_nonneg in auto)
      also have "… ≤ sum_eps"
        by (simp add: sum_irreg_pos)
      finally show ?thesis by simp
    qed
    also have "… = (∑(i,j) ∈ ?REG. energy_graph_subsets i j G) 
                   + (∑(i,j) ∈ ε-irregular_set G P. energy_graph_subsets i j G) + sum_eps"
      by (simp add: ‹finite P› energy_graph_partitions_def sum.cartesian_product irregular_set_subset sum.subset_diff)
    also have "… ≤ (∑(i,j) ∈ ?REG. energy_graph_subsets i j G)
                   + (∑(i,j) ∈ ε-irregular_set G P. energy_graph_partitions G (part2 (X i j) i) (part2 (Y i j) j))"
      using A unfolding sum_eps_def case_prod_unfold
      by (force intro: sum_mono simp flip: sum.distrib)
    also have "… ≤ (∑(i,j) ∈ ?REG. energy_graph_partitions G (QS i) (QS j))
                   + (∑(i,j) ∈ ε-irregular_set G P. energy_graph_partitions G (part2 (X i j) i) (part2 (Y i j) j))"
      by (auto intro!: part_P_QS sum_mono energy_graph_partition_increase)
    also have "… ≤ (∑(i,j) ∈ ?REG. energy_graph_partitions G (QS i) (QS j)) 
                  + (∑(i,j) ∈ ε-irregular_set G P. energy_graph_partitions G (QS i) (QS j))"
      using B
    proof (intro sum_mono add_mono ordered_comm_monoid_add_class.sum_mono2)
    qed (auto split: prod.split)
    also have "… = (∑(i,j) ∈ ?PP. energy_graph_partitions G (QS i) (QS j))"
      by (metis (no_types, lifting) ‹finite P› finite_SigmaI irregular_set_subset sum.subset_diff)
    also have "… = (∑i∈P. ∑j∈P. energy_graph_partitions G (QS i) (QS j))"
      by (simp flip: sum.cartesian_product)
    also have "… = (∑A ∈ Q. ∑B ∈ Q. energy_graph_subsets A B G)"
      unfolding energy_graph_partitions_def Q_def
      by (simp add: disj_QSP ‹finite P› sum.UNION_disjoint_family sum.swap [of _ "P" "QS _"])
    also have "… = mean_square_density G Q"
      by (simp add: mean_square_density energy_graph_subsets_def sum_divide_distrib)
    finally show "mean_square_density G P + ε ^ 5 ≤ mean_square_density G Q" .

    define QinP where "QinP ≡ λi. {j∈Q. j ⊆ i}"
    show card_QP: "card (QinP i) ≤ 2 ^ Suc k"
      if "i ∈ P" for i 
    proof -
      have less_cardP: "iP i < k"
        using iP bij_betwE that by blast
      have card_cr: "card (QS i) ≤ 2 ^ Suc k"
      proof -
        have "card (QS i) ≤ prod card (PP i)"
          by (simp add: QS_def card_common_refinement finPP inPP_fin) 
        also have "… = prod card (XP i ∪ YP i)"
          using finPP by (simp add: PP_def prod.insert_if)
        also have "… ≤ 2 ^ Suc k" 
        proof (rule prod_le_power)
          define XS where "XS ≡ (⋃R ∈ {R∈P. iP R ≤ iP i}. {part2 (X0 i R) i})"
          define YS where "YS ≡ (⋃R ∈ {R∈P. iP R ≥ iP i}. {part2 (Y0 R i) i})"
          have 1: "{R ∈ P. iP R ≤ iP i} ⊆ iP -` {..iP i} ∩ P"
            by auto
          have "card XS ≤ card {R ∈ P. iP R ≤ iP i}"
            by (force simp add: XS_def ‹finite P› intro: order_trans [OF card_UN_le])
          also have "… ≤ card (iP -` {..iP i} ∩ P)"
            using 1 by (simp add: ‹finite P› card_mono)
          also have "… ≤ Suc (iP i)"
            by (metis card_vimage_inj_on_le bij_betw_def card_atMost finite_atMost iP)
          finally have cXS: "card XS ≤ Suc (iP i)" .
          have 2: "{R ∈ P. iP R ≥ iP i} ⊆ iP -` {iP i..<k} ∩ P"
            by clarsimp (meson bij_betw_apply iP lessThan_iff nat_less_le)
          have "card YS ≤ card {R ∈ P. iP R ≥ iP i}"
            by (force simp add: YS_def ‹finite P› intro: order_trans [OF card_UN_le])
          also have "… ≤ card (iP -` {iP i..<k} ∩ P)"
            using 2 by (simp add: ‹finite P› card_mono)
          also have "… ≤ card {iP i..<k}"
            by (meson bij_betw_def card_vimage_inj_on_le finite_atLeastLessThan iP)
          finally have "card YS ≤ k - iP i" 
            by simp
          with less_cardP cXS have k': "card XS + card YS ≤ Suc k"
            by linarith
          have finXYS: "finite (XS ∪ YS)"
            unfolding XS_def YS_def using ‹finite P› by (auto intro: finite_vimageI) 
          have "XP i ∪ YP i ⊆ XS ∪ YS"
            apply (simp add: XP_def X_def YP_def Y_def XS_def YS_def irregular_set_def image_def subset_iff)
            by (metis insert_iff linear not_le)
          then have "card (XP i ∪ YP i) ≤ card XS + card YS"
            by (meson card_Un_le card_mono finXYS order_trans)
          then show "card (XP i ∪ YP i) ≤ Suc k"
            using k' le_trans by blast
          fix x
          assume "x ∈ XP i ∪ YP i"
          then show "0 ≤ card x ∧ card x ≤ 2"
            using XP_def YP_def card_part2 by force
        qed auto
        finally show ?thesis .
      qed
      have "i' = i" if "q ⊆ i" "i'∈P" "q ∈ QS i'" for i' q
        by (metis QS_ne QS_subset_P ‹i ∈ P› disjnt_iff equals0I pairwiseD part_GP partition_on_def subset_eq that)
      then have "QinP i ⊆ QS i"
        by (auto simp: QinP_def Q_def)
      then have "card (QinP i) ≤ card (QS i)"
        by (simp add: card_mono that)
      also have "… ≤ 2 ^ Suc k"
        using QS_def card_cr by presburger
      finally show ?thesis .
    qed
    have "card Q ≤ card (⋃i∈P. QinP i)"
      unfolding Q_def
    proof (rule card_mono)
      show "(⋃ (QS ` P)) ⊆ (⋃i∈P. QinP i)"
        using ref_QP QS_subset_P Q_def QinP_def by blast
      show "finite (⋃i∈P. QinP i)"
        by (simp add: Q_def QinP_def ‹finite P›)
    qed 
    also have "… ≤ (∑i∈P. 2 ^ Suc k)"
      by (smt (verit) ‹finite P› card_QP card_UN_le order_trans sum_mono)
    finally show "card Q ≤ k * 2 ^ Suc k" 
      by (simp add: cardP)
  qed
qed

subsection ‹The Regularity Proof Itself›

text‹We start with a trivial partition (one part). If it is already $\epsilon$-regular, we are done. If
not, we refine it by applying lemma @{thm[source]"exists_refinement"} above, which increases the
energy. We can repeat this step, but it cannot increase forever: by @{thm [source]
mean_square_density_bounded} it cannot exceed~1. This defines an algorithm that must stop
after at most $\epsilon^{-5}$ steps, resulting in an $\epsilon$-regular partition.›
theorem Szemeredi_Regularity_Lemma:
  assumes "ε > 0"
  obtains M where "⋀G. card (uverts G) > 0 ⟹ ∃P. ε-regular_partition G P ∧ card P ≤ M"
proof 
  fix G
  assume "card (uverts G) > 0"
  then obtain finG: "finite (uverts G)" and nonempty: "uverts G ≠ {}"
    by (simp add: card_gt_0_iff) 
  define Φ where "Φ ≡ λQ P. refines (uverts G) Q P ∧ 
                                 mean_square_density G Q ≥ mean_square_density G P + ε^5 ∧ 
                                 card Q ≤ card P * 2 ^ Suc (card P)"
  define nxt where "nxt ≡ λP. if ε-regular_partition G P then P else SOME Q. Φ Q P"
  define iter where "iter ≡ λi. (nxt ^^ i) {uverts G}"
  define last where "last ≡ Suc (nat⌈1 / ε ^ 5⌉)"
  have iter_Suc [simp]: "iter (Suc i) = nxt (iter i)" for i
    by (simp add: iter_def)
  have Φ: "Φ (nxt P) P"
    if Pk: "partition_on (uverts G) P" and irreg: "¬ ε-regular_partition G P" for P
  proof -
    have "finite_graph_partition (uverts G) P (card P)"
      by (meson Pk finG finite_elements finite_graph_partition_def)
    then show ?thesis
      using that exists_refinement [OF _ finG irreg assms] irreg Pk
      unfolding Φ_def nxt_def by (smt (verit) someI)
  qed
  have partition_on: "partition_on (uverts G) (iter i)" for i
  proof (induction i)
    case 0
    then show ?case
      by (simp add: iter_def nonempty trivial_graph_partition_exists partition_on_space)
  next
    case (Suc i)
    with Φ show ?case
      by (metis Φ_def iter_Suc nxt_def refines_def)
  qed
  have False if irreg: "⋀i. i≤last ⟹ ¬ ε-regular_partition G (iter i)"
  proof -
    have Φ_loop: "Φ (nxt (iter i)) (iter i)" if "i≤last" for i
      using Φ irreg partition_on that by blast
    have iter_grow: "mean_square_density G (iter i) ≥ i * ε^5" if "i≤last" for i
      using that
    proof (induction i)
      case (Suc i)
      then show ?case
        by (clarsimp simp: algebra_simps) (smt (verit, best) Suc_leD Φ_def Φ_loop)
    qed (auto simp: iter_def)
    have "last * ε^5 ≤ mean_square_density G (iter last)"
      by (simp add: iter_grow)
    also have "… ≤ 1"
      by (meson finG finite_elements finite_graph_partition_def mean_square_density_bounded partition_on)
    finally have "real last * ε ^ 5 ≤ 1" .
    with assms show False
      unfolding last_def by (meson lessI natceiling_lessD not_less pos_divide_less_eq zero_less_power)
  qed
  then obtain i where "i ≤ last" and "ε-regular_partition G (iter i)"
    by force
  then have reglar: "ε-regular_partition G (iter (i + d))" for d
    by (induction d) (auto simp add: nxt_def)
  define tower where "tower ≡ λk. (power(2::nat) ^^ k) 2"
  have [simp]: "tower (Suc k) = 2 ^ tower k" for k
    by (simp add: tower_def)
  have iter_tower: "card (iter i) ≤ tower (2*i)" for i
  proof (induction i)
    case (Suc i)
    then have Qm: "card (iter i) ≤ tower (2 * i)"
      by simp
    then have *: "card (nxt (iter i)) ≤ card (iter i) * 2 ^ Suc (card (iter i))"
      using Φ by (simp add: Φ_def nxt_def partition_on)
    also have "… ≤ 2 ^ 2 ^ tower (2 * i)"
      by (metis One_nat_def Suc.IH le_tower_2 lessI numeral_2_eq_2 order.trans power_increasing_iff)
    finally show ?case
      by (simp add: Qm)
  qed (auto simp: iter_def tower_def)
  then show "∃P. ε-regular_partition G P ∧ card P ≤ tower(2 * last)"
    by (metis ‹i ≤ last› nat_le_iff_add reglar)
qed 

text ‹The actual value of the bound is visible above: a tower of exponentials of height $2(1 + \epsilon^{-5})$.›

end