The deletion game: proof internals #
Proofs behind Complexitylib.Algebraic.LinearAlgebra.Tensor.DeletionGame. Write n = 2k + 1.
- The width function.
Φ_n(r, s) ≥ 2n/3, since(n - r) + (n - s) + (r + s) = 2n, andΦ_nis2-Lipschitz in each argument. - Two intervals.
Φ_n(r, s) ≤ Tforcesr ≥ n - T,r + s ≤ T, and either2 (r + s) ≤ Tor2 (n - r - s) ≤ T, sorlies in[n - T, ⌊T/2⌋ - s]or in[⌈n - T/2⌉ - s, min (k, T - s)]. Fors ≥ 0the positionsr ∈ [1, k]withΦ_n(r, s) ≤ Tnumber at most(3T - 2n + 3) / 2: if the first interval is empty the second has at most3T/2 - n + 1points, and otherwise its length forcesT - spastk, so the second has at mostT/2 + s - kpoints; forT ≥ nthe bound exceedsk. - The count at the stopping time (
le_sub_card_add_of_lost), for the sidefthat keeps a good block. Each block has diameterL - 1, so every survivorain a good winning blockihasΦ_n(f a, s₀) ≤ Φ_n(r_i, s_i) + 4L, where(r_i, s_i)is the pair given for blockiands₀is the losing-side offset of one fixed pair. WritingV = D (T' - E), the survivors in good winning blocks thus inject into the two-interval set forT₀ = ⌊T'⌋ + 4L. The other winning blocks hold at mostR - 1survivors each, the losing side at mostR - 1per block plus the one deleted slice, and offset0at most one. There are at mostk / L + 1blocks per side. WithD ≥ 3/2andT' ≥ 2n/3,(n - card S) + V ≥ 2n + (D - 3/2) T' - D E - O(L + R n / L) ≥ (1 + 2D/3) n - D E - …. - The stopping time (
exists_stage). Both signs have a good block before any deletion (the first block on each side hasL ≥ Rslices) and neither has one after alln. At the last stageqwhere both have one, the next deletion removes at most one slice and leaves one sign without a good block. That sign plays the losing side, with the roles of the signs exchanged throughΦ_n(r, s) = Φ_n(s, r)when it is the positive sign.
The width function #
The two-interval lemma #
Blocks #
Counting survivors #
theorem
Algebraic.Tensor3.DeletionGame.Internal.card_filter_le_sum
{α : Type u_1}
[Fintype α]
(f : α → ℤ)
{k L : ℕ}
(hL : 0 < L)
(hf : ∀ (a : α), f a ≤ ↑k)
[DecidableEq α]
(U : Finset α)
:
The elements of U with f a ∈ [1, k] lie in the blocks of index < k / L + 1.
theorem
Algebraic.Tensor3.DeletionGame.Internal.card_filter_le_of_forall_lt
{α : Type u_1}
[Fintype α]
(f : α → ℤ)
{k L R : ℕ}
(hL : 0 < L)
(hf : ∀ (a : α), f a ≤ ↑k)
[DecidableEq α]
{U : Finset α}
(hU : ∀ (i : ℕ), (U ∩ sideBlock f L i).card < R)
:
A side with no good block holds at most R - 1 elements per block.
theorem
Algebraic.Tensor3.DeletionGame.Internal.card_filter_le_add_of_good
{α : Type u_1}
[Fintype α]
[DecidableEq α]
{f : α → ℤ}
{k L R : ℕ}
(hL : 0 < L)
(hf : ∀ (a : α), f a ≤ ↑k)
(S : Finset α)
:
The elements of S on the side f lie in its good blocks, or in one of the at most
k / L + 1 other blocks, each holding at most R - 1 of them.
theorem
Algebraic.Tensor3.DeletionGame.Internal.card_le_of_lost
{α : Type u_1}
[Fintype α]
[DecidableEq α]
{f : α → ℤ}
{k L R : ℕ}
(hL : 0 < L)
(hf : ∀ (a : α), -↑k ≤ f a)
{S S' : Finset α}
(hSS' : (S \ S').card ≤ 1)
(hlost : ∀ (j : ℕ), (S' ∩ sideBlock (fun (a : α) => -f a) L j).card < R)
:
If deleting at most one element of S leaves no good block on the side -f, then S has
at most (k / L + 1) (R - 1) + 1 elements on that side.
The count at the stopping time #
theorem
Algebraic.Tensor3.DeletionGame.Internal.le_sub_card_add_of_lost
{α : Type u_1}
[Fintype α]
[DecidableEq α]
{k L R : ℕ}
{D E V : ℝ}
{f : α → ℤ}
(hf : Function.Injective f)
(hfk : ∀ (a : α), -↑k ≤ f a ∧ f a ≤ ↑k)
(hR : 1 ≤ R)
(hRL : R ≤ L)
(hD : 3 / 2 ≤ D)
{S S' : Finset α}
(hSS' : (S \ S').card ≤ 1)
(hlost : ∀ (j : ℕ), (S' ∩ sideBlock (fun (a : α) => -f a) L j).card < R)
{i₁ j₀ : ℕ}
(hi₁ : R ≤ (S ∩ sideBlock f L i₁).card)
(hH :
∀ (i : ℕ),
R ≤ (S ∩ sideBlock f L i).card →
∃ a ∈ sideBlock f L i, ∃ b ∈ sideBlock (fun (a : α) => -f a) L j₀, D * (↑(phi (2 * ↑k + 1) (f a) (-f b)) - E) ≤ V)
:
Offsets #
The stopping time #
theorem
Algebraic.Tensor3.DeletionGame.Internal.card_sdiff_take_succ_le_one
{α : Type u_1}
[Fintype α]
[DecidableEq α]
(l : List α)
(q : ℕ)
:
Deleting one more element of a list removes at most one element from the survivors.