Property 3.3 — the Net mechanism is ε-differentially private

Proved

PrivateRelease.NetMechanism.property_3_3

by mikedeng1 · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

differential-privacyexponential-mechanismp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1query-release

Let $X$ be a finite data universe, $n$ an input size, $\mathcal Q$ a class of real-valued queries on databases, $\alpha$ a real number and $N$ a minimum $\alpha$ -net for $\mathcal Q$ (the paper's $N_\alpha(C)$ ), and suppose the Net mechanism's quality score $q(z,D')=-\max_{Q\in\mathcal Q}|Q(z)-Q(D')|$ has positive sensitivity $GS_q$ over $N$ . Then for every $\varepsilon>0$ the Net mechanism with parameter $\varepsilon$ is $\varepsilon$ -differentially private:

\Pr[\mathrm{Net}(z)\in S]\le e^{\varepsilon}\,\Pr[\mathrm{Net}(z')\in S]

for all inputs $z,z'$ differing in one entry and all sets $S$ of output databases, and each output law is a probability distribution.

Together with the utility results that follow, this is the "private" half of the paper's main theorem.

Formalization Note Neighbours differ in exactly one entry. The hypothesis $GS_q>0$ is where the exponential mechanism's formula is defined.

Preamble

import Mathlib
import Definitions.Def_PrivateRelease_NetMechanism_ExpMech

Formal statement

namespace PrivateRelease.NetMechanism

open MeasureTheory

/-- Property 3.3 (p. 8): the Net mechanism (run on a minimum α-net `N = N_α(C)`, with a quality
score of positive sensitivity) is ε-differentially private, and its output laws are probability
measures. -/
theorem property_3_3 {X : Type} [Fintype X] {n : ℕ} (QC : Set (Multiset X → ℝ)) (ε α : ℝ)
    (N : Finset (Database X)) (hN : IsMinNet QC α N) (hsens : 0 < netSens n QC N)
    (hε : 0 < ε) :
    PrivLearn.Generic.IsDP (netMech (n := n) QC ε N) ε ∧
      ∀ z : Fin n → X, IsProbabilityMeasure (netMech QC ε N z) := by sorry

end PrivateRelease.NetMechanism

Source

Blum, Ligett, Roth, A Learning Theory Approach to Non-Interactive Database Privacy, arXiv:1109.2229v1 (2011), p. 8, Property 3.3

Human review

Endorsed by Shuze Chen · Oct 8, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph