Chain compression (Lemma 1 and the abstract part of Lemma 2)

A chain system splits the positive integers into chains: every n > 0 sits at position pos n of the chain key n, and elt k u is the element at position u of chain k (valid positions form an initial segment, elements increase along a chain).

comp S replaces the occupied positions of every chain by an initial segment of the same size. We show |comp S| = |S|, that comp does not decrease any |A S t| provided the multiples j * elt k e (j ≤ t) can be described by "shifted windows" in target chains (Cons), and that comp strictly decreases the sum of the elements as soon as some chain has a gap.

structure RunsOfMultiples.ChainSys (κ : Type) : Type

A partition of the positive integers into increasing chains.

• key : ℕ → κ

  The chain containing a positive integer.

• pos : ℕ → ℕ

  The position of a positive integer in its chain.

• elt : κ → ℕ → ℕ

  The integer at a given chain and position.

• vld : κ → ℕ → Prop

  The positions belonging to a chain, forming an initial segment.

• elt_key_pos (n : ℕ) : 0 < n → self.elt (self.key n) (self.pos n) = n
• vld_key_pos (n : ℕ) : 0 < n → self.vld (self.key n) (self.pos n)
• key_elt (k : κ) (u : ℕ) : self.vld k u → self.key (self.elt k u) = k
• pos_elt (k : κ) (u : ℕ) : self.vld k u → self.pos (self.elt k u) = u
• elt_pos (k : κ) (u : ℕ) : self.vld k u → 0 < self.elt k u
• vld_mono (k : κ) (u v : ℕ) : self.vld k u → v ≤ u → self.vld k v
• elt_lt (k : κ) (u v : ℕ) : self.vld k v → u < v → self.elt k u < self.elt k v

def RunsOfMultiples.ChainSys.occ {κ : Type} [DecidableEq κ] (C : ChainSys κ) (S : Finset ℕ) (k : κ) : Finset ℕ

Occupied positions of chain k.

Equations

• C.occ S k = Finset.image C.pos ({n ∈ S | C.key n = k})

def RunsOfMultiples.ChainSys.comp {κ : Type} [DecidableEq κ] (C : ChainSys κ) (S : Finset ℕ) : Finset ℕ

Compression: every chain's occupied positions become an initial segment.

Equations

• C.comp S = (Finset.image C.key S).biUnion fun (k : κ) => Finset.image (C.elt k) (Finset.range (C.occ S k).card)

def RunsOfMultiples.ChainSys.Cons {κ : Type} (C : ChainSys κ) (t : ℕ) (k : κ) : Prop

The window condition describing A S t along chain k.

Equations

• One or more equations did not get rendered due to their size.

theorem RunsOfMultiples.ChainSys.mem_occ_iff {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) {k : κ} {u : ℕ} : u ∈ C.occ S k ↔ C.vld k u ∧ C.elt k u ∈ S

theorem RunsOfMultiples.ChainSys.vld_of_lt_card {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) {k : κ} {u : ℕ} (hu : u < (C.occ S k).card) : C.vld k u

theorem RunsOfMultiples.ChainSys.mem_comp_iff {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) {n : ℕ} (hn : 0 < n) : n ∈ C.comp S ↔ C.pos n < (C.occ S (C.key n)).card

theorem RunsOfMultiples.ChainSys.comp_pos {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (n : ℕ) : n ∈ C.comp S → 0 < n

theorem RunsOfMultiples.ChainSys.occ_comp {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (k : κ) : C.occ (C.comp S) k = Finset.range (C.occ S k).card

theorem RunsOfMultiples.ChainSys.pos_injOn {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (k : κ) : Set.InjOn C.pos ↑({n ∈ S | C.key n = k})

On a chain, pos is injective.

theorem RunsOfMultiples.ChainSys.card_fibre {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (k : κ) : {n ∈ S | C.key n = k}.card = (C.occ S k).card

theorem RunsOfMultiples.ChainSys.key_mem_of_mem_comp {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) {n : ℕ} (hn : n ∈ C.comp S) : C.key n ∈ Finset.image C.key S

theorem RunsOfMultiples.ChainSys.card_comp {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) : (C.comp S).card = S.card

Compression preserves cardinality.

theorem RunsOfMultiples.ChainSys.sum_eq_sum_occ {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) : ∑ n ∈ S, n = ∑ k ∈ Finset.image C.key S, ∑ u ∈ C.occ S k, C.elt k u

The sum of a set, chain by chain.

theorem RunsOfMultiples.ChainSys.sum_range_le_sum (f : ℕ → ℕ) (P : ℕ → Prop) (hf : ∀ (u v : ℕ), P v → u < v → f u < f v) (s : ℕ) (E : Finset ℕ) : E.card = s → (∀ u ∈ E, P u) → ∑ u ∈ Finset.range s, f u ≤ ∑ u ∈ E, f u ∧ (E ≠ Finset.range s → ∑ u ∈ Finset.range s, f u < ∑ u ∈ E, f u)

Sum over an initial segment is at most the sum over any set of the same size, for a function increasing on an initial segment containing the set; strictly if the set is not the initial segment.

theorem RunsOfMultiples.ChainSys.sum_comp_le {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) : ∑ n ∈ C.comp S, n ≤ ∑ n ∈ S, n ∧ ((∃ (k : κ), C.occ S k ≠ Finset.range (C.occ S k).card) → ∑ n ∈ C.comp S, n < ∑ n ∈ S, n)

Compression does not increase the sum, and strictly decreases it if some chain has a gap.

theorem RunsOfMultiples.ChainSys.card_A_le_comp {κ : Type} [DecidableEq κ] {C : ChainSys κ} {S : Finset ℕ} (hS : ∀ n ∈ S, 0 < n) (t : ℕ) (hC : ∀ (k : κ), C.Cons t k) : (A S t).card ≤ (A (C.comp S) t).card

Lemma 1 + compression: if every chain satisfies the window condition for t, compression does not decrease |A S t|.