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 ↑Δ) : SLang.DP (SLang.privNoisedQueryPure query Δ ε₁ ε₂) (↑↑ε₁ / ↑↑ε₂)

Differential privacy bound for a privNoisedQueryPure

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

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