Live-variable averaging for random restrictions

This module supplies the quantitative existence step needed to iterate the switching lemma without appealing to sampling or finite search. A coordinate is live under the independent p-restriction with probability exactly p. Consequently, after refining a fixed restriction rho, the expected number of surviving live variables is exactly p * rho.liveCount.

The final theorem turns an upper bound delta on any bad event into a good restriction with many survivors. If m = rho.liveCount and

delta * m + k < p * m,

then some restriction outside the bad event leaves at least k variables live below rho. This is a direct finite averaging argument. It introduces no concentration theorem, optimizer, sampler, or circuit search.

theorem Algebraic.AC0.RandomRestriction.probability_coordinate_live (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (selected : Fin n) : (probability n p atMostOne fun (rho : PartialAssignment n) => rho selected = none) = ↑p

A designated coordinate is live with probability exactly p.

noncomputable def Algebraic.AC0.RandomRestriction.expectedLiveCountAfter (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho : PartialAssignment n) : ENNReal

Expected live-variable count after independently refining rho.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.AC0.RandomRestriction.liveCount_refine_eq_sum_indicators {n : ℕ} (rho extension : PartialAssignment n) : ↑(rho.refine extension).liveCount = ∑ index ∈ rho.liveVariables, if extension index = none then 1 else 0

The live count of a refinement is the sum of the survival indicators over the coordinates currently live in the base restriction.

theorem Algebraic.AC0.RandomRestriction.expectedLiveCountAfter_eq (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho : PartialAssignment n) : expectedLiveCountAfter n p atMostOne rho = ↑p * ↑rho.liveCount

Exact first moment of the surviving live-variable count.

theorem Algebraic.AC0.RandomRestriction.exists_good_refinement_with_liveCount (n : ℕ) (p : NNReal) (atMostOne : p ≤ 1) (rho : PartialAssignment n) (bad : PartialAssignment n → Prop) [DecidablePred bad] (failureBound : ENNReal) (retained : ℕ) (failure : probability n p atMostOne bad ≤ failureBound) (room : failureBound * ↑rho.liveCount + ↑retained < ↑p * ↑rho.liveCount) : ∃ (extension : PartialAssignment n), ¬bad extension ∧ retained ≤ (rho.refine extension).liveCount

Finite averaging outside a bad event. If the bad mass can account for at most failureBound * rho.liveCount of the first moment and the displayed strict inequality leaves room for retained, some good refinement retains at least that many live variables.