Definitions

def PermPattern {n : ℕ} (σ : Equiv.Perm (Fin n)) (i j : Fin n) : Prop

Equations

• PermPattern σ i j = (σ i = j)

@[simp]

theorem permPattern_one (n : ℕ) : PermPattern 1 = IdentityPattern n

@[simp]

theorem permPattern_refl (n : ℕ) : PermPattern (Equiv.refl (Fin n)) = IdentityPattern n

Proofs

theorem ex_identityPattern_le (k n : ℕ) : ex (IdentityPattern k) n ≤ (2 * n - 1) * (k - 1)

Marcus Tardos' theorem

def rectPtsetq (n q i j : ℕ) : Finset (Fin n × Fin n)

Equations

• rectPtsetq n q i j = rectPtset n (q * i) (q * (i + 1)) (q * j) (q * (j + 1))

noncomputable def rectPtsetqMatrix {n : ℕ} (M : Fin n → Fin n → Prop) (q i j : ℕ) : Finset (Fin n × Fin n)

Equations

• rectPtsetqMatrix M q i j = {x : Fin n × Fin n | match x with | (a, b) => M a b ∧ (a, b) ∈ rectPtsetq n q i j}

def blkMatrix {n : ℕ} (M : Fin n → Fin n → Prop) (q : ℕ) : Fin (n / q) → Fin (n / q) → Prop

Equations

• blkMatrix M q i j = ∃ (p : Fin n × Fin n), M p.1 p.2 ∧ p ∈ rectPtsetq n q ↑i ↑j

noncomputable def blk_den {n q : ℕ} (M : Fin n → Fin n → Prop) (i j : Fin (n / q)) : ℕ

Equations

• blk_den M i j = (rectPtsetqMatrix M q ↑i ↑j).card

theorem den_eq_sum_blk_den {n q : ℕ} (M : Fin n → Fin n → Prop) (hqn : q ∣ n) : let B := blkMatrix M q; density M = ∑ x : Fin (n / q) × Fin (n / q) with match x with | (i, j) => B i j, match x with | (i, j) => blk_den M i j

theorem den_submatrix_eq_sum_blk_den {n q : ℕ} (M : Fin n → Fin n → Prop) (hqn : q ∣ n) (f1 : Fin (n / q) → Fin (n / q) → Prop) : have B := blkMatrix M q; let B1 := fun (i j : Fin (n / q)) => B i j ∧ f1 i j; have fq := fun (x : Fin n) => ⟨↑x / q, ⋯⟩; have M1 := fun (i j : Fin n) => M i j ∧ B1 (fq i) (fq j); let Q := Fin (n / q) × Fin (n / q); density M1 = ∑ x : Q with match x with | (i, j) => B1 i j, match x with | (i, j) => blk_den M i j

theorem split_density_blk {n q : ℕ} (hqn : q ∣ n) (M : Fin n → Fin n → Prop) (f1 f2 : Fin (n / q) → Fin (n / q) → Prop) : let Q := Fin (n / q) × Fin (n / q); let f3 := fun (i j : Fin (n / q)) => ¬f1 i j ∧ ¬f2 i j; have B := blkMatrix M q; let B1 := fun (i j : Fin (n / q)) => B i j ∧ f1 i j; let B2 := fun (i j : Fin (n / q)) => B i j ∧ f2 i j; let N := fun (i j : Fin (n / q)) => B i j ∧ f3 i j; density M ≤ ((∑ x : Q with match x with | (i, j) => B1 i j, match x with | (i, j) => blk_den M i j) + ∑ x : Q with match x with | (i, j) => B2 i j, match x with | (i, j) => blk_den M i j) + ∑ x : Q with match x with | (i, j) => N i j, match x with | (i, j) => blk_den M i j

theorem sum_blk_den_le_mul_den_blk {n q c : ℕ} (M : Fin n → Fin n → Prop) (B : Fin (n / q) → Fin (n / q) → Prop) (h : ∀ (i j : Fin (n / q)), B i j → blk_den M i j ≤ c) : (∑ x : Fin (n / q) × Fin (n / q) with match x with | (i, j) => B i j, match x with | (i, j) => blk_den M i j) ≤ c * density B

theorem av_perm_contract_av_perm {k n : ℕ} (q : ℕ) (σ : Equiv.Perm (Fin k)) (M : Fin n → Fin n → Prop) (hM : ¬Contains (PermPattern σ) M) : ¬Contains (PermPattern σ) (blkMatrix M q)

theorem density_WB {n k : ℕ} (h_n : 0 < n) (h_k : k ^ 2 ∣ n) (M : Fin n → Fin n → Prop) {σ : Equiv.Perm (Fin k)} (M_avoid_perm : ¬Contains (PermPattern σ) M) : have q := k ^ 2; have B := blkMatrix M q; have W := fun (i j : Fin (n / q)) => k ≤ {c : Fin n | ∃ (r : Fin n), (r, c) ∈ rectPtsetqMatrix M q ↑i ↑j}.card; have WB := fun (i j : Fin (n / q)) => W i j ∧ B i j; density WB ≤ n / k ^ 2 * (k * (k ^ 2).choose k)

theorem density_TB {n k : ℕ} (h_n : 0 < n) (h_k : k ^ 2 ∣ n) (M : Fin n → Fin n → Prop) {σ : Equiv.Perm (Fin k)} (M_avoid_perm : ¬Contains (PermPattern σ) M) : have q := k ^ 2; have B := blkMatrix M q; have T := fun (i j : Fin (n / q)) => k ≤ {r : Fin n | ∃ (c : Fin n), (r, c) ∈ rectPtsetqMatrix M q ↑i ↑j}.card; have TB := fun (i j : Fin (n / q)) => T i j ∧ B i j; density TB ≤ n / k ^ 2 * (k * (k ^ 2).choose k)

theorem blk_den_SB {n : ℕ} (k : ℕ) (M : Fin n → Fin n → Prop) : have q := k ^ 2; have B := blkMatrix M q; have W := fun (i j : Fin (n / q)) => k ≤ {c : Fin n | ∃ (r : Fin n), (r, c) ∈ rectPtsetqMatrix M q ↑i ↑j}.card; have T := fun (i j : Fin (n / q)) => k ≤ {r : Fin n | ∃ (c : Fin n), (r, c) ∈ rectPtsetqMatrix M q ↑i ↑j}.card; have S := fun (i j : Fin (n / q)) => ¬W i j ∧ ¬T i j; have SB := fun (i j : Fin (n / q)) => S i j ∧ B i j; ∀ (i j : Fin (n / q)), SB i j → blk_den M i j ≤ (k - 1) ^ 2

theorem ex_perm_recurrence {k : ℕ} (σ : Equiv.Perm (Fin k)) (n : ℕ) (hkn : k ^ 2 ∣ n) : ex (PermPattern σ) n ≤ (k - 1) ^ 2 * ex (PermPattern σ) (n / k ^ 2) + 2 * n * k ^ 3 * (k ^ 2).choose k

theorem ex_permPattern_le {k : ℕ} (σ : Equiv.Perm (Fin k)) (n : ℕ) : ex (PermPattern σ) n ≤ 2 * k ^ 4 * (k ^ 2).choose k * n

theorem le_ex_permPattern {k : ℕ} (σ : Equiv.Perm (Fin k)) (n : ℕ) (hk : 2 ≤ k) : n ≤ ex (PermPattern σ) n