@[simp]

theorem CommunicationComplexity.Internal.enat_iInf_le_coe_iff {ι : Sort u_1} {f : ι → ℕ∞} {n : ℕ} : iInf f ≤ ↑n ↔ ∃ (i : ι), f i ≤ ↑n

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

Equations

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

theorem CommunicationComplexity.Deterministic.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.complexity ≤ n

theorem CommunicationComplexity.Deterministic.communicationComplexity_le_iff_finiteMessage {X : Type u_1} {Y : Type u_2} {α : Type u_3} (f : X → Y → α) (n : ℕ) : communicationComplexity f ≤ ↑n ↔ ∃ (p : FiniteMessage.Protocol X Y α), p.run = f ∧ p.complexity ≤ n

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