def CommunicationComplexity.Deterministic.Protocol.shape {X : Type u_1} {Y : Type u_2} {α : Type u_3} : Protocol X Y α → Tree Unit

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).shape = Tree.nil
• (CommunicationComplexity.Deterministic.Protocol.alice f P).shape = Tree.node () (P false).shape (P true).shape
• (CommunicationComplexity.Deterministic.Protocol.bob f P).shape = Tree.node () (P false).shape (P true).shape

def CommunicationComplexity.Deterministic.Protocol.numLeaves {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : ℕ

The number of leaves (output nodes) in a protocol, defined via its tree shape.

Equations

• p.numLeaves = p.shape.numLeaves

theorem CommunicationComplexity.tree_balanced_subtree {α : Type u_3} (t : Tree α) (hn : 1 < t.numLeaves) : ∃ (s : Tree α), CommunicationComplexity.TreeIsSubtree✝ s t ∧ 3 * s.numLeaves ≥ t.numLeaves ∧ 3 * s.numLeaves < 2 * t.numLeaves

Lemma 1.8: every binary tree with > 1 leaves has a subtree with between n/3 and 2n/3 leaves (where n = total leaves).