Appendix E.1 — exponential tail for DARE output error

Proved

DAREx.DAREExponentialTail

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. Fix $n\ge0$ , deterministic $c\in\mathbb R^n$ , $0<p<1$ , energy $Q=\sum_jc_j^2>0$ , and $t>0$ . Draw independent Bernoulli( $p$ ) drop indicators and let $H=\sum_jc_j(1-(1-\omega_j)/(1-p))$ . With $\Phi$ defined by the logarithmic quotient and $\Phi(1/2)=1/2$ ,

\Pr(|H|>t)\le2\exp\left(-\frac{t^2(1-p)^2}{\Phi(p)Q}\right).

Formalization note: direct source tail formula with explicit positive energy for its denominator; strict $>t$ matches the source. Arbitrary signed coefficients are allowed. The main confidence-bound goal separately includes the zero-energy case.

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. 30, unnumbered tail display immediately preceding equation (8), from Theorem E.1, PDF p. 29, equations (6)–(7).

Preamble

import Definitions.Def_DAREx_Model

Formal statement

namespace DAREx
theorem DAREExponentialTail :
  ∀ (n : ℕ) (c : Fin n → ℝ) (p t : ℝ),
    0 < p → p < 1 → 0 < energy c → 0 < t →
    probability p (fun ω ↦ t < |dareError p c ω|) ≤
      2 * Real.exp (-(t ^ 2 * (1 - p) ^ 2 / (phi p * 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. 30, unnumbered tail display immediately preceding equation (8), from Theorem E.1, PDF p. 29, equations (6)–(7).

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,t$ satisfying $0<p<1$ , $V:=\sum_{j\in I_n}c_j^2>0$ , and $t>0$ , one has $\sum_{\omega\in\Omega_n:\ t<|D(\omega)|}w_p(\omega)\le2\exp\!\bigl(-t^2(1-p)^2/(\phi(p)V)\bigr)$ . 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 left-hand side is the probability under the finite product distribution of independent Boolean coordinates each true with probability $p$ ; $D(\omega)=\sum_{j\in I_n}(c_j-h_j(\omega_j))$ with $h_j(\mathsf{true})=0$ and $h_j(\mathsf{false})=c_j/(1-p)$ ; and $\phi(p)=\tfrac12$ at $p=\tfrac12$ and $\phi(p)=(1-2p)/\log((1-p)/p)$ otherwise. Thus the error is a sum of $c_j$ on true coordinates and $c_j-c_j/(1-p)$ on false coordinates, with no subtraction of a separately introduced bias. The bad event is strictly $t<|D(\omega)|$ , so masks with $|D(\omega)|=t$ are not counted. There are no sign or sum constraints on $c$ , no upper bound on $t$ , and no separately stated lower bound on $\phi(p)$ ; the only explicit energy hypothesis is $V>0$ , which makes the premises unsatisfiable for $n=0$ or for the identically zero coefficient family. The size $n=1$ and all nonzero real coefficient families are otherwise included. The bound is the displayed exponential expression itself, with no truncation at $1$ . 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