Appendix E.1, equation (8) — DARE output concentration

Proved

DAREx.DAREOutputConcentration

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 $n>0$ , fix any real influence coefficients $c_j=\Delta W_jx_j$ . Set $\bar c=n^{-1}\sum_jc_j$ and $\sigma^2=n^{-1}\sum_j(c_j-\bar c)^2$ . Let $0<p<1$ be the drop probability and $0<\gamma<1$ the allowed failure probability. Draw independent Bernoulli( $p$ ) drop indicators $\omega_j$ and define $H=\sum_jc_j(1-(1-\omega_j)/(1-p))$ . Put $\Phi(1/2)=1/2$ and $\Phi(p)=(1-2p)/\log((1-p)/p)$ otherwise. Then

\Pr\left\{|H|\le\frac{\sqrt{\Phi(p)}}{1-p}\sqrt{n(\bar c^2+\sigma^2)}\sqrt{\log(2/\gamma)}\right\}\ge1-\gamma.

There is no nonzero-coefficient or positive-energy hypothesis. Formalization note: equation (8), using the source's coefficient-energy identity, with an explicit continuous value at $p=1/2$ . This is not the piecewise formula printed in Theorem 3.1: the missing square root and the one-sided high-pruning refinement are not imported. The mission description explains the distinction.

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, Appendix E.1, PDF p. 30, equation (8); PDF p. 31, unnumbered coefficient-energy identity; Section 3.2, PDF p. 5, equation (2) and Theorem 3.1 notation.

Preamble

import Definitions.Def_DAREx_Model

Formal statement

namespace DAREx
theorem DAREOutputConcentration :
  ∀ (n : ℕ) (c : Fin n → ℝ) (p γ : ℝ),
    0 < n → 0 < p → p < 1 → 0 < γ → γ < 1 →
    1 - γ ≤ probability p (fun ω ↦ |dareError p c ω| ≤
      Real.sqrt (phi p) / (1 - p) *
        Real.sqrt ((n : ℝ) * (empiricalMean c ^ 2 + empiricalVariance c)) *
        Real.sqrt (Real.log (2 / γ))) := 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, Appendix E.1, PDF p. 30, equation (8); PDF p. 31, unnumbered coefficient-energy identity; Section 3.2, PDF p. 5, equation (2) and Theorem 3.1 notation.

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,\gamma$ satisfying $0<n$ , $0<p<1$ , and $0<\gamma<1$ , one has $1-\gamma\le\sum_{\omega\in\Omega_n:\ |D(\omega)|\le R}w_p(\omega)$ , where $R=\dfrac{\sqrt{\phi(p)}}{1-p}\sqrt{n(\bar c^{\,2}+s_c^2)}\sqrt{\log(2/\gamma)}$ , $\bar c=(\sum_{j\in I_n}c_j)/n$ , and $s_c^2=(\sum_{j\in I_n}(c_j-\bar c)^2)/n$ . The natural number $n$ is interpreted as a real number in these formulas and the variance uses denominator $n$ , not $n-1$ . Here $\Omega_n=\{\mathsf{false},\mathsf{true}\}^{I_n}$ , $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$ , so the sum is the probability for independent Boolean coordinates each true with probability $p$ ; $D(\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/(1-p)$ ; and $\phi(p)=\tfrac12$ if $p=\tfrac12$ , otherwise $\phi(p)=(1-2p)/\log((1-p)/p)$ . The square roots are real square roots, with the total convention that a nonpositive input has square root $0$ . The good event uses the weak inequality $|D(\omega)|\le R$ and is centered at error $0$ . There is no positivity assumption on $\sum_jc_j^2$ , no separate assumption about $\phi(p)$ , and no sign or nonzero restriction on the coefficients. In particular, the identically zero coefficient family is included: then $D=R=0$ and the event contains every mask. The case $n=0$ is excluded, but $n=1$ is included and has $s_c^2=0$ ; both endpoints of each interval for $p$ and $\gamma$ are excluded. 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