Switching lemmas against parity -- proof internals

theorem Complexity.DNF.freeVariables_card_le_switchingDepth_of_xorBool_internal {N : ℕ} (formula : DNF N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) : restriction.freeVariables.card ≤ (formula.switchingDecisionTreeUnder restriction).depth

theorem Complexity.DNF.freeVariables_atLeast_implies_switchingBad_internal {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (queryCount : ℕ) (restriction : Restriction.On N) (hfree : queryCount ≤ restriction.freeVariables.card) : formula.switchingBad queryCount restriction

theorem Complexity.DNF.freeVariables_eventCount_le_switchingBad_internal {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) ≤ RandomRestriction.eventCount q (formula.switchingBad queryCount)

theorem Complexity.DNF.switchingParity_width_counting_bound_internal {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.DNF.switchingParity_width_one_free_bound_internal {N : ℕ} (formula : DNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q : ℕ) : ((2 * q + 1) ^ N - (2 * q) ^ N) * q ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1))

theorem Complexity.CNF.freeVariables_card_le_switchingDepth_of_xorBool_internal {N : ℕ} (formula : CNF N) (restriction : Restriction.On N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) : restriction.freeVariables.card ≤ (formula.switchingDecisionTreeUnder restriction).depth

theorem Complexity.CNF.freeVariables_atLeast_implies_switchingBad_internal {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (queryCount : ℕ) (restriction : Restriction.On N) (hfree : queryCount ≤ restriction.freeVariables.card) : formula.switchingBad queryCount restriction

theorem Complexity.CNF.freeVariables_eventCount_le_switchingBad_internal {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) ≤ RandomRestriction.eventCount q (formula.switchingBad queryCount)

theorem Complexity.CNF.switchingParity_width_counting_bound_internal {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q queryCount : ℕ) : (RandomRestriction.eventCount q fun (restriction : Restriction.On N) => queryCount ≤ restriction.freeVariables.card) * q ^ queryCount ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1)) ^ queryCount

theorem Complexity.CNF.switchingParity_width_one_free_bound_internal {N : ℕ} (formula : CNF N) (computes : ∀ (input : BitString N), formula.eval input = Schnorr.xorBool N input) (q : ℕ) : ((2 * q + 1) ^ N - (2 * q) ^ N) * q ≤ (2 * q + 1) ^ N * (4 * (formula.width + 1))