def CommunicationComplexity.Rectangle.IsRectangle {X : Type u_1} {Y : Type u_2} (S : Set (X × Y)) : Prop

A subset of X × Y is a rectangle if it factors as A ×ˢ B.

Equations

• CommunicationComplexity.Rectangle.IsRectangle S = ∃ (A : Set X) (B : Set Y), S = A ×ˢ B

theorem CommunicationComplexity.Rectangle.IsRectangle_iff {X : Type u_1} {Y : Type u_2} (R : Set (X × Y)) : IsRectangle R ↔ ∀ (x x' : X) (y y' : Y), (x, y) ∈ R → (x', y') ∈ R → (x', y) ∈ R ∧ (x, y') ∈ R

Characterization of rectangles by the cross property: if (x,y) and (x',y') are in R, then the mixed pairs are also in R.

def CommunicationComplexity.Rectangle.IsMonochromatic {X : Type u_1} {Y : Type u_2} {α : Type u_3} (S : Set (X × Y)) (g : X → Y → α) : Prop

A set is monochromatic for g if g is constant on that set.

Equations

• CommunicationComplexity.Rectangle.IsMonochromatic S g = ∀ (x x' : X) (y y' : Y), (x, y) ∈ S → (x', y') ∈ S → g x y = g x' y'

def CommunicationComplexity.Rectangle.IsFoolingSet {X : Type u_1} {Y : Type u_2} {α : Type u_3} (S : Set (X × Y)) (g : X → Y → α) : Prop

A set S ⊆ X × Y is a fooling set for g if every monochromatic rectangle with respect to g contains at most one point of S.

Equations

• One or more equations did not get rendered due to their size.

def CommunicationComplexity.Rectangle.IsMonoPartition {X : Type u_1} {Y : Type u_2} {α : Type u_3} (Part : Set (Set (X × Y))) (g : X → Y → α) : Prop

A set of sets is a monochromatic rectangle partition of X × Y with respect to g if every member is a rectangle, every member is monochromatic for g, the members cover X × Y, and distinct members are disjoint.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Rectangle.monoPartition_point_mem {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} (h : IsMonoPartition Part g) (p : X × Y) : ∃ R ∈ Part, p ∈ R

Every point is in some member of a monochromatic rectangle partition.

theorem CommunicationComplexity.Rectangle.monoPartition_part_unique {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} (h : IsMonoPartition Part g) {R S : Set (X × Y)} (hR : R ∈ Part) (hS : S ∈ Part) {p : X × Y} (hp1 : p ∈ R) (hp2 : p ∈ S) : R = S

If a point is in two parts of a monochromatic rectangle partition, the parts must be equal.

theorem CommunicationComplexity.Rectangle.monoPartition_cross_mem {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} (h : IsMonoPartition Part g) {R : Set (X × Y)} (hR : R ∈ Part) {x x' : X} {y y' : Y} (hxy : (x, y) ∈ R) (hx'y' : (x', y') ∈ R) : (x', y) ∈ R ∧ (x, y') ∈ R

In a monochromatic rectangle partition, if (x,y) and (x',y') are in the same part, then so are (x',y) and (x,y').

theorem CommunicationComplexity.Rectangle.monoPartition_values_eq {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} (h : IsMonoPartition Part g) {R : Set (X × Y)} (hR : R ∈ Part) {x x' : X} {y y' : Y} (hxy : (x, y) ∈ R) (hx'y' : (x', y') ∈ R) : g x y = g x' y'

In a monochromatic rectangle partition, any two points in the same part have equal function values.

theorem CommunicationComplexity.Rectangle.foolingSet_encard_le_of_monoPartition {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} {S : Set (X × Y)} (hS : IsFoolingSet S g) (hPart : IsMonoPartition Part g) : S.encard ≤ Part.encard

Any monochromatic rectangle partition has at least as many parts as any fooling set for the same function.

theorem CommunicationComplexity.Rectangle.foolingSet_ncard_le_of_monoPartition {X : Type u_1} {Y : Type u_2} {α : Type u_3} {Part : Set (Set (X × Y))} {g : X → Y → α} {S : Set (X × Y)} (hS : IsFoolingSet S g) (hPart : IsMonoPartition Part g) (hfin : Part.Finite) : S.ncard ≤ Part.ncard

Any finite monochromatic rectangle partition has at least as many parts as any fooling set for the same function.