noncomputable def CommunicationComplexity.Deterministic.Rank.boolFunctionMatrix {X : Type u_1} {Y : Type u_2} (f : X → Y → Bool) : Matrix X Y ℝ

The real-valued matrix of a Boolean function f : X → Y → Bool, where the (x, y) entry is 1 if f x y = true and 0 otherwise.

Equations

• CommunicationComplexity.Deterministic.Rank.boolFunctionMatrix f = Matrix.of fun (x : X) (y : Y) => if f x y = true then 1 else 0

noncomputable def CommunicationComplexity.Deterministic.Rank.boolFunctionRank {X : Type u_1} {Y : Type u_2} [Fintype Y] (f : X → Y → Bool) : ℕ

The rank of a Boolean function f, defined as the rank of its real-valued matrix over ℝ.

Equations

• CommunicationComplexity.Deterministic.Rank.boolFunctionRank f = (CommunicationComplexity.Deterministic.Rank.boolFunctionMatrix f).rank

noncomputable def CommunicationComplexity.Deterministic.Rank.rectMatrix {X : Type u_1} {Y : Type u_2} (R : Set (X × Y)) : Matrix X Y ℝ

The {0,1}-matrix of a subset R ⊆ X × Y.

Equations

• CommunicationComplexity.Deterministic.Rank.rectMatrix R = Matrix.of fun (x : X) (y : Y) => if (x, y) ∈ R then 1 else 0

theorem CommunicationComplexity.Deterministic.Rank.rank_rectMatrix_le_one {X : Type u_1} {Y : Type u_2} [Fintype Y] (R : Set (X × Y)) (hR : Rectangle.IsRectangle R) : (rectMatrix R).rank ≤ 1

For a rectangle R = A ×ˢ B, rectMatrix R is an outer product, hence has rank ≤ 1.

theorem Matrix.rank_add_le {X : Type u_1} {Y : Type u_2} [Fintype Y] (A B : Matrix X Y ℝ) : (A + B).rank ≤ A.rank + B.rank

Matrix rank is subadditive: rank (A + B) ≤ rank A + rank B.

theorem Matrix.rank_sum_le {X : Type u_1} {Y : Type u_2} [Fintype Y] {ι : Type u_3} (s : Finset ι) (A : ι → Matrix X Y ℝ) : (∑ i ∈ s, A i).rank ≤ ∑ i ∈ s, (A i).rank

Matrix rank is subadditive over finite sums.

theorem CommunicationComplexity.Deterministic.Rank.boolFunctionRank_le_ncard {X : Type u_1} {Y : Type u_2} [Finite X] [Fintype Y] (f : X → Y → Bool) (Part : Set (Set (X × Y))) (hPart : Rectangle.IsMonoPartition Part f) : boolFunctionRank f ≤ Part.ncard

The rank of a Boolean function is at most the number of rectangles in any monochromatic rectangle partition. Each true-mono rectangle contributes a rank-1 matrix, M_f is their sum, and rank is subadditive.

theorem CommunicationComplexity.Deterministic.Rank.boolFunctionRank_le_pow_of_communicationComplexity_le {X : Type u_1} {Y : Type u_2} [Finite X] [Fintype Y] (f : X → Y → Bool) (n : ℕ) (h : communicationComplexity f ≤ ↑n) : boolFunctionRank f ≤ 2 ^ n

If the deterministic CC of f is at most n, then the rank of f is at most 2^n.

theorem CommunicationComplexity.Deterministic.Rank.log_rank_lower_bound {X : Type u_1} {Y : Type u_2} [Finite X] [Fintype Y] (f : X → Y → Bool) : ↑(Nat.clog 2 (boolFunctionRank f)) ≤ communicationComplexity f

Log-rank lower bound: the deterministic communication complexity of a Boolean function f is at least ⌈log₂(rank f)⌉.