Yao's minimax principle for decision trees

The distributional complexity D^ν_ε(f) of f for a distribution ν on the inputs is the least depth of a deterministic decision tree that errs with probability at most ε on inputs drawn from ν (QueryComplexity.distributionalComplexity). Yao's minimax principle [Yao77] says that the randomized complexity is the distributional complexity of a hardest distribution: R_ε(f) = max_ν D^ν_ε(f) (QueryComplexity.randomizedComplexity_eq_iSup_distributionalComplexity, QueryComplexity.exists_distributionalComplexity_eq_randomizedComplexity).

One inequality is the averaging argument: some tree that an optimal randomized tree can draw does as well as the randomized tree on inputs drawn from ν (RandomizedDecisionTree.Computes.exists_distributionalError_le). This is the direction used for lower bounds: a distribution on which every shallow tree errs often bounds R_ε(f) below (QueryComplexity.distributionalComplexity_le_randomizedComplexity).

The other inequality is the minimax theorem for a finite two-player zero-sum game (Convexity.StdSimplex.exists_forall_sum_le_of_forall_exists_sum_le, in Complexity.Probability.Minimax), which follows from Sion's minimax theorem in Mathlib [Sio58]. The algorithm player picks the set of inputs on which a tree of depth at most d errs, of which there are finitely many, the input player picks an input, and the payoff is 1 when the tree errs. If every distribution on the inputs has a tree of depth at most d erring with probability at most ε, the minimax theorem gives a distribution over such trees erring with probability at most ε on every input (QueryComplexity.exists_computes_of_forall_exists_distributionalError_le).

Main definitions

• Cslib.QueryComplexity.distributionalComplexity: the distributional complexity D^ν_ε(f).

Main results

• Cslib.QueryComplexity.distributionalComplexity_le_randomizedComplexity: D^ν_ε(f) ≤ R_ε(f).
• Cslib.QueryComplexity.exists_computes_of_forall_exists_distributionalError_le: the converse for a fixed depth.
• Cslib.QueryComplexity.randomizedComplexity_eq_iSup_distributionalComplexity: Yao's minimax principle, R_ε(f) = ⨆ ν, D^ν_ε(f).
• Cslib.QueryComplexity.exists_distributionalComplexity_eq_randomizedComplexity: some distribution is hardest.

References

• A. C.-C. Yao, Probabilistic computations: toward a unified measure of complexity
• M. Sion, On general minimax theorems

noncomputable def Cslib.QueryComplexity.distributionalComplexity {ι : Type u_1} {β : Type u_2} (ε : ℝ) (ν : Convexity.StdSimplex ℝ (ι → Bool)) (f : (ι → Bool) → β) : ℕ

The distributional complexity D^ν_ε(f): the least depth of a decision tree that errs with probability at most ε on inputs drawn from ν. It is 0 when no decision tree qualifies, which over finitely many variables happens exactly for ε < 0.

theorem Cslib.QueryComplexity.distributionalComplexity_le_depth {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ν : Convexity.StdSimplex ℝ (ι → Bool)} {ε : ℝ} {t : DecisionTree ι β} (h : t.distributionalError ν f ≤ ε) : distributionalComplexity ε ν f ≤ t.depth

theorem Cslib.QueryComplexity.distributionalComplexity_of_neg {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ν : Convexity.StdSimplex ℝ (ι → Bool)} {ε : ℝ} (hε : ε < 0) : distributionalComplexity ε ν f = 0

D^ν_ε(f) = 0 for ε < 0, where no decision tree qualifies.

theorem Cslib.QueryComplexity.exists_distributionalError_le_depth_eq_distributionalComplexity {ι : Type u_1} {β : Type u_2} {ε : ℝ} [Finite ι] (hε : 0 ≤ ε) (ν : Convexity.StdSimplex ℝ (ι → Bool)) (f : (ι → Bool) → β) : ∃ (t : DecisionTree ι β), t.distributionalError ν f ≤ ε ∧ t.depth = distributionalComplexity ε ν f

For ε ≥ 0 the distributional complexity is attained: some decision tree of depth D^ν_ε(f) errs with probability at most ε on inputs drawn from ν.

theorem Cslib.QueryComplexity.distributionalComplexity_le_randomizedComplexity {ι : Type u_1} {β : Type u_2} [Finite ι] (ε : ℝ) (ν : Convexity.StdSimplex ℝ (ι → Bool)) (f : (ι → Bool) → β) : distributionalComplexity ε ν f ≤ randomizedComplexity ε f

The easy direction of Yao's principle: D^ν_ε(f) ≤ R_ε(f) for every distribution ν on the inputs. To bound R_ε(f) below, it suffices to find a distribution on which every shallow decision tree errs often.

theorem Cslib.QueryComplexity.exists_computes_of_forall_exists_distributionalError_le {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε : ℝ} {d : ℕ} [Finite ι] (h : ∀ (ν : Convexity.StdSimplex ℝ (ι → Bool)), ∃ (t : DecisionTree ι β), t.depth ≤ d ∧ t.distributionalError ν f ≤ ε) : ∃ (μ : RandomizedDecisionTree ι β), μ.Computes ε f ∧ μ.depth ≤ d

The hard direction of Yao's principle, by the minimax theorem: if for every distribution ν on the inputs some decision tree of depth at most d errs with probability at most ε on inputs drawn from ν, then some randomized decision tree of depth at most d computes f with error ε.

theorem Cslib.QueryComplexity.randomizedComplexity_le_iff_forall_distributionalComplexity_le {ι : Type u_1} {β : Type u_2} {f : (ι → Bool) → β} {ε : ℝ} {d : ℕ} [Finite ι] : randomizedComplexity ε f ≤ d ↔ ∀ (ν : Convexity.StdSimplex ℝ (ι → Bool)), distributionalComplexity ε ν f ≤ d

R_ε(f) ≤ d exactly when D^ν_ε(f) ≤ d for every distribution ν on the inputs.

theorem Cslib.QueryComplexity.randomizedComplexity_eq_iSup_distributionalComplexity {ι : Type u_1} {β : Type u_2} [Finite ι] (ε : ℝ) (f : (ι → Bool) → β) : randomizedComplexity ε f = ⨆ (ν : Convexity.StdSimplex ℝ (ι → Bool)), distributionalComplexity ε ν f

Yao's minimax principle: the randomized decision tree complexity is the largest distributional complexity over the distributions on the inputs, R_ε(f) = ⨆ ν, D^ν_ε(f).

theorem Cslib.QueryComplexity.exists_distributionalComplexity_eq_randomizedComplexity {ι : Type u_1} {β : Type u_2} [Finite ι] (ε : ℝ) (f : (ι → Bool) → β) : ∃ (ν : Convexity.StdSimplex ℝ (ι → Bool)), distributionalComplexity ε ν f = randomizedComplexity ε f

Yao's minimax principle, with a hardest distribution: some distribution ν on the inputs has D^ν_ε(f) = R_ε(f).