noncomputable def density {m n : ℕ} (M : Fin m → Fin n → Prop) : ℕ

Equations

• density M = {x : Fin m × Fin n | match x with | (i, j) => M i j}.card

theorem density_def {n : ℕ} (M : Fin n → Fin n → Prop) [DecidableRel M] : density M = {x : Fin n × Fin n | match x with | (i, j) => M i j}.card

theorem density_mono {m n : ℕ} {M N : Fin m → Fin n → Prop} (h : ∀ (i : Fin m) (j : Fin n), M i j → N i j) : density M ≤ density N

noncomputable def row_density {n : ℕ} (M : Fin n → Fin n → Prop) (i : Fin n) : ℕ

Equations

• row_density M i = {j : Fin n | M i j}.card

noncomputable def col_density {n : ℕ} (M : Fin n → Fin n → Prop) (j : Fin n) : ℕ

Equations

• col_density M j = {i : Fin n | M i j}.card

noncomputable def ex {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (P : α → β → Prop) (n : ℕ) : ℕ

Equations

• ex P n = {M : Fin n → Fin n → Prop | ¬Contains P M}.sup density

@[simp]

theorem ex_zero {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (P : α → β → Prop) : ex P 0 = 0

theorem ex_le_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {P : α → β → Prop} {m n : ℕ} : ex P n ≤ m ↔ ∀ (M : Fin n → Fin n → Prop), ¬Contains P M → density M ≤ m

theorem le_ex_iff {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (P : α → β → Prop) (P_nonempty : ∃ (a : α) (b : β), P a b) {m n : ℕ} : m ≤ ex P n ↔ ∃ (M : Fin n → Fin n → Prop), ¬Contains P M ∧ m ≤ density M

theorem ex_le_sq {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {P : α → β → Prop} (n : ℕ) : ex P n ≤ n ^ 2

theorem density_le_ex_of_not_contains {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {n : ℕ} {P : α → β → Prop} (M : Fin n → Fin n → Prop) (AvoidP : ¬Contains P M) : density M ≤ ex P n

theorem split_density_to_rows {n : ℕ} (M : Fin n → Fin n → Prop) : density M = ∑ i : Fin n, row_density M i

theorem density_by_rows_ub {n c : ℕ} (M : Fin n → Fin n → Prop) (h_row_density_bounded : ∀ (i : Fin n), row_density M i ≤ c) : density M ≤ n * c

theorem split_density_to_cols {n : ℕ} (M : Fin n → Fin n → Prop) : density M = ∑ i : Fin n, col_density M i

theorem density_by_cols_ub {n c : ℕ} (M : Fin n → Fin n → Prop) (h_col_bounded : ∀ (i : Fin n), col_density M i ≤ c) : density M ≤ n * c

def rectPtset (n a₁ b₁ a₂ b₂ : ℕ) : Finset (Fin n × Fin n)

Equations

• rectPtset n a₁ b₁ a₂ b₂ = {a : Fin n | ↑a ∈ Finset.Ico a₁ b₁} ×ˢ {a : Fin n | ↑a ∈ Finset.Ico a₂ b₂}

noncomputable def rectPtsetMatrix {n : ℕ} (M : Fin n → Fin n → Prop) (a₁ b₁ a₂ b₂ : ℕ) : Finset (Fin n × Fin n)

Equations

• rectPtsetMatrix M a₁ b₁ a₂ b₂ = {x : Fin n × Fin n | match x with | (a, b) => M a b ∧ (a, b) ∈ rectPtset n a₁ b₁ a₂ b₂}

noncomputable def rectPtsetSubsetMatrix {n : ℕ} (M : Fin n → Fin n → Prop) (R C : Finset (Fin n)) : Finset (Fin n × Fin n)

Equations

• rectPtsetSubsetMatrix M R C = {x : Fin n × Fin n | match x with | (a, b) => M a b ∧ (a, b) ∈ R ×ˢ C}

theorem card_interval {n : ℕ} (x y : ℕ) (hy : y ≤ n) : {a : Fin n | ↑a ∈ Finset.Ico x y}.card = (Finset.Ico x y).card

@[simp]

theorem card_rectPtSet (n a₁ b₁ a₂ b₂ : ℕ) (h : b₁ ≤ n ∧ b₂ ≤ n) : (rectPtset n a₁ b₁ a₂ b₂).card = (b₁ - a₁) * (b₂ - a₂)

@[simp]

theorem card_rectPtsetSubsetMatrix {n : ℕ} (M : Fin n → Fin n → Prop) (R C : Finset (Fin n)) : (rectPtsetSubsetMatrix M R C).card ≤ R.card * C.card

theorem density_mk_mem_product {n : ℕ} (I J : Finset (Fin n)) : (density fun (i j : Fin n) => (i, j) ∈ I ×ˢ J) = I.card * J.card

theorem den_all1_matrix_row_subset {n : ℕ} (I : Finset (Fin n)) : have M := fun (i j : Fin n) => (i, j) ∈ I ×ˢ Finset.univ; density M = n * I.card

theorem den_all1_matrix_col_subset {n : ℕ} (I : Finset (Fin n)) : have M := fun (i j : Fin n) => (i, j) ∈ Finset.univ ×ˢ I; density M = n * I.card

theorem den_all1_matrix_column_interval {n : ℕ} (a b : Fin n) : have I := {x : Fin n | ↑x ∈ Finset.Icc ↑a ↑b}; have M := fun (i j : Fin n) => (i, j) ∈ Finset.univ ×ˢ I; density M = n * (↑b + 1 - ↑a)

theorem den_all1_matrix_row_interval {n : ℕ} (a b : Fin n) : have I := {x : Fin n | ↑x ∈ Finset.Icc ↑a ↑b}; have M := fun (i j : Fin n) => (i, j) ∈ I ×ˢ Finset.univ; density M = n * (↑b + 1 - ↑a)

theorem den_all1_matrix_single_row {n : ℕ} (x : Fin n) : have M := fun (i x_1 : Fin n) => i = x; density M = n

theorem den_all1_matrix_single_col {n : ℕ} (x : Fin n) : have M := fun (x_1 j : Fin n) => j = x; density M = n

theorem le_ex_self_of_two_points {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (P : α → β → Prop) (n : ℕ) (hP : ∃ (x : α × β) (y : α × β), P x.1 x.2 ∧ P y.1 y.2 ∧ x ≠ y) : n ≤ ex P n

theorem exists_av_and_ex_eq {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {n : ℕ} {P : α → β → Prop} (P_nonempty : ∃ (a : α) (b : β), P a b) : ∃ (M : Fin n → Fin n → Prop), ¬Contains P M ∧ ex P n = density M

theorem split_density {n : ℕ} (M Pred : Fin n → Fin n → Prop) : have M1 := fun (i j : Fin n) => M i j ∧ Pred i j; have M2 := fun (i j : Fin n) => M i j ∧ ¬Pred i j; density M = density M1 + density M2