def combineConcentrated (U : ℕ+) (ε₁ : ℕ+) (ε₂ : ℕ+) : SLang.DPSystem.prop (SLang.privNoisedBoundedMean U ε₁ ε₂) (↑↑ε₁ / ↑↑ε₂)

Equations

• combineConcentrated = ⋯

def combinePure (U : ℕ+) (ε₁ : ℕ+) (ε₂ : ℕ+) : SLang.DPSystem.prop (SLang.privNoisedBoundedMean U ε₁ ε₂) (↑↑ε₁ / ↑↑ε₂)

Equations

• combinePure = ⋯

def numBins : ℕ+

Equations

• numBins = 64

def bin (n : ℕ) : Fin ↑numBins

Equations

• bin n = ⟨min (Nat.log 2 n) numBins.natPred, ⋯⟩

def unbin (n : Fin ↑numBins) : ℕ+

Equations

• unbin n = 2 ^ (1 + ↑n)

noncomputable def combineMeanHistogram : SLang.Mechanism ℕ (Option ℚ)

Equations

• combineMeanHistogram = SLang.privMeanHistogram SLang.PureDPSystem numBins { bin := bin } unbin 1 20 2 1 20