Theory Transitive_Union_Closed_Families

(*Session: Transitive_Union_Closed_Families
  Title: Transitive Union-Closed Families
  Authors: Angeliki Koutsoukou-Argyraki, Royal Holloway, University of London and University of Cambridge
  and Lawrence C. Paulson, University of Cambridge
  Date: 24 December 2024.*)



section‹Transitive Union-Closed Families›


text‹ A family of sets is union-closed if the union of any two sets from the family is in the family. 
The Union-Closed Conjecture is an open problem in combinatorics posed by Frankl in 1979. It
states that for every finite, union-closed family of sets (other than the family containing 
only the empty set) there exists an element that belongs to at least half of the sets in the family.
We formalise a proof by Aaronson, Ellis and Leader showing that the Union-Closed Conjecture 
holds for the union-closed family generated by the cyclic translates of any fixed set 
\cite{Aaronson_Ellis_Leader}.›


theory Transitive_Union_Closed_Families 
  imports "Pluennecke_Ruzsa_Inequality.Pluennecke_Ruzsa_Inequality"

begin

no_notation equivalence.Partition (infixl "'/" 75)

definition union_closed:: "'a set set ⇒ bool" 
  where "union_closed ℱ ≡ (∀A∈ℱ. ∀ B∈ℱ. A ∪ B ∈ ℱ)"

abbreviation set_difference :: "['a set,'a set] ⇒ 'a set" (infixl "∖" 65)
  where "A ∖ B ≡ A-B"

locale Family = additive_abelian_group +
  fixes R 
  assumes finG: "finite G"
  assumes RG: "R ⊆ G"
  assumes R_nonempty: "R ≠ {}" 

begin

definition union_closed_conjecture_property:: "'a set set ⇒ bool"
  where "union_closed_conjecture_property ℱ 
       ≡ ∃𝒳⊆ℱ. ∃x∈G. x ∈ ⋂𝒳 ∧ card 𝒳 ≥ card ℱ / 2"

definition "Neighbd ≡ λA. sumset A R"

definition "Interior ≡ λA. {x∈G. sumset {x} R ⊆ A}"

definition "ℱ ≡ Neighbd ` Pow G" 

text‹We show that the family @{term ℱ} as defined above and appears in the statement of the theorem 
\cite{Aaronson_Ellis_Leader} is actually a finite, nonempty union-closed family indeed.›

lemma cardℱ_gt0 [simp]: "card ℱ > 0" and finiteℱ: "finite ℱ"
  using ℱ_def finG by fastforce+

lemma "union_closed ℱ"    
proof-
  have *:"∀ A ⊆ G. ∀ B ⊆ G. (sumset A R) ∪ (sumset B R) = sumset (A ∪ B) R"
    by (simp add: sumset_subset_Un1)
  show ?thesis using *  
    by (auto simp: union_closed_def ℱ_def Neighbd_def)
qed

lemma cardG_gt0: "card G > 0"
  using RG R_nonempty card_0_eq finG by blast

lemma ℱ_subset: "ℱ ⊆ Pow G"
  by (simp add: Neighbd_def PowI ℱ_def image_subset_iff sumset_subset_carrier)

subsection‹Proof of the main theorem›

lemma card_Interior_le:
  assumes "S ⊆ G"
  shows "card (Interior S) ≤ card S"
proof -
  obtain r where "r ∈ R"
    using R_nonempty by blast
  show ?thesis
  proof (intro card_inj_on_le)
    let ?f = "(λx. x ⊕ r)"
    show "inj_on ?f (Interior S)" "?f ` Interior S ⊆ S"
      using RG ‹r ∈ R› by (auto simp: Interior_def inj_on_def)
    show "finite S"
      using assms finG finite_subset by blast
  qed
qed

lemma Interior_subset_G [iff]: "Interior S ⊆ G"
  using Interior_def by auto

lemma Neighbd_subset_G [iff]: "Neighbd S ⊆ G"
  by (simp add: Neighbd_def sumset_subset_carrier)

lemma average_ge: 
  shows "(∑S∈ℱ.(card S)) / card ℱ ≥ card G / 2"
proof-
  define f where "f ≡ λS. minusset (G ∖ Interior S)" 

  text‹The following corresponds to (1) in the paper.›
  have 1: "card S + card (f S) ≥ card G" if "S ⊆ G" for S
  proof-
    have "card (f S) = card G - card (Interior S)"
      unfolding f_def
      by (metis Diff_subset Interior_subset_G card_Diff_subset card_minusset' finG finite_subset)
    with that show ?thesis using card_Interior_le
      by (metis (no_types, lifting) add.commute diff_le_mono2 le_diff_conv)
  qed

  text‹The following corresponds to (2) in the paper.›
  have 2: "f S = sumset (minusset (G ∖ S)) R" if "S ⊆ G" for S
  proof-
    have *: "x ∈ f S ⟷ x ∈ sumset (minusset (G ∖ S)) R" if "x ∈ G" for x
    proof -
      have "x ∈ f S ⟷ inverse x ∉ Interior S"
        using that minusset.simps by (fastforce simp: f_def)+
      also have "… ⟷ (sumset {inverse x} R) ∩ (G∖S) ≠ {}"
        using sumset_subset_carrier that by (auto simp: Interior_def)
      also have "… ⟷ x ∈ sumset (minusset (G∖S)) R"
      proof
        assume L: "sumset {inverse x} R ∩ (G ∖ S) ≠ {}"
        then obtain r where r: "inverse x ⊕ r ∉ S" and "r ∈ R"
          using ‹S ⊆ G› ‹x ∈ G› by (auto simp: sumset_eq minusset_eq)
        then have "inverse (inverse x ⊕ r) ∈ minusset (G ∖ S)"
          using RG that by auto
        moreover have "x = inverse (inverse x ⊕ r) ⊕ r"
          using RG ‹r ∈ R› that commutative inverse_composition_commute invertible_right_inverse2 
          by auto
        ultimately show "x ∈ sumset (minusset (G ∖ S)) R"
          by (metis RG ‹r ∈ R› minusset_subset_carrier subset_eq sumset.simps)
      next
        assume R: "x ∈ sumset (minusset (G ∖ S)) R"
        then obtain g r where *: "g∈G" "g ∉ S" "r∈R" "x = inverse g ⊕ r"
          by (metis Diff_iff minusset.simps sumset.cases)
        show "sumset {inverse x} R ∩ (G ∖ S) ≠ {}"
        proof
          assume "sumset {inverse x} R ∩ (G ∖ S) = {}"
          then have "g ∉ sumset {inverse x} R" 
            using ‹g ∉ S› sumset_subset_carrier that by fastforce
          then have "g ≠ local.inverse (local.inverse g ⊕ r) ⊕ r"
            using * RG that by (auto simp: sumset_eq)
          with * RG that show False
            by (metis commutative invertible invertible_left_inverse2 invertible_right_inverse2 subset_eq)
        qed
      qed
      finally show ?thesis .
    qed
    show ?thesis
    proof
      show "f S ⊆ sumset (minusset (G ∖ S)) R"
      using "*" f_def minusset_subset_carrier by blast
    next
      show "sumset (minusset (G ∖ S)) R ⊆ f S"
      by (meson "*" subset_iff sumset_subset_carrier)
    qed
  qed
  then have "f ` Pow G ⊆ ℱ"
    by (auto simp: Neighbd_def ℱ_def minusset_subset_carrier)

  text‹The following corresponds to (3) in the paper.›

  have 3: "Neighbd (Interior (sumset A R)) = sumset A R" 
    if "A ⊆ G" for A
    using that by (force simp: sumset_eq Neighbd_def Interior_def)
  
  text‹"Putting everything together": ›
  moreover
  have "sumset X R = sumset Y R"
    if "X ⊆ G" "Y ⊆ G"
      "minusset (G ∖ Interior (sumset X R)) = minusset (G ∖ Interior (sumset Y R))"
    for X Y
    using that 3
    by (metis Diff_Diff_Int Int_absorb2 Interior_subset_G inf_commute minus_minusset)
  ultimately have "inj_on f ℱ"
    by (auto simp: inj_on_def ℱ_def f_def Neighbd_def)
  moreover have "f ` ℱ ⊆ ℱ"
    using 2 ℱ_def ‹f ` Pow G ⊆ ℱ› by force
  moreover have "ℱ ⊆ f ` ℱ"
    by (metis ‹inj_on f ℱ› ‹f ` ℱ ⊆ ℱ› endo_inj_surj finiteℱ)
  ultimately have "bij_betw f ℱ ℱ" 
    by (simp add: bij_betw_def)
  then have sum_card_eq: "(∑S∈ℱ. card (f S)) = (∑S∈ℱ. card S)"
    by (simp add: sum.reindex_bij_betw)

  have "card G / 2 = (1 / (2 * card ℱ)) * (∑S∈ℱ. card G)"
    by simp
  also have "… ≤ (1 / (2 * card ℱ)) * (∑S∈ℱ. card S + card (f S))"
    by (intro sum_mono mult_left_mono of_nat_mono 1) (auto simp: ℱ_def)
  also have "… = (1 / card ℱ) * (∑S∈ℱ. card S)"
    by (simp add: sum_card_eq sum.distrib)
  finally show ?thesis
    by argo
qed

text‹We have thus shown that the average size of a set in the family @{term ℱ} is
at least $|G|/2$, proving the first part of Theorem 2 in the paper \cite{Aaronson_Ellis_Leader}. 
Using this, we will now show the main statement, i.e. that the Union-Closed Conjecture holds for 
the family @{term ℱ}.›
 

theorem Aaronson_Ellis_Leader_union_closed_conjecture:
  shows "union_closed_conjecture_property ℱ"
proof -
  ― ‹First, quite a big calculation not mentioned in the article:
      counting all the elements in two different ways.›
have *: "(∑S∈ℱ.(card S)) = (∑x∈G. card {S∈ℱ. x∈S})"
    using finiteℱ ℱ_subset
  proof induction
    case empty
    then show ?case 
      by simp
  next
    case (insert S 𝒢)
    then have A: "{T. (T = S ∨ T∈𝒢) ∧ x∈T} 
                 = {T∈𝒢. x∈T} ∪ (if x∈S then {S} else {})"
      for x
      by auto
    have B: "card {T. (T = S ∨ T∈𝒢) ∧ x∈T} 
           = card {T∈𝒢. x∈T} + (if x∈S then 1 else 0)"
      for x
      by (simp add: A card_insert_if insert)
    have "S = (⋃x∈G. if x ∈ S then {x} else {})"
      using insert.prems by auto
    then have "card S = card (⋃x∈G. if x ∈ S then {x} else {})"
      by simp
    also have "… = (∑i∈G. card (if i ∈ S then {i} else {}))"
      by (intro card_UN_disjoint) (auto simp: finG)
    also have "… = (∑x∈G. if x ∈ S then 1 else 0)"
      by (force intro: sum.cong)
    finally have C: "card S = (∑x∈G. if x ∈ S then 1 else 0)" .
    show ?case
      using insert by (auto simp: sum.distrib B C)
  qed
 
  have "1/2 ≤ (sum card ℱ) / (card ℱ * card G)"
    using mult_right_mono [OF average_ge, of "1 / card G"] 
    using cardG_gt0 by (simp add: divide_simps split: if_splits)
  also have "… = (∑x∈G. ((card {S∈ℱ. x∈S}) / (card  ℱ))) / card G"
    by (simp add: * sum_divide_distrib)
  finally have **: "1/2 ≤ (∑x∈G. card {S∈ℱ. x∈S} / card ℱ) / card G" .
    ― ‹There is a typo in the paper (bottom of page): 
               instead of @{term "x ∈ S"} it says @{term "x ∈ ℱ"}.›
  show ?thesis
  proof (rule ccontr)  ―‹Contradict the inequality proved above›
    assume "¬ union_closed_conjecture_property ℱ"
    then have A: "⋀𝒳 x. ⟦𝒳⊆ℱ; x∈G; x ∈ ⋂𝒳⟧ ⟹ card 𝒳 < card ℱ / 2"
      by (fastforce simp: union_closed_conjecture_property_def)
    have "(∑x∈G. real (card {S∈ℱ. x∈S})) < (∑x∈G. card ℱ / 2)"
    proof (intro sum_strict_mono)
      fix x :: 'a
      assume "x ∈ G"
      then have "card {S∈ℱ. x∈S} < card ℱ / 2"
        by (intro A) auto
      then show "real (card {S∈ℱ. x∈S}) < real (card ℱ) / 2"
        by blast
    qed (use unit_closed finG in auto)
    also have "… = card ℱ * (card G / 2)"
      by simp
    finally have B: "(∑x∈G. real (card {S∈ℱ. x∈S})) < card ℱ * (card G / 2)" .
    have "(∑x∈G. card {S∈ℱ. x∈S} / card ℱ) / card G < 1/2"
      using divide_strict_right_mono [OF B, of "card ℱ * card G"]
      using cardG_gt0
      by (simp add: divide_simps sum_divide_distrib)
    with ** show False
      by argo
  qed
qed

end

end