Rescaled pruning — exact bias, variance, and mean square

Proved

DAREx.RescaledErrorMoments

by Minghui · Sep 29, 2026 · Mathlib c5ea003 (Lean v4.30.0)

delta-parameter-pruningmachine-learningprobability

Notation. $\Omega=\{0,1\}^n$ is the finite space of Bernoulli drop masks; $n$ is the number of coordinates and $p$ is the drop probability. Coefficients are fixed before drawing the mask. For any $n\ge0$ , fixed coefficients $c_j\in\mathbb R$ , $0\le p\le1$ , and $q>0$ , draw independent Bernoulli( $p$ ) drop indicators $\omega_j$ . Put $H_q=\sum_jc_j(1-(1-\omega_j)/q)$ , $S=\sum_jc_j$ , $Q=\sum_jc_j^2$ , and $b_q=(1-(1-p)/q)S$ . Then

\mathbb EH_q=b_q,\qquad\mathbb E(H_q-b_q)^2=\frac{p(1-p)}{q^2}Q,

\mathbb EH_q^2=b_q^2+\frac{p(1-p)}{q^2}Q.

Expectations are finite product-mask sums. Formalization note: paper-derived extension of the DARE moment calculation to the general $1/q$ rescaling model; this does not assert the optimizer or tail formula later printed in Appendix E.2. Empty vectors and deterministic endpoint masks are included.

Source: Deng et al., DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025, arXiv:2410.09344v2, https://arxiv.org/pdf/2410.09344v2, Section 3.2, PDF p. 5, equation (2); Appendix E.1, PDF p. 29, initial unnumbered mean/variance calculations; Appendix E.2, PDF p. 31, initial unnumbered general-rescaling identity.

Preamble

import Definitions.Def_DAREx_Model

Formal statement

namespace DAREx
theorem RescaledErrorMoments :
  ∀ (n : ℕ) (c : Fin n → ℝ) (p q : ℝ), 0 ≤ p → p ≤ 1 → 0 < q →
    mean p (outputError q c) = outputBias p q c ∧
    mean p (fun ω ↦ (outputError q c ω - outputBias p q c) ^ 2) =
      p * (1 - p) / q ^ 2 * energy c ∧
    mean p (fun ω ↦ outputError q c ω ^ 2) =
      outputBias p q c ^ 2 + p * (1 - p) / q ^ 2 * energy c := by sorry
end DAREx

Source

Deng et al., DARE the Extreme: Revisiting Delta-Parameter Pruning For Fine-Tuned Models, ICLR 2025, arXiv:2410.09344v2, https://arxiv.org/pdf/2410.09344v2, Section 3.2, PDF p. 5, equation (2); Appendix E.1, PDF p. 29, initial unnumbered mean/variance calculations; Appendix E.2, PDF p. 31, initial unnumbered general-rescaling identity.

Read-back

What the Lean code literally says, in plain math · inherited model (exact model identifier unavailable)

This open theorem asserts that, for every natural number $n$ , every real coefficient family $c:I_n\to\mathbb R$ with $I_n=\{0,\ldots,n-1\}$ , and every pair of real numbers $p,q$ satisfying $0\le p\le1$ and $0<q$ , the following three equalities hold simultaneously. Let $\Omega_n=\{\mathsf{false},\mathsf{true}\}^{I_n}$ , assign each mask weight $w_p(\omega)=\prod_{j\in I_n}a_p(\omega_j)$ with $a_p(\mathsf{true})=p$ and $a_p(\mathsf{false})=1-p$ , and define $\mathcal M_p(f)=\sum_{\omega\in\Omega_n}w_p(\omega)f(\omega)$ . These are the weights of independent Boolean coordinates that are true with probability $p$ . Put $C=\sum_{j\in I_n}c_j$ , $V=\sum_{j\in I_n}c_j^2$ , $E(\omega)=\sum_{j\in I_n}(c_j-h_j(\omega_j))$ , where $h_j(\mathsf{true})=0$ and $h_j(\mathsf{false})=c_j/q$ , and $b=(1-(1-p)/q)C$ . Then $\mathcal M_p(E)=b$ , $\mathcal M_p(\omega\mapsto(E(\omega)-b)^2)=p(1-p)V/q^2$ , and $\mathcal M_p(\omega\mapsto E(\omega)^2)=b^2+p(1-p)V/q^2$ . The parameter $q$ can be any positive real number and is not required to equal $1-p$ or to be at most $1$ ; no nonzero-energy or positive-size assumption is imposed. The endpoints $p=0$ and $p=1$ are included: the product distribution is then deterministic and the claimed centered second moment is $0$ . The empty case $n=0$ is included, has exactly one mask of weight $1$ , and has $C=V=E=b=0$ , so all three equalities read $0=0$ ; the zero coefficient family is also included for every $n$ . The supplied proof slot is a placeholder; no completed proof is supplied.

Human review

Endorsed by Shuze Chen · Sep 29, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 29, 2026
Confirmed by the mission captain (proposal self-audit).

View graph