Kearns–Saul inequality — both exponential-moment directions

Proved

DAREx.KearnsSaulMGF

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

delta-parameter-pruningmachine-learningprobability

Notation. $B$ is a Bernoulli random variable, $p=\Pr(B=1)$ , $t$ is an arbitrary real exponential-moment parameter, and $\Phi$ is defined below. For $0<p<1$ , let $\Phi(p)=(1-2p)/\log((1-p)/p)$ when $p\ne1/2$ , and $\Phi(1/2)=1/2$ . Then $0<\Phi(p)\le1/2$ , and for every real $t$ ,

(1-p)e^{-tp}+pe^{t(1-p)}\le\exp(\Phi(p)t^2/4).

The left side is the exponential moment of a centered Bernoulli( $p$ ) variable. Both signs of $t$ are part of the conclusion. Formalization note: explicitly sourced external analytic input, specialized to the open probability interval needed by DARE, together with the source's coefficient bound. The half-probability value is the removable-singularity extension in the proof of Berend–Kontorovich Theorem 4. It is not the one-sided refinement in Lemma 5.

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. 29, Theorem E.1 and equations (6)–(7); PDF p. 30, bounds on Phi following equation (8). Berend and Kontorovich, On the Concentration of the Missing Mass, https://arxiv.org/pdf/1210.3248v1, Section 3, PDF p. 3, Theorem 4, equation (6), proof PDF pp. 3–4.

Preamble

import Definitions.Def_DAREx_Model

Formal statement

namespace DAREx
theorem KearnsSaulMGF :
  ∀ p : ℝ, 0 < p → p < 1 →
    0 < phi p ∧ phi p ≤ 1 / 2 ∧
    ∀ t : ℝ, (1 - p) * Real.exp (-t * p) + p * Real.exp (t * (1 - p)) ≤
      Real.exp (phi p * t ^ 2 / 4) := 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. 29, Theorem E.1 and equations (6)–(7); PDF p. 30, bounds on Phi following equation (8). Berend and Kontorovich, On the Concentration of the Missing Mass, https://arxiv.org/pdf/1210.3248v1, Section 3, PDF p. 3, Theorem 4, equation (6), proof PDF pp. 3–4.

Read-back

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

This open theorem asserts that, for every real number $p$ satisfying $0<p<1$ , the explicitly defined scalar $\phi(p)$ satisfies both $0<\phi(p)$ and $\phi(p)\le\tfrac12$ , and, for every real number $t$ , $(1-p)\exp(-tp)+p\exp(t(1-p))\le\exp(\phi(p)t^2/4)$ . Here $\phi(p)=\tfrac12$ when $p=\tfrac12$ , and $\phi(p)=(1-2p)/\log((1-p)/p)$ otherwise; $\log$ is the real logarithm and $\exp$ is the real exponential. The left-hand side is explicitly the two-point weighted sum for a variable taking the centered values $-p$ and $1-p$ with weights $1-p$ and $p$ , respectively; no unspecified random variable or probability-space assumption occurs. The two bounds on $\phi(p)$ are conclusions in conjunction with the exponential inequality, not assumptions. The parameter $t$ is unrestricted and may be negative, zero, or positive; at $t=0$ the exponential inequality is $1\le1$ . The midpoint $p=\tfrac12$ is included using its designated value of $\phi$ , giving $\tfrac12\exp(-t/2)+\tfrac12\exp(t/2)\le\exp(t^2/8)$ ; the endpoints $p=0$ and $p=1$ 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