theorem SLang.NoisedQuery_NonZeroNQPureDP {T : Type} (query : List T → ℤ) (Δ : ℕ+) (ε₁ : ℕ+) (ε₂ : ℕ+) : SLang.NonZeroNQ (SLang.privNoisedQueryPure query Δ ε₁ ε₂)

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

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

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

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