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

The syntactic transcript of a deterministic protocol.

For a fixed protocol, this is exactly the message sequence: terminal protocols have one transcript, and each communication node contributes one Boolean plus the remaining child transcript.

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).Transcript = Unit
• (CommunicationComplexity.Deterministic.Protocol.alice f P).Transcript = ((b : Bool) × (P b).Transcript)
• (CommunicationComplexity.Deterministic.Protocol.bob f P).Transcript = ((b : Bool) × (P b).Transcript)

def CommunicationComplexity.Deterministic.Protocol.Transcript.output {X : Type u_1} {Y : Type u_2} {α : Type u_3} {p : Protocol X Y α} : p.Transcript → α

The protocol output attached to a syntactic transcript.

Equations

• x_2.output = val
• t.output = t.snd.output
• t.output = t.snd.output

def CommunicationComplexity.Deterministic.Protocol.Transcript.inputSet {X : Type u_1} {Y : Type u_2} {α : Type u_3} {p : Protocol X Y α} : p.Transcript → Set (X × Y)

The rectangle of inputs that follow a syntactic transcript.

Equations

• x_2.inputSet = Set.univ
• t.inputSet = {xy : X × Y | f xy.1 = t.fst ∧ t.snd.inputSet xy}
• t.inputSet = {xy : X × Y | f xy.2 = t.fst ∧ t.snd.inputSet xy}

theorem CommunicationComplexity.Deterministic.Protocol.Transcript.inputSet_isRectangle {X : Type u_1} {Y : Type u_2} {α : Type u_3} {p : Protocol X Y α} (t : p.Transcript) : Rectangle.IsRectangle t.inputSet

The rectangle represented by a syntactic transcript is a rectangle.

noncomputable instance CommunicationComplexity.Deterministic.Protocol.transcriptFintype {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : Fintype p.Transcript

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).transcriptFintype = inferInstanceAs (Fintype Unit)
• (CommunicationComplexity.Deterministic.Protocol.alice f P).transcriptFintype = inferInstanceAs (Fintype ((b : Bool) × (P b).Transcript))
• (CommunicationComplexity.Deterministic.Protocol.bob f P).transcriptFintype = inferInstanceAs (Fintype ((b : Bool) × (P b).Transcript))

instance CommunicationComplexity.Deterministic.Protocol.transcriptMeasurableSpace {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : MeasurableSpace p.Transcript

Equations

• p.transcriptMeasurableSpace = ⊤

def CommunicationComplexity.Deterministic.Protocol.transcript {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : X × Y → p.Transcript

Execute a protocol and return the syntactic transcript reached by the input.

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).transcript x✝ = ()
• (CommunicationComplexity.Deterministic.Protocol.alice f P).transcript x✝ = ⟨f x✝.1, (P (f x✝.1)).transcript x✝⟩
• (CommunicationComplexity.Deterministic.Protocol.bob f P).transcript x✝ = ⟨f x✝.2, (P (f x✝.2)).transcript x✝⟩

theorem CommunicationComplexity.Deterministic.Protocol.mem_transcript {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (xy : X × Y) : xy ∈ (p.transcript xy).inputSet

The input follows its own transcript.

theorem CommunicationComplexity.Deterministic.Protocol.transcript_eq_of_mem {X : Type u_1} {Y : Type u_2} {α : Type u_3} {p : Protocol X Y α} (t : p.Transcript) {xy : X × Y} : xy ∈ t.inputSet → p.transcript xy = t

If an input follows a syntactic transcript, then this is its computed transcript.

theorem CommunicationComplexity.Deterministic.Protocol.run_eq_transcript_output {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (xy : X × Y) : p.run xy.1 xy.2 = (p.transcript xy).output

The output attached to the reached transcript is the protocol output.

theorem CommunicationComplexity.Deterministic.Protocol.run_eq_of_transcript_eq {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) {xy xy' : X × Y} (h : p.transcript xy = p.transcript xy') : p.run xy.1 xy.2 = p.run xy'.1 xy'.2

Inputs with the same transcript have the same protocol output.

theorem CommunicationComplexity.Deterministic.Protocol.card_transcript_le_two_pow_complexity {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : Fintype.card p.Transcript ≤ 2 ^ p.complexity

A protocol has at most 2 ^ complexity syntactic transcripts.

def CommunicationComplexity.Deterministic.Protocol.transcriptSwap {X : Type u_1} {Y : Type u_2} {α : Type u_3} {p : Protocol X Y α} : p.Transcript → p.swap.Transcript

Swap a syntactic transcript by swapping Alice and Bob throughout the protocol.

Equations

• CommunicationComplexity.Deterministic.Protocol.transcriptSwap x_2 = ()
• CommunicationComplexity.Deterministic.Protocol.transcriptSwap t = ⟨t.fst, CommunicationComplexity.Deterministic.Protocol.transcriptSwap t.snd⟩
• CommunicationComplexity.Deterministic.Protocol.transcriptSwap t = ⟨t.fst, CommunicationComplexity.Deterministic.Protocol.transcriptSwap t.snd⟩

theorem CommunicationComplexity.Deterministic.Protocol.transcriptSwap_injective {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) : Function.Injective transcriptSwap

Swapping Alice and Bob preserves the message sequence injectively.

theorem CommunicationComplexity.Deterministic.Protocol.transcriptSwap_transcript {X : Type u_1} {Y : Type u_2} {α : Type u_3} (p : Protocol X Y α) (x : X) (y : Y) : transcriptSwap (p.transcript (x, y)) = p.swap.transcript (y, x)

def CommunicationComplexity.Deterministic.Protocol.transcriptComap {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) : p.Transcript → (p.comap fX fY).Transcript

Pull a syntactic transcript back along maps on Alice's and Bob's inputs.

Equations

• (CommunicationComplexity.Deterministic.Protocol.output val).transcriptComap x✝¹ x✝ x_6 = ()
• (CommunicationComplexity.Deterministic.Protocol.alice f P).transcriptComap x✝¹ x✝ t = ⟨t.fst, (P t.fst).transcriptComap x✝¹ x✝ t.snd⟩
• (CommunicationComplexity.Deterministic.Protocol.bob f P).transcriptComap x✝¹ x✝ t = ⟨t.fst, (P t.fst).transcriptComap x✝¹ x✝ t.snd⟩

theorem CommunicationComplexity.Deterministic.Protocol.transcriptComap_injective {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) : Function.Injective (p.transcriptComap fX fY)

Pulling a transcript back along input maps preserves the message sequence injectively.

theorem CommunicationComplexity.Deterministic.Protocol.transcriptComap_transcript {X : Type u_1} {Y : Type u_2} {α : Type u_3} {X' : Type u_4} {Y' : Type u_5} (p : Protocol X Y α) (fX : X' → X) (fY : Y' → Y) (x' : X') (y' : Y') : p.transcriptComap fX fY (p.transcript (fX x', fY y')) = (p.comap fX fY).transcript (x', y')