structure CommunicationComplexity.Deterministic.OneWay.Protocol (X : Type u_4) (Y : Type u_5) (α : Type u_6) : Type (max (max (max 1 u_4) u_5) u_6)

A one-way deterministic communication protocol.

Message is the protocol's message codebook (language): the finite set of admissible full one-shot messages Alice may send. It is not the base symbol alphabet/signature (for example, bits), but whole message values (codewords).

• Message : Type

  The message codebook/language: all admissible complete one-shot messages.

• instFintypeMessage : Fintype self.Message

  Finiteness of the message codebook, needed to assign a bit cost.

• instNonemptyMessage : Nonempty self.Message

  Nonemptiness of the codebook (mirrors existing finite-message conventions).

• send : X → self.Message

  Alice's encoder: picks a codeword/message from the protocol codebook.

• decode : self.Message → Y → α

  Bob's local decoder from received message and Bob's input.

def CommunicationComplexity.Deterministic.OneWay.Protocol.run {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (x : X) (y : Y) : α

Execute a one-way protocol on input (x, y).

Equations

• p.run x y = p.decode (p.send x) y

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

Protocol-level communication cost in bits: ⌈log₂ |Message|⌉, where Message is the protocol codebook/language.

Equations

• p.cost = Nat.clog 2 (Fintype.card p.Message)

def CommunicationComplexity.Deterministic.OneWay.Protocol.Computes {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (f : X → Y → α) : Prop

A one-way protocol computes f when its execution agrees with f everywhere.

Equations

• p.Computes f = (p.run = f)

noncomputable def CommunicationComplexity.Deterministic.OneWay.Protocol.toFiniteMessage {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Fintype α] [Nonempty α] (p : Protocol X Y α) : FiniteMessage.Protocol X Y α

Embed a one-way protocol into the finite-message interactive model by having Alice send the one-way message, then Bob send the decoded output.

Equations

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

@[simp]

theorem CommunicationComplexity.Deterministic.OneWay.Protocol.toFiniteMessage_run {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Fintype α] [Nonempty α] (p : Protocol X Y α) (x : X) (y : Y) : p.toFiniteMessage.run x y = p.run x y

@[simp]

theorem CommunicationComplexity.Deterministic.OneWay.Protocol.toFiniteMessage_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Fintype α] [Nonempty α] (p : Protocol X Y α) : p.toFiniteMessage.complexity = p.cost + Nat.clog 2 (Fintype.card α)

noncomputable def CommunicationComplexity.Deterministic.OneWay.communicationComplexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) : ℕ∞

One-way deterministic communication complexity of f: the infimum, over one-way protocols computing f, of protocol bit cost.

Equations

• CommunicationComplexity.Deterministic.OneWay.communicationComplexity f = ⨅ (p : CommunicationComplexity.Deterministic.OneWay.Protocol X Y α), ⨅ (_ : p.Computes f), ↑p.cost

theorem CommunicationComplexity.Deterministic.OneWay.communicationComplexity_le_iff {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (n : ℕ) : communicationComplexity f ≤ ↑n ↔ ∃ (p : Protocol X Y α), p.Computes f ∧ p.cost ≤ n

Characterization of one-way communication complexity bounds by existence of a one-way protocol with bounded cost.

theorem CommunicationComplexity.Deterministic.OneWay.le_communicationComplexity_iff {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (k : ℕ) : ↑k ≤ communicationComplexity f ↔ ∀ (p : Protocol X Y α), p.Computes f → k ≤ p.cost

theorem CommunicationComplexity.Deterministic.OneWay.deterministic_communicationComplexity_le_of_oneWay_le {X : Type u_1} {Y : Type u_2} {α : Type u_3} [Fintype α] [Nonempty α] (f : X → Y → α) (n : ℕ) (h : communicationComplexity f ≤ ↑n) : Deterministic.communicationComplexity f ≤ ↑n + ↑(Nat.clog 2 (Fintype.card α))

A one-way upper bound yields a deterministic upper bound, with additive ⌈log₂ |α|⌉ to let Bob send the decoded output in the interactive model.

theorem CommunicationComplexity.Deterministic.OneWay.deterministic_communicationComplexity_le_of_oneWay_le_bool {X : Type u_1} {Y : Type u_2} (f : X → Y → Bool) (n : ℕ) (h : communicationComplexity f ≤ ↑n) : Deterministic.communicationComplexity f ≤ ↑n + 1

Same as deterministic_communicationComplexity_le_of_oneWay_le but specialized to Bool.