Finite-family switching corollaries

Depth reduction must simplify every formula at a circuit layer, not just one formula. The exact finite union bound lifts the DNF and CNF switching lemmas to an indexed family: the probability that any of M width-t formulas retains decision-tree depth at least s is at most M * (5pt)^s.

This is the ordinary union-bound corollary of the single-formula switching lemma. It is intentionally not called a multi-switching lemma, whose conclusion would provide one common shallow decision tree for an entire family.

theorem Algebraic.AC0.RandomRestriction.probability_exists_dnf_depthAtLeast_restrict_le_five {formulaCount n widthBound : ℕ} (formulas : Fin formulaCount → DNF n) (bounded : ∀ (index : Fin formulaCount), (formulas index).WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (index : Fin formulaCount), DecisionTree.DepthAtLeast ((formulas index).restrict rho).eval pathLength) ≤ ↑formulaCount * (5 * ↑p * ↑widthBound) ^ pathLength

Finite-family DNF switching bound obtained by a union bound.

theorem Algebraic.AC0.RandomRestriction.probability_exists_dnf_not_depthAtMost_restrict_le_five {formulaCount n widthBound : ℕ} (formulas : Fin formulaCount → DNF n) (bounded : ∀ (index : Fin formulaCount), (formulas index).WidthAtMost widthBound) (depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (index : Fin formulaCount), ¬DecisionTree.DepthAtMost ((formulas index).restrict rho).eval depthBound) ≤ ↑formulaCount * (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Off-by-one finite-family DNF form used to obtain a simultaneous depth upper bound.

theorem Algebraic.AC0.RandomRestriction.probability_exists_cnf_depthAtLeast_restrict_le_five {formulaCount n widthBound : ℕ} (formulas : Fin formulaCount → CNF n) (bounded : ∀ (index : Fin formulaCount), (formulas index).WidthAtMost widthBound) (pathLength : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (index : Fin formulaCount), DecisionTree.DepthAtLeast ((formulas index).restrict rho).eval pathLength) ≤ ↑formulaCount * (5 * ↑p * ↑widthBound) ^ pathLength

Finite-family CNF switching bound obtained by De Morgan duality and a union bound.

theorem Algebraic.AC0.RandomRestriction.probability_exists_cnf_not_depthAtMost_restrict_le_five {formulaCount n widthBound : ℕ} (formulas : Fin formulaCount → CNF n) (bounded : ∀ (index : Fin formulaCount), (formulas index).WidthAtMost widthBound) (depthBound : ℕ) (p : NNReal) (atMostOne : p ≤ 1) : (probability n p atMostOne fun (rho : PartialAssignment n) => ∃ (index : Fin formulaCount), ¬DecisionTree.DepthAtMost ((formulas index).restrict rho).eval depthBound) ≤ ↑formulaCount * (5 * ↑p * ↑widthBound) ^ (depthBound + 1)

Off-by-one finite-family CNF form used to obtain a simultaneous depth upper bound.