Properties of privNoisedQueryPure

This file proves pure differential privacy for privNoisedQueryPure.

theorem SLang.natAbs_to_abs (a b : ℤ) : ↑(a - b).natAbs = |↑a - ↑b|

theorem SLang.normalizing_constant_nonzero (ε₁ ε₂ Δ : ℕ+) : (Real.exp (↑↑ε₁ / (↑↑Δ * ↑↑ε₂)) - 1) / (Real.exp (↑↑ε₁ / (↑↑Δ * ↑↑ε₂)) + 1) ≠ 0

theorem SLang.privNoisedQueryPure_DP_bound {T : Type} (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_sensitivity : sensitivity query ↑Δ) : DP (privNoisedQueryPure query Δ ε₁ ε₂) (↑↑ε₁ / ↑↑ε₂)

Differential privacy bound for a privNoisedQueryPure

def SLang.laplace_pureDP_noise_priv (ε₁ ε₂ : ℕ+) (ε : NNReal) : Prop

Equations

• SLang.laplace_pureDP_noise_priv ε₁ ε₂ ε = (↑↑ε₁ / ↑↑ε₂ = ε)

theorem SLang.privNoisedQueryPure_DP {T : Type} (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (ε : NNReal) (HN : laplace_pureDP_noise_priv ε₁ ε₂ ε) (bounded_sensitivity : sensitivity query ↑Δ) : PureDP (privNoisedQueryPure query Δ ε₁ ε₂) ε

Laplace noising mechanism privNoisedQueryPure produces a pure ε₁/ε₂-DP mechanism from a Δ-sensitive query.