Bisection cut ranks of bilinear forms

The bilinear form xᵀ R y on inputs of length n is the quadratic form of the n × n matrix with R in the block whose rows are the left half and whose columns are the right half (Correlation.bipartiteMatrix). Cut the coordinates into U and Uᶜ. The block of the polar matrix with rows U and columns Uᶜ contains, on disjoint sets of columns, the block of R with rows x ∩ U and columns y \ U, and the transpose of the block with rows x \ U and columns y ∩ U. If every square block of R with k rows has rank at least k - t, then for |U| = ⌊n/2⌋ the two blocks have total rank at least ⌊n/2⌋ - 1 - 2t.

theorem Complexity.Correlation.leftIdx_injective {n : ℕ} : Function.Injective (leftIdx n)

theorem Complexity.Correlation.rightIdx_injective {n : ℕ} : Function.Injective (rightIdx n)

theorem Complexity.Correlation.leftIdx_ne_rightIdx {n : ℕ} (a b : Fin (n / 2)) : leftIdx n a ≠ rightIdx n b

theorem Complexity.Correlation.disjoint_range_leftIdx_rightIdx {n : ℕ} : Disjoint (Set.range (leftIdx n)) (Set.range (rightIdx n))

theorem Complexity.Correlation.bipartiteMatrix_apply {n : ℕ} (R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)) (a b : Fin (n / 2)) : bipartiteMatrix n R (leftIdx n a) (rightIdx n b) = R a b

theorem Complexity.Correlation.bipartiteMatrix_eq_zero {n : ℕ} (R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)) {i j : Fin n} (h : i ∉ Set.range (leftIdx n) ∨ j ∉ Set.range (rightIdx n)) : bipartiteMatrix n R i j = 0

theorem Complexity.Correlation.bilinForm_eq_quadForm {n : ℕ} (R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)) : bilinForm R = quadForm (bipartiteMatrix n R)

The bilinear form is the quadratic form of the bipartite matrix.

theorem Complexity.Correlation.ncard_preimage_add_ncard_preimage_le {n m : ℕ} {f g : Fin m → Fin n} (hf : Function.Injective f) (hg : Function.Injective g) (hfg : Disjoint (Set.range f) (Set.range g)) (V : Set (Fin n)) : (f ⁻¹' V).ncard + (g ⁻¹' V).ncard ≤ V.ncard

Two injective relabellings with disjoint ranges pull back at most |V| elements of V.

theorem Complexity.Correlation.SubmatrixRobust.min_le {m : ℕ} {R : Matrix (Fin m) (Fin m) (ZMod 2)} {t : ℕ} (hR : SubmatrixRobust R t) (A B : Set (Fin m)) : min A.ncard B.ncard ≤ blockRank R A B + t

A robust matrix has every block of rank at least its smaller side minus t.

theorem Complexity.Correlation.half_le_cutRank_bipartiteMatrix {n : ℕ} {R : Matrix (Fin (n / 2)) (Fin (n / 2)) (ZMod 2)} {t : ℕ} (hR : SubmatrixRobust R t) {U : Set (Fin n)} (hU : U.ncard = n / 2) : n / 2 ≤ cutRank (bipartiteMatrix n R) U + (2 * t + 1)

Bisection cut rank of a robust bilinear form.