Documentation

LeanPool.Erdos865.FoldedAux

The four sets T₁,…,T₄ and their pairwise intersections #

Supporting material for the folded additive lemma: the images T₁,…,T₄ of B inside ZMod m, their cardinalities, and the pairwise-intersection bounds culminating in the four-set union bound case2_bound.

Generic helpers #

source
theorem Erdos865.four_card_le {X : Type u_1} [DecidableEq X] (s1 s2 s3 s4 : Finset X) :
s1.card + s2.card + s3.card + s4.card ≤ (s1 ∪ s2 ∪ s3 ∪ s4).card + ((s1 ∩ s2).card + (s1 ∩ s3).card + (s1 ∩ s4).card + (s2 ∩ s3).card + (s2 ∩ s4).card + (s3 ∩ s4).card)
source
theorem Erdos865.card_two_sol (m : ℕ) [NeZero m] (c : ZMod m) :
{x : ZMod m | 2 * x = c}.card ≤ 2

The four sets T₁,…,T₄ in ZMod m #

source
def Erdos865.T1 (m : ℕ) (B : Finset ℕ) :
Finset (ZMod m)

T₁ = B inside ZMod m.

Equations
Instances For
    source
    def Erdos865.T2 (m : ℕ) (B : Finset ℕ) :
    Finset (ZMod m)

    T₂ = -B inside ZMod m.

    Equations
    Instances For
      source
      def Erdos865.T3 (m : ℕ) (B : Finset ℕ) (α : ℕ) :
      Finset (ZMod m)

      T₃ = (B - α) \ {0} inside ZMod m.

      Equations
      Instances For
        source
        def Erdos865.T4 (m : ℕ) (B : Finset ℕ) (β : ℕ) :
        Finset (ZMod m)

        T₄ = (β - B) \ {0} inside ZMod m.

        Equations
        Instances For
          source
          theorem Erdos865.cast_injOn {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
          Set.InjOn (fun (b : ℕ) => ↑b) ↑B
          source
          theorem Erdos865.card_T1 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
          (T1 m B).card = B.card
          source
          theorem Erdos865.card_T2 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
          (T2 m B).card = B.card
          source
          theorem Erdos865.card_T3 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B) :
          (T3 m B α).card = B.card - 1
          source
          theorem Erdos865.card_T4 {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ} (hβ : β ∈ B) :
          (T4 m B β).card = B.card - 1
          source
          theorem Erdos865.union_card_le {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) (α β : ℕ) :
          (T1 m B ∪ T2 m B ∪ T3 m B α ∪ T4 m B β).card ≤ m - 1

          The pairwise intersection bounds #

          source
          theorem Erdos865.inter_T1_T2_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) :
          (T1 m B ∩ T2 m B).card ≤ 1
          source
          theorem Erdos865.inter_T1_T2_odd {m : ℕ} (hodd : ¬2 ∣ m) {B : Finset ℕ} (hB : FoldedOK m B) :
          T1 m B ∩ T2 m B = ∅
          source
          theorem Erdos865.inter_T1_T3_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B) :
          (T1 m B ∩ T3 m B α).card ≤ 1
          source
          theorem Erdos865.inter_T2_T3_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α : ℕ} (hα : α ∈ B) (hmin : ∀ x ∈ B, α ≤ x) :
          (T2 m B ∩ T3 m B α).card ≤ 1
          source
          theorem Erdos865.inter_T2_T4_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ} (hβ : β ∈ B) :
          (T2 m B ∩ T4 m B β).card ≤ 1
          source
          theorem Erdos865.inter_T1_T4_le {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {β : ℕ} (hβ : β ∈ B) :
          (T1 m B ∩ T4 m B β).card ≤ 2
          source
          theorem Erdos865.inter_T3_T4_le {m : ℕ} {B : Finset ℕ} (hB : FoldedOK m B) {α β : ℕ} (hα : α ∈ B) (hβ : β ∈ B) (hαβ : α < β) (hmin : ∀ x ∈ B, α ≤ x) (hmin2 : ∀ x ∈ B, x ≠ α → β ≤ x) (hsum : α + β < m) (hnc : α + β ∉ collisions m B) :
          (T3 m B α ∩ T4 m B β).card ≤ 2

          The Case 2 bound #

          source
          theorem Erdos865.case2_bound {m : ℕ} (hm : 2 ≤ m) {B : Finset ℕ} (hB : FoldedOK m B) {α β : ℕ} (hα : α ∈ B) (hβ : β ∈ B) (hαβ : α < β) (hmin : ∀ x ∈ B, α ≤ x) (hmin2 : ∀ x ∈ B, x ≠ α → β ≤ x) (hsum : α + β < m) (hnc : α + β ∉ collisions m B) :
          4 * B.card ≤ m + 8